ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures

Amortised analysis, as introduced by Sleator and Tarjan [47, 49], is a method for the worst-case cost analysis of data structures. The innovation of amortised analysis lies in considering the cost of a single data structure operation as part of a sequence of data structure operations. The methodology of amortised analysis allows one to assign a low (e.g., constant or logarithmic) amortised cost to a data structure operation even though the worst-case cost of a single operation might be high (e.g., linear, polynomial or worse). The setup of amortised analysis guarantees that for a sequence of data structure operations the worst-case cost is indeed the number of data structure operations times the amortised cost. In this way amortised cost analysis provides a methodology for worst-case cost analysis. Notably, the cost analysis of self-adjusting data structures, such as splay trees, has been a main objective already in the initial proposal of amortised analysis [47, 49]. Analysing these data structures requires sophisticated potential functions, which typically contain logarithmic expressions. Possibly for these reasons, and despite the recent progress in automated complexity analysis, they have so far eluded automation.

In this paper, we present the first fully-automated amortised cost analysis of self-adjusting data structures, that is, of splay trees, splay heaps and pairing heaps, which so far have only (semi-) manually been analysed in the literature. We implement and extend a recently proposed type-and-effect system for amortised resource analysis [26, 27]. This system belongs to a line of work (see [20, 22‐25, 28] and the references therein), where types are template potential functions with unknown coefficients and the type-and-effect system extracts constraints over these coefficients in a syntax directed way from the program under analysis. Our work improves over [26, 27] in three regards: 1) The approach of [26, 27] only supports type checking, i.e. verifying that a manually provided type is correct. In this paper, we add an optimisation layer to the set-up of [26, 27] in order to support type inference, i.e. our approach does not rely on manual annotations. Our target function steers the search towards coefficients that minimise the inferred amortised complexity. 2) The only case study of [26, 27] is partial, focusing on the zig-zig case of the splay tree function \(\mathtt {splay}\), while we report on the full analysis of the operations of several data structures. 3) [26, 27] does not report on a fully-automated analysis. Besides the requirement that the user needs to provide the resource annotation, the user also has to apply the structural rules of the type system manually. Our tool \(\mathsf {ATLAS}\) is able to analyse our benchmarks fully automatically. Achieving full automation required substantial implementation effort as the structural rules need to be applied carefully—as we learned during our experiments—in order to avoid a size explosion of the generated constraint system. We evaluate and discuss our design choices that lead to a scalable implementation.

With our implementation and the obtained experimental results we make two contributions to the complexity analysis of data structures:

1.) We automatically infer complexity estimates that match previous results (obtained by sophisticated pen-and-paper proofs), and in some cases even infer better complexity estimates than previously published. In Table 1, we state the complexity bounds computed by \(\mathsf {ATLAS}\) next to results from the literature. We match or improve the results from [37, 41, 42]. To the best of our knowledge, the bounds for splay trees and splay heaps represent the state-of-the-art. In particular, we improve the bound for the \(\mathtt {delete}\) function of splay trees and all bounds for the splay heap functions. For pairing heaps, Iacono [29, 30] has proven (using a more involved potential function) that \(\mathtt {insert}\) and \(\mathtt {merge}\) have constant amortised complexity, while the other data structure operations continue to have an amortised complexity of ; while we leave an automated analysis based on Iacono’s potential function for future work, we note that his coefficients k in the logarithmic terms are large, and that therefore the small coefficients in Table 1 are still of interest. We will detail below that we used a simpler potential function than [37, 41, 42] to obtain our results. Hence, also the new proofs of the confirmed complexity bounds can be considered a contribution.

\(^\mathrm{a}\)[42] uses a different cost metric, i.e. the numbers of arithmetic comparisons, whereas we and [37] count the number of (recursive) function applications. We adapted the results of [42] to our cost metric to make the results easier to compare, i.e. the coefficients of the logarithmic terms are by a factor 2 smaller compared to [42].

