Control-flow refinement and progress invariants for bound analysis

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.

REFERENCES

• 1: Phoenix Compiler. research.microsoft.com/Phoenix/.
• 2: Z3 Theorem Prover. research.microsoft.com/projects/Z3/.
• 3: Elvira Albert , Puri Arenas , Samir Genaim , Germán Puebla, Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis, Proceedings of the 15th international symposium on Static Analysis, July 16-18, 2008, Valencia, Spain [doi>10.1007/978-3-540-69166-2_15]
• 4: Gogul Balakrishnan , Sriram Sankaranarayanan , Franjo Ivančić , Ou Wei , Aarti Gupta, SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement, Proceedings of the 15th international symposium on Static Analysis, July 16-18, 2008, Valencia, Spain [doi>10.1007/978-3-540-69166-2_16]
• 5: Josh Berdine , Aziem Chawdhary , Byron Cook , Dino Distefano , Peter O'Hearn, Variance analyses from invariance analyses, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 6: Byron Cook , Andreas Podelski , Andrey Rybalchenko, Termination proofs for systems code, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 7: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 8: Karl Crary , Stephnie Weirich, Resource bound certification, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.184-198, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325716]
• 9: Simon F. Goldsmith , Alex S. Aiken , Daniel S. Wilkerson, Measuring empirical computational complexity, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia [doi>10.1145/1287624.1287681]
• 10: Denis Gopan and Thomas W. Reps. Lookahead widening. In CAV, 2006.
• 11: Denis Gopan and Thomas W. Reps. Guided static analysis. In SAS, 2007.
• 12: Bhargav S. Gulavani , Sumit Gulwani, A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis, Proceedings of the 20th international conference on Computer Aided Verification, July 07-14, 2008, Princeton, NJ, USA [doi>10.1007/978-3-540-70545-1_35]
• 13: Bhargav S. Gulavani , Thomas A. Henzinger , Yamini Kannan , Aditya V. Nori , Sriram K. Rajamani, SYNERGY: a new algorithm for property checking, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA [doi>10.1145/1181775.1181790]
• 14: Sumit Gulwani , Nebojsa Jojic, Program verification as probabilistic inference, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 15: Sumit Gulwani , Krishna K. Mehra , Trishul Chilimbi, SPEED: precise and efficient static estimation of program computational complexity, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
• 16: Jan Gustafsson , Andreas Ermedahl , Christer Sandberg , Bjorn Lisper, Automatic Derivation of Loop Bounds and Infeasible Paths for WCET Analysis Using Abstract Execution, Proceedings of the 27th IEEE International Real-Time Systems Symposium, p.57-66, December 05-08, 2006 [doi>10.1109/RTSS.2006.12]
• 17: Nicolas Halbwachs , Yann-Erick Proy , Patrick Roumanoff, Verification of Real-Time Systems using Linear Relation Analysis, Formal Methods in System Design, v.11 n.2, p.157-185, Aug. 1997 [doi>10.1023/A:1008678014487]
• 18: Christopher Healy , Mikael Sjödin , Viresh Rustagi , David Whalley , Robert Van Engelen, Supporting Timing Analysis by Automatic Bounding of LoopIterations, Real-Time Systems, v.18 n.2/3, p.129-156, May 2000 [doi>10.1023/A:1008189014032]
• 19: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 20: Björn Lisper. Fully automatic, parametric worst--case execution time analysis. In WCET, 2003.
• 21: Ali Mili. Reflexive transitive loop invariants: A basis for computing loop functions. In WING, 2007.
• 22: Antoine Miné, The octagon abstract domain, Higher-Order and Symbolic Computation, v.19 n.1, p.31-100, March 2006 [doi>10.1007/s10990-006-8609-1]
• 23: A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. LNCS, 2003.
• 24: Andreas Podelski , Andrey Rybalchenko, Transition Invariants, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, p.32-41, July 13-17, 2004 [doi>10.1109/LICS.2004.50]
• 25: Sriram Sankaranarayanan, Franjo Ivancic, Ilya Shlyakhter, and Aarti Gupta. Static analysis in disjunctive numerical domains. In SAS, 2006.
• 26: Chao Wang, Zijiang Yang, Aarti Gupta, and Franjo Ivancic. Using counterexamples for improving the precision of reachability computation with polyhedra. In CAV, 2007.
• 27: Reinhard Wilhelm , Jakob Engblom , Andreas Ermedahl , Niklas Holsti , Stephan Thesing , David Whalley , Guillem Bernat , Christian Ferdinand , Reinhold Heckmann , Tulika Mitra , Frank Mueller , Isabelle Puaut , Peter Puschner , Jan Staschulat , Per Stenström, The worst-case execution-time problem—overview of methods and survey of tools, ACM Transactions on Embedded Computing Systems (TECS), v.7 n.3, p.1-53, April 2008 [doi>10.1145/1347375.1347389]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  C. Computer Systems Organization
  C.4 PERFORMANCE OF SYSTEMS
      Subjects: Measurement techniques; Reliability, availability, and serviceability

  D. Software
  D.4 OPERATING SYSTEMS
      D.4.8 Performance
          Subjects: Modeling and prediction

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Performance, Reliability, Verification

Keywords:
bound analysis, control-flow refinement, formal verification, program verification, progress invariants, termination