SPEED: precise and efficient static estimation of program computational complexity. This paper describes an inter-procedural technique for computing symbolic bounds on the number of statements a procedure executes in terms of its scalar inputs and user-defined quantitative functions of input data-structures. Such computational complexity bounds for even simple programs are usually disjunctive, non-linear, and involve numerical properties of heaps. We address the challenges of generating these bounds using two novel ideas. We introduce a proof methodology based on multiple counter instrumentation (each counter can be initialized and incremented at potentially multiple program locations) that allows a given linear invariant generation tool to compute linear bounds individually on these counter variables. The bounds on these counters are then composed together to generate total bounds that are non-linear and disjunctive. We also give an algorithm for automating this proof methodology. Our algorithm generates complexity bounds that are usually precise not only in terms of the computational complexity, but also in terms of the constant factors. Next, we introduce the notion of user-defined quantitative functions that can be associated with abstract data-structures, e.g., length of a list, height of a tree, etc. We show how to compute bounds in terms of these quantitative functions using a linear invariant generation tool that has support for handling uninterpreted functions. We show application of this methodology to commonly used data-structures (namely lists, list of lists, trees, bit-vectors) using examples from Microsoft product code. We observe that a few quantitative functions for each data-structure are usually sufficient to allow generation of symbolic complexity bounds of a variety of loops that iterate over these data-structures, and that it is straightforward to define these quantitative functions. The combination of these techniques enables generation of precise computational complexity bounds for real-world examples (drawn from Microsoft product code and C++ STL library code) for some of which it is non-trivial to even prove termination. Such automatically generated bounds are very useful for early detection of egregious performance problems in large modular codebases that are constantly being changed by multiple developers who make heavy use of code written by others without a good understanding of their implementation complexity.
This software is also peer reviewed by journal TOMS.
This software is also peer reviewed by journal TOMS.
Keywords for this software
References in zbMATH (referenced in 25 articles )
Showing results 1 to 20 of 25.
- Hoffmann, Jan; Das, Ankush; Weng, Shu-Chun: Towards automatic resource bound analysis for OCaml (2017)
- Sinn, Moritz; Zuleger, Florian; Veith, Helmut: Complexity and resource bound analysis of imperative programs using difference constraints (2017)
- McCarthy, Jay; Fetscher, Burke; New, Max; Feltey, Daniel; Findler, Robert Bruce: A Coq library for internal verification of running-times (2016)
- Zanardini, Damiano; Albert, Elvira; Villela, Karina: Resource-usage-aware configuration in software product lines (2016)
- Albert, Elvira; Correas, Jesús; Puebla, Germán; Román-Díez, Guillermo: A multi-domain incremental analysis engine and its application to incremental resource analysis (2015)
- Alves, Péricles R.O.; Rodrigues, Raphael E.; de Sousa, Rafael Martins; Quintão Pereira, Fernando Magno: A case for a fast trip count predictor (2015) ioport
- Avanzini, Martin; Eguchi, Naohi; Moser, Georg: A new order-theoretic characterisation of the polytime computable functions (2015)
- Hainry, Emmanuel; Péchoux, Romain: Objects in polynomial time (2015)
- Johnsen, Einar Broch; Schlatte, Rudolf; Tapia Tarifa, S.Lizeth: Integrating deployment architectures and resource consumption in timed object-oriented models (2015)
- Bubel, Richard; Montoya, Antonio Flores; Hähnle, Reiner: Analysis of executable software models (2014)
- Avanzini, Martin; Moser, Georg: Polynomial path orders (2013)
- Hofmann, Martin; Rodriguez, Dulma: Automatic type inference for amortised heap-space analysis (2013)
- Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using state and transition invariants (2013)
- Mazzieri, I.; Stupazzini, M.; Guidotti, R.; Smerzini, C.: SPEED: spectral elements in elastodynamics with discontinuous Galerkin: a non-conforming approach for 3D multi-scale problems (2013)
- Albert, Elvira; Arenas, Puri; Genaim, Samir; Gómez-Zamalloa, Miguel; Puebla, Germán: Automatic inference of resource consumption bounds (2012)
- Maisonneuve, Vivien: Convex invariant refinement by control node splitting: a heuristic approach (2012)
- Albert, Elvira; Genaim, Samir; Masud, Abu Naser: More precise yet widely applicable cost analysis (2011)
- Alias, Christophe; Darte, Alain; Feautrier, Paul; Gonnord, Laure: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs (2010)
- Atkey, Robert: Amortised resource analysis with separation logic (2010)
- Dillig, Isil; Dillig, Thomas; Aiken, Alex: Fluid updates: beyond strong vs. weak updates (2010)