2.) We establish a new approach for the complexity analysis of data structures. Establishing the prior results in Table 1 required considerable effort. Schoenmakers studied in his PhD thesis [42] the best amortised complexity bounds that can be obtained using a parameterised potential function \(\phi (t)\), where t is a binary tree, defined by and , for real-valued parameters \(\alpha ,\beta > 0\). Carrying out a sophisticated optimisation with pen and paper, he concluded that the best bounds are obtained by setting \(\alpha = \root 3 \of {4}\) and \(\beta = \frac{1}{3}\) for splay trees, and by setting \(\alpha = \sqrt{2}\) and \(\beta = \frac{1}{2}\) for pairing heaps (splay heaps were proposed only some years later by Okasaki in [38]). Brinkop and Nipkow verify his complexity results for splay trees in the theorem prover Isabelle [37]. They note that manipulating the expressions corresponding to could only partly be automated¹. For splay heaps, there is to the best of our knowledge no previous attempt to optimise the obtained complexity bounds, which might explain why our optimising analysis was able to improve all bounds. For pairing heaps, Brinkop and Nipkow did not use the optimal parameters reported by Schoenmakers—probably in order to avoid reasoning about polynomial inequalities—, which explains the worse complexity bounds. In contrast to the discussed approaches, we were able to verify and improve the previous results fully automatically. Our approach uses a variation of Schoenmakers’ potential function, where we roughly fix \(\alpha = 2\) and leave \(\beta \) as a parameter for the optimisation phase (see Sect. 2 for more details). Despite this choice, our approach was able to derive bounds that match and improve the previous results, which came as a surprise to us. Looking back at our experiments and interpreting the obtained results, we recognise that we might have been in luck with the particular choice of the potential function (because we can obtain the previous results despite fixing \(\alpha = 2\)). However, we would not have expected that an automated analysis is able to match and improve all previously reported coefficients, which shows the power of the optimisation phase. Thus, we believe that our results suggest a new approach for the complexity analysis of data structures. So far, self-adjusting data structures had to be analysed manually. This is possibly due to the use of sophisticated potential functions, which may contain logarithmic expressions. Both features are challenging for automated reasoning. Our results suggest that the following alternative (see Sects. 2 and 4.2 for more details): (i) Fix a parameterised potential function; (ii) derive a (linear) constraint system over the function parameters from the AST of the program; (iii) capture the required non-linear reasoning in lemmata, and use Farkas’ lemma to integrate the application of these lemmata into the constraint system (in our case two lemmata, one about an arithmetic property and one about the monotonicity of the logarithm, were sufficient for all of our benchmarks); and finally (iv) find values for the parameters by an (optimising) constraint solver. We believe that our approach will carry over to other data structures: one needs to adapt the potential functions and add suitable lemmata, but the overall setup will be the same. We compare the proposed methodology to program synthesis by sketching [48], where the synthesis engineer communicates her main insights to the synthesis engine (in our case the potential functions plus suitable lemmata), and a constraint solver then fills in the details. As conclusion from our benchmarking, we observe that an automated analysis of sophisticated data structures are possible without the need to (i) resort to user guidance; (ii) forfeit optimal results; or (iii) be bogged down in computation times. These results also show how dependencies on properties of functional correctness of the code can be circumvented.

Related Work. To the best of our knowledge the here presented automated amortised analysis of self-adjusting data-structures is novel and unparalleled in the literature. However, there is a vast amount of literature on (automated) resource analysis. Without hope for a completeness, we briefly mention [1‐7, 9‐11, 14, 15, 17, 18, 20, 22‐25, 39, 44‐46, 52] for an overview of the field. Logarithmic and sublinear bounds are typically not in the focus of the cited approaches, but can be inferred by some tools. In the recurrence relations based approach to cost analysis [1] refinements of linear ranking functions are combined with criteria for divide-and-conquer patterns; this allows the tool PUBS to recognise logarithmic bounds for some problems, but examples such as mergesort or splaying are beyond the scope of this approach. Logarithmic and exponential terms are integrated into the synthesis of ranking functions in [8], making use of an insightful adaption of Farkas’ and Handelman’s lemmas. The approach is able to handle examples such as mergesort, but again not suitable to handle self-balancing data structures. A type based approach to cost analysis for an ML-like language is presented in [50], which uses the Master Theorem to handle divide-and-conquer-like recurrences. Recently, support for the Master Theorem was also integrated for the analysis of rewriting systems [51], extending [4] on the modular resource analysis of rewriting to so-called logically constrained rewriting systems [12]. The resulting approach also supports the fully automated analysis of mergesort.

