Sumit Gulwani
Sagar Jain
Abstract
Symbolic complexity bounds help programmers understand the performance characteristics of their implementations. Existing work provides techniques for statically determining bounds of procedures with simple control-flow. However, procedures with nested loops or multiple paths through a single loop are challenging.
In this paper we describe two techniques, control-flow refinement and progress invariants, that together enable estimation of precise bounds for procedures with nested and multi-path loops. Control-flow refinement transforms a multi-path loop into a semantically equivalent code fragment with simpler loops by making the structure of path interleaving explicit. We show that this enables non-disjunctive invariant generation tools to find a bound on many procedures for which previous techniques were unable to prove termination. Progress invariants characterize relationships between consecutive states that can arise at a program location. We further present an algorithm that uses progress invariants to compute precise bounds for nested loops. The utility of these two techniques goes beyond our application to symbolic bound analysis. In particular, we discuss applications of control-flow refinement to proving safety properties that otherwise require disjunctive invariants.
We have applied our methodology to over 670,000 lines of code of a significant Microsoft product and were able to find symbolic bounds for 90% of the loops. We are not aware of any other published results that report experiences running a bound analysis on a real code-base.
- Phoenix Compiler. research.microsoft.com/Phoenix/.Google Scholar
- Z3 Theorem Prover. research.microsoft.com/projects/Z3/.Google Scholar
- Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. Automatic inference of upper bounds for recurrence relations in cost analysis. In SAS, 2008. Google ScholarDigital Library
- G. Balakrishnan, S. Sankaranarayanan, F. Ivancic, O. Wei, and A. Gupta. SLR: Path-sensitive analysis through infeasible-path detection and syntactic language refinement. Lecture Notes in Computer Science, 5079, 2008. Google ScholarDigital Library
- Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, and Peter W. O'Hearn. Variance analyses from invariance analyses. In POPL, 2007. Google ScholarDigital Library
- Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Termination proofs for systems code. In PLDI, 2006. Google ScholarDigital Library
- Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In POPL, 1978.\pagebreak Google ScholarDigital Library
- Karl Crary and Stephanie Weirich. Resource bound certification. In POPL, 2000. Google ScholarDigital Library
- Simon Goldsmith, Alex Aiken, and Daniel Shawcross Wilkerson. Measuring empirical computational complexity. In ESEC/SIGSOFT FSE, 2007. Google ScholarDigital Library
- Denis Gopan and Thomas W. Reps. Lookahead widening. In CAV, 2006. Google ScholarDigital Library
- Denis Gopan and Thomas W. Reps. Guided static analysis. In SAS, 2007. Google ScholarDigital Library
- Bhargav S. Gulavani and Sumit Gulwani. A numerical abstract domain based on expression abstraction and max operator with application in timing analysis. In CAV, 2008. Google ScholarDigital Library
- Bhargav S. Gulavani, Thomas A. Henzinger, Yamini Kannan, Aditya V. Nori, and Sriram K. Rajamani. SYNERGY: A new algorithm for property checking. In FSE, 2006. Google ScholarDigital Library
- Sumit Gulwani and Nebojsa Jojic. Program verification as probabilistic inference. In POPL, 2007. Google ScholarDigital Library
- Sumit Gulwani, Krishna Mehra, and Trishul Chilimbi. SPEED: Precise and efficient static estimation of program computational complexity. In POPL, 2009. Google ScholarDigital Library
- Jan Gustafsson, Andreas Ermedahl, Christer Sandberg, and Bjorn Lisper. Automatic derivation of loop bounds and infeasible paths for wcet analysis using abstract execution. In RTSS, 2006. Google ScholarDigital Library
- Nicolas Halbwachs, Yann-Erick Proy, and Patrick Roumanoff. Verification of real--time systems using linear relation analysis. FMSD, 1997. Google ScholarDigital Library
- Christopher A. Healy, Mikael Sjodin, Viresh Rustagi, David B. Whalley, and Robert van Engelen. Supporting timing analysis by automatic bounding of loop iterations. Real-Time Systems, 18(2/3), 2000. Google ScholarDigital Library
- Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Grégoire Sutre. Lazy abstraction. In POPL, 2002. Google ScholarDigital Library
- Björn Lisper. Fully automatic, parametric worst--case execution time analysis. In WCET, 2003.Google Scholar
- Ali Mili. Reflexive transitive loop invariants: A basis for computing loop functions. In WING, 2007.Google Scholar
- Antoine Miné. The Octagon Abstract Domain. Higher-Order and Symbolic Computation, 19(1), 2006. Google ScholarDigital Library
- A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. LNCS, 2003.Google Scholar
- A. Podelski and A. Rybalchenko. Transition invariants. In LICS, 2004. Google ScholarDigital Library
- Sriram Sankaranarayanan, Franjo Ivancic, Ilya Shlyakhter, and Aarti Gupta. Static analysis in disjunctive numerical domains. In SAS, 2006. Google ScholarDigital Library
- Chao Wang, Zijiang Yang, Aarti Gupta, and Franjo Ivancic. Using counterexamples for improving the precision of reachability computation with polyhedra. In CAV, 2007. Google ScholarDigital Library
- Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David Whalley, Guillem Bernat, Christian Ferdinand, Reinhold Heckmann, Frank Mueller, Isabelle Puaut, Peter Puschner, Jan Staschulat, and Per Stenström. The Determination of Worst-Case Execution Times-Overview of the Methods and Survey of Tools. In TECS, 2007. Google ScholarDigital Library
Index Terms
- Control-flow refinement and progress invariants for bound analysis
Recommendations
Path invariants
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and ImplementationThe success of software verification depends on the ability to find a suitable abstraction of a program automatically. We propose a method for automated abstraction refinement which overcomes some limitations of current predicate discovery schemes. In ...
Control-flow refinement and progress invariants for bound analysis
PLDI '09: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and ImplementationSymbolic complexity bounds help programmers understand the performance characteristics of their implementations. Existing work provides techniques for statically determining bounds of procedures with simple control-flow. However, procedures with nested ...
Temporal property verification as a program analysis task
We describe a reduction from temporal property verification to a program analysis problem. First we present a proof system that, unlike the standard formulation, is more amenable to reasoning about infinite-state systems: disjunction is treated by ...
Comments