An Order Theory Framework of Recurrence Equations for Static Cost Analysis $-$ Dynamic Inference of Non-Linear Inequality Invariants

TL;DR

This work addresses the challenge of inferring tight, non-linear bounds for complex recurrence relations arising in static cost analysis. It introduces an order-theoretical framework that treats recurrences as monotone operators, whose solutions are fixpoints, enabling bound-search via pre/postfixpoints and enabling principled algorithms. A proof-of-concept instantiation combines dynamic invariant generation with constrained optimization (affine templates and quadratic programming) to produce tight bounds that outperform several existing solvers on diverse benchmarks, including non-linear and multi-phase recurrences. The approach also connects to abstract interpretation and Galois connections, outlining avenues to extend beyond monotone cases and integrate with fine-grained cost models and size analyses.

Abstract

Recurrence equations have played a central role in static cost analysis, where they can be viewed as abstractions of programs and used to infer resource usage information without actually running the programs with concrete data. Such information is typically represented as functions of input data sizes. More generally, recurrence equations have been increasingly used to automatically obtain non-linear numerical invariants. However, state-of-the-art recurrence solvers and cost analysers suffer from serious limitations when dealing with the (complex) features of recurrences arising from cost analyses. We address this challenge by developing a novel order-theoretical framework where recurrences are viewed as operators and their solutions as fixpoints, which allows leveraging powerful pre/postfixpoint search techniques. We prove useful properties and provide principles and insights that enable us to develop techniques and combine them to design new solvers. We have also implemented and experimentally evaluated an optimisation-based instantiation of the proposed approach. The results are quite promising: our prototype outperforms state-of-the-art cost analysers and recurrence solvers, and can infer tight non-linear lower/upper bounds, in a reasonable time, for complex recurrences representing diverse program behaviours.

Figures (2)

• Figure 1: Candidate and operator dynamics. The operator $\mathrm{\rawPhi}$ of a program computing the gcd interacts with a candidate upper bound $\hat{f}(x,y)=x+y$. Plots represent the solution $f_{sol}$ (black), $\hat{f}$ (blue left), $\mathrm{\rawPhi}\hat{f}$ (red left, blue right), and $\mathrm{\rawPhi}^2\hat{f}$ (red right). We observe that $\mathrm{\rawPhi}\hat{f} \leq\hat{f}$, which is enough to prove that $\hat{f}$ is an upper bound on $f_{sol}$. Iterates $\mathrm{\rawPhi}^k\hat{f}$ progressively get closer to $f_{sol}$, but have more complex expressions.
• Figure 2: A grammar of operators to construct equations. All constructors presented here preserve monotonicity of equations. Note that no assumptions are made on $P$ and $\phi$ in (Base-Case) and (Rec-Call), which form the base cases for structural induction. (Sum) and (Scale) allow analysing programs with non-linear recursion. (Choice) corresponds to (restricted) conditional choice, and enables piecewise definitions. (Comp) is convenient for combining equations. Finally, (Max) and (Min) give simple ways to analyse worst- and best-cases in branching programs.

Theorems & Definitions (28)

• definition thmcounterdefinition
• definition thmcounterdefinition: Prefixpoints and postfixpoints
• definition thmcounterdefinition
• theorem thmcountertheorem: Knaster-Tarski, Knaster28Tarski55
• definition thmcounterdefinition: Monotone equation
• proposition thmcounterproposition
• proof
• theorem thmcountertheorem
• remark thmcounterremark
• definition thmcounterdefinition: Inductive bounds