Berry Schoenmakers

Armin Walch, Georg Moser, Berry Schoenmakers et al.

We study the fully automated amortised analysis of purely functional data structures like skew heaps, as well as weight- and rank-biased leftist heaps. For that we generalise earlier works on automated amortised resource analysis by developing a type inference based approach with a generic type system. This allows for modular reasoning and the inference of precise and optimal cost bounds. More specifically, we extend the work on the ATLAS system by Leutgeb et al. which was developed to cover the analysis of splay trees and some closely related data structures. To enable the analysis of skew heaps, however, and the even more challenging (amortised) analysis of leftist heaps, we have developed a range of new techniques for type-based automated analysis. By introducing a generic type system we allow for arbitrary (classes of) potential functions, compared to the use of hard-coded potential functions in ATLAS, which we have implemented in Haskell in an entirely modular way. We have also greatly enhanced the existing type inference algorithm by extensions in multiple directions, including path-sensitive reasoning, data structure invariants, and template parameters for piecewise defined potential functions. We show how our newly developed system supports the use of all known potential functions for analysing skew heaps and leftist heaps, confirming the known bounds.

Berry Schoenmakers

We present optimal binary pebbling algorithms for in-place reversal (backward traversal) of one-way hash chains. For a hash chain of length $2^k$, the number of hashes performed in each output round does not exceed $\lceil k/2 \rceil$, whereas the number of hash values stored (pebbles) throughout is at most $k$. We introduce a framework for rigorous comparison of explicit binary pebbling algorithms, including simple speed-1 binary pebbling, Jakobsson's speed-2 binary pebbling, and our optimal binary pebbling algorithm. Explicit schedules describe for each pebble exactly how many hashes need to be performed in each round. The optimal schedule turns out to be essentially unique and exhibits a nice recursive structure, which allows for fully optimized implementations that can readily be deployed. In particular, we develop the first in-place implementations with minimal storage overhead (essentially, storing only hash values), and fast implementations with minimal computational overhead.