Structure. In Sects. 2 and 3 we review the type system of [26, 27]. We sketch the challenges to automation in Sect. 4 and present our contributions in Sects. 5 and 6. Finally, we conclude in Sect. 7.

In this and the next section we sketch the theory developed by Hofmann et al. in [27], in order to be able to present the contributions of this article in Sect. 4 and 5. For brevity, we restrict our exposition to those parts essential in the analysis of a particular program code. As motivating example consider splay trees, introduced by Sleator and Tarjan [47, 49]. Splaying is the most important operation on splay trees, which performs rotation. Consider Fig. 1, a depiction of the zig-zig case of , which implements splaying.

The analysis of [27] (see also [26]) is formulated in terms of the physicist’s method of amortised analysis in the style of Sleator and Tarjan [47, 49]. The central idea of this approach is to assign a potential to the data structures of interest such that the difference in potential before and after executing a function is sufficient to pay for the actual cost of the function, i.e. one chooses potential functions \(\phi ,\psi \) such that \(\phi (v) \geqslant c_f(v) + \psi (f(v))\) holds for all inputs v to a function f, where \(c_f(v)\) denotes the worst-case cost of executing function f on v. This generalises the original formulation, which can be seen by setting , where \(a_f(v)\) denotes the amortised cost of f.

In order to be able to analyse self-adjusting data structures such as splay trees, one needs potential functions that can express logarithmic amortised cost. Hofmann et al. [26, 27] propose to make use of a variant of Schoenmakers’ potential, \(\mathsf {rk}(t)\) for a tree t, cf. [37, 41, 42], defined inductively by

where l, r are the left resp. right child of the tree , denotes the size of a tree (defined as the number of leaves of the tree), and d is some data element that is ignored by the potential function. Besides Schoenmakers’ potential, further basic potential functions need to be added to the analysis: For a sequence of m trees and coefficients \(a_i,b \in {\mathbb {N}}\), the potential functiondenotes the logarithm of a linear combination of the sizes of the tree.

Following [37], we set the cost of splaying a tree t to be the number of recursive calls to . Splaying and all operations that depend on splaying can be done in \(O(\log _2 n)\) amortised cost. Employing the above introduced potential functions, the analysis of [27] is able verify the following cost annotation for splaying (the annotation needs to be provided by the user):From this result, one directly reads off as bound on the amortised cost of splaying.²

Based on earlier work [6, 20, 22‐25, 27, 28] employs a type-and-effect system that uses template potential functions, i.e. functions of a fixed shape with indeterminate coefficients. The key challenge is to identify templates that are suitable for logarithmic analysis and that are closed under the basic operations of the considered programming language. For example, one introduces the coefficients \(q_*,q_{(1,0)},q_{(0,2)},q'_*,q'_{(1,0)},q'_{(0,2)}\) and introduces the potential function templates

for the input and output of the splay function. The type system then derives constraints on the template function coefficients, as indicated in the sequel. We take up further discussion of the constraint system, in particular how to maintain a scalable analysis, in Sect. 4.

We explain the use of the type system on the motivating example. For brevity, type judgements and the type rules are presented in a simplified form. In particular, we restrict our attention to tree types, denoted as \(\mathsf {T}\). This omission is inessential to the actual complexity analysis. For the full set of rules see [27].

Let e denote the body of the function definition of , depicted in Fig. 1. Our automated analysis infers an annotated type of splaying, by verifying that the type judgementis derivable. As above, types are decorated with annotations and  —employed to express the potential carried by the arguments to and its results.

The soundness theorem of the type system (Theorem 1) expresses that if the above type judgement is derivable, then the total cost of splaying is bound by the difference between and , i.e. . In particular, Eq. 1 can be derived in this way.

We now provide an intuition on the type-and-effect system, stepping through the code of Fig. 1. The corresponding type derivation tree is depicted in Fig. 2. We note that the tree contains further annotations \(Q_1,Q_2,Q_3,Q_4\) (besides the annotations Q and \(Q'\)) which again represent the unknown coefficients of potential function templates. The goal of the type-and-effect system is to provide constraints for each programming construct that connect the annotations in subsequent derivation steps, e.g. \(Q_2\) and \(Q_3\). The type-and-effect system operates syntax-directed and formulates one rule per programming languages construct. We now discuss some of these rules for the partial derivation for .

The outermost command of e is a statement, for which the following rule is applied:

Here \(e_1\) denotes the subexpression of e, which constitutes the nested pattern match. Primarily, this is a standard type rule for pattern matching. The novelty are the constraints on the annotations Q, \(Q'\) and \(Q_1\). More precisely, \((\mathsf {{match}})\) induces the constraintswhich can be directly read-off the definition of . Similarly, the nested command, starting expression \(e'_1\), is subject to the same rule; the resulting constraints amount toBesides the rules for programming language constructs, the type-and-effect system contains structural rules, which operate on the type annotations themselves. The weakening rule allows a suitable adaptation of the coefficients of the potential function \(\varPhi ({\varGamma } {\mid } {Q_2})\) to obtain a new potential function \(\varPhi ({\varGamma } {\mid } {Q_3})\), where we use the shorthand :

The difficulty in applying the weakening rule, consists in discharging the constraint:Note, that the comparison is to be performed symbolically, that is, abstracted from the concrete value of the variables. We emphasise that this step can neither be avoided, nor easily moved to the axioms of the derivation, as in related approaches in the literature [19, 21‐23, 28, 31, 35]. We use Farkas’ Lemma in conjunction with two facts about the logarithm to linearise this symbolic comparison, namely the monotonicity of the logarithm and the fact that \(2 + \log _2(x) + \log _2(y) \leqslant 2\log _2(x+y)\) for all \(x,y \geqslant 1\). For example, for the facts and , we use Farkas’ Lemma to generate the constraints

for some coefficients \(f,g \geqslant 0\) introduced by Farkas’ Lemma. We note that Farkas’ Lemma can be interpreted as systematically exploring all positive-linear combinations of the considered mathematical facts. This can be seen on the above example: one can combine g times the first fact with f times the second fact.

Next, we apply the rule for the  expression. This rule is the most involved typing rule in the system proposed by Hofmann et al. [27].

Ignoring the annotations and in particular the second premise for a moment, the type rule specifies a standard typing for a  expression. We note that, as required by the rule, all variables in the type context \(\varGamma \) occur at most once in the let-expression. \(\varGamma \) can then be split into contexts and . Here, and \(e_3\) denotes the last statement in e. The let-rule facilitates a splitting of the potential \(Q_3\) for the evaluation of \(e_2\) and \(e_3\) according to the type contexts \(\varDelta \) and \(\varTheta \). Abusing notation, the distribution of potentials facilitated by the let-rule can be stated very roughly as two “equalities”, that is, (i) “\(Q_3 = Q + R + P\)” and (ii) “\(Q_4 = (Q'-1) + R' + P\)”. (i) states that the potential \(Q_3\) pays for evaluating the  expression \(e_2\) (with and without costs, requiring the potential Q and R) and leaves the remainder potential P. (ii) states that the potential \(Q_4\) is constituted of the remainder potential P and of the potentials left after evaluating \(e_2\) (with and without costs, i.e. potentials \(Q'-1\) and \(R'\)). E.g. \(Q_4\) is given by the following constraints

where the coefficients \(q^3\) stem from the remainder potential of \(Q_3\), the coefficient \(q'_*\) from \(Q'-1\) and \({r'}_{(1,0)}\) from \(R'\).

The most original part of this type rule is the second premise . Here, \(\vdash ^{\text {cf}}\) denotes the same kind of typing judgement as used in the overall typing derivation, but where all costs are set to zero (hence, the superscript cost-free). Let us assume \(R=[{r}_{(1,0)}]\), \(R'=[{r'}_{(1,0)}]\), and that \(\mathsf {ATLAS}\) was able to establish thatestablishing the coefficients \({r}_{(1,0)} = 1\) and \({r'}_{(1,0)} =1\). (We note that cost-free typing derivations as in Eq. (4) constitute a size analysis that relates the sizes of input and output). Then, \(\mathsf {ATLAS}\) infers from (4), taking advantage of the monotonicity of \(\log \), thatThis inequality expresses that if the summand is included in the potential \(\varPhi ({\varGamma } {\mid } {Q_3})\), then the summand may be included in the potential \(\varPhi ({{cr}{:}\!{\mathsf {T}},{br}{:}\!{\mathsf {T}},{s}{:}\!{\mathsf {T}}} {\mid } {Q_4})\). (The two logarithmic terms correspond to the coefficients \(q^3_{(1,1,1,0)}\) and \(q^4_{(1,1,1,0)}\) marked in red above.) Thus, the cost-free derivation allows the potential R to pass from \(Q_3\), via \(R'\), to \(Q_4\). This is crucial for being able to pay for the evaluation of \(e_3\).

The let-rule has the three premises \({\varDelta } {\mid } {Q} \vdash {e_2}{:}\!{\mathsf {T}} {\mid } {Q'-1}\), \({\varDelta } {\mid } {R} \vdash ^{\text {cf}} {e_2}{:}\!{\mathsf {T}} {\mid } {R'}\) and \({\varTheta } {\mid } {Q_4} \vdash {e_3}{:}\!{\mathsf {T}} {\mid } {Q'}\). We focus here on the first premise and do not state the derivations for the other two premises (such derivations can be found in [27]). The judgement can be derived by the rule for function application, which states a cost of 1 with regard to the type signature of , represented by decrementing the potential induced by the annotation \(Q'\).

The rule for function application is an axiom, and closes this branch of the typing derivation. This concludes the presentation of the partial type inference given in Fig. 2. Similarly to the above example of , estimates for the amortised costs of insertion and deletion on splay trees can be automatically inferred by our tool \(\mathsf {ATLAS}\). Further, our analysis handles similar self-adjusting data structures like pairing heaps and splay heaps (see Sect. 6.1).

In this short section, we provide a more detailed account of the formal system underlying our tool \(\mathsf {ATLAS}\). We state the soundness of the system in Theorem 1.

A typing context is a mapping from variables \(\mathcal {V}\) to types; denoted by upper-case Greek letters. A program \(\mathsf {P}\) is a set of typed function definitions of the form , where the \(x_i\) are variables and e an expression. A substitution (or an environment) \(\sigma \) is a mapping from variables to values that respects types. Substitutions are denoted as sets of assignments: . We employ a simple cost-sensitive big-step semantics based on eager evaluation, dressed up with cost assertions. The judgement means that under environment \(\sigma \), expression e is evaluated to value v in exactly \(\ell \) steps. Here only rule applications emit (unit) costs. For brevity, the formal definition of the semantics is omitted but can be found in [27].

In Sect. 2, we introduced a variant of Schoenmakers’ potential function, denoted as \(\mathsf {rk}(t)\), and the additional potential functions , denoting the \(\log _2\) of a linear combination of tree sizes. \(\log _2\) denotes the logarithm to the base 2; throughout the paper we stipulate \(\log _2(0) := 0\) in order to avoid case distinctions. Note that the constant function 1 is representable: . We are now ready to state the resource annotation of a sequence of trees:

In case of an annotation of length 1, we sometimes write \(q_*\) instead of \(q_1\), as we already did above.

Let \(\sigma \) be a substitution, let \(\varGamma \) denote a typing context and let denote all tree types in \(\varGamma \). A resource annotation for \(\varGamma \) or simply annotation is an annotation for the sequence of trees . We define the potential of the annotated context \(\varGamma {\mid } Q\) wrt. a substitution \(\sigma \) as .

Instead of , we sometimes succinctly write . The cost-free signature, denoted as \(\mathcal {F}^{\text {cf}}\), is similarly defined.

Let \(Q = [q_*] \cup [(q_{(a,b)})_{a,b \in {\mathbb {N}}}]\) be an annotation such that \(q_{(a,b)} > 0\). Then is defined as follows: \(Q' = [q_*] \cup [(q'_{(a,b)})_{a,b \in {\mathbb {N}}}]\), where and for all \((a,b) \not = (0,2)\) . By definition the annotation coefficient \(q_{(0,2)}\) is the coefficient of the basic potential function , so the annotation \(Q-1\), decrements cost 1 from the potential induced by Q.

Type-and-Effect System. The typing system makes use of a cost-free semantics, which does not attribute any costs to the calculation. I.e. the rule \((\mathsf {{app}})\) (Sect. 2) is changed so that no cost is emitted. The cost-free application rule is denoted as \((\mathsf {{app:cf}})\). The cost-free typing judgement is written as \({\varGamma } {\mid } {Q} \vdash ^{\text {cf}} {e}{:}\!{\alpha } {\mid } {Q'}\). The judgement \({\varGamma } {\mid } {Q} \vdash {e}{:}\!{\alpha } {\mid } {Q'}\) is governed by a plethora of typing rules. We have illustrated several typing rules in Sect. 2 (the complete set of typing rules can be found in [27]).

A program \(\mathsf {P}\) is called well-typed if for any rule and any annotated signature , we have \({{x_1}{:}\!{\alpha _1},\dots ,{x_k}{:}\!{\alpha _k}} {\mid } {Q} \vdash {e}{:}\!{\beta } {\mid } {Q'}\). A program \(\mathsf {P}\) is called cost-free well-typed, if the cost-free typing relation is employed.

Hofmann et al. establish the following soundness result:³

The above sketched type-and-effect system, originally proposed in [27], is only a first step towards full automation. Several challenges need to be overcome, which we detail in this section.

In this section, we present our tool \(\mathsf {ATLAS}\), which implements type inference for the type system presented in Sects. 2 and 3. \(\mathsf {ATLAS}\) operates in three phases:

In terms of overall resource requirements, the bottleneck of the system is phase three. Preprocessing is both simple and fast. While the code implementing constraint generation might be complex, its execution is fast. All of the underlying complexity is shifted into the third phase. On modern machines with multiple gibibytes of main memory, \(\mathsf {ATLAS}\) is constrained by the CPU, and not by the available memory. In the remainder of this section, we first detail these phases of \(\mathsf {ATLAS}\). We then go into more details of the second phase. Finally, we elaborate the optimisation function which is the key enabler of type inference.

We first describe the benchmark functions employed to evaluate \(\mathsf {ATLAS}\) and then detail this experimental evaluation, already depicted in Table 1.

In this paper we have for the first time been able to automatically conduct an amortised analysis for self-adjusting data structures. Our analysis is based on the “sum of logarithms” potential function and we have been able to automate reasoning about these potential functions by using Farkas’ Lemma for the linear part of the calculations and adding necessary facts about the logarithm. Immediate future work is concerned with replacing the “sum of logarithms” potential function in order to analyse skew heaps and Fibonacci heaps [42]. In particular, the potential function for skew heaps, which counts “right heavy” nodes, is interesting, because it is also used as a building block by Iacono in his improved analysis of pairing heaps [29, 30]. Further, we envision to extend our analysis to related probabilistic settings such as priority queues [13] and skip lists [40].