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

TL;DR

This paper introduces a new order-theoretical framework for solving complex recurrence equations in static cost analysis, enabling more accurate inference of non-linear resource bounds with improved solver performance.

Contribution

It develops a novel framework viewing recurrences as operators and solutions as fixpoints, enhancing the ability to infer non-linear invariants in cost analysis.

Findings

Prototype outperforms existing cost analyzers and solvers.

Successfully infers tight non-linear bounds for complex recurrences.

Handles diverse program behaviors efficiently.

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.