SPEED: precise and efficient static estimation of program computational complexity

ABSTRACT

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.

REFERENCES

• 1: 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
• 2: D. Beyer, T. Henzinger, R. Majumdar, and A. Rybalchenko. Invariant synthesis for combined theories. In VMCAI'07, pages 378--394.
• 3: A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, and T. Vojnar. Programs with lists are counter automata. In CAV, 2006.
• 4: A. R. Bradley, Z. Manna, and H. B. Sipma. The polyranking principle. In ICALP, pages 1349--1361, 2005.
• 5: Aaron R. Bradley , Zohar Manna , Henny B. Sipma, Termination analysis of integer linear loops, CONCUR 2005 - Concurrency Theory, Springer-Verlag, London, 2005 [doi>10.1007/11539452_37]
• 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: Nils Anders Danielsson, Lightweight semiformal time complexity analysis for purely functional data structures, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 10: Nurit Dor , Michael Rodeh , Mooly Sagiv, CSSV: towards a realistic tool for statically detecting all buffer overflows in C, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 11: 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]
• 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: S. Gulwani, krishna Mehra, and T. Chilimbi. Speed: Precise and efficient static estimation of program computational complexity. Technical Report MSR-TR-2008-95, Microsoft Research, 2008.
• 14: Sumit Gulwani , Tal Lev-Ami , Mooly Sagiv, A combination framework for tracking partition sizes, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
• 15: S. Gulwani and G. C. Necula. A Polynomial-Time Algorithm for Global Value Numbering. In SAS, pages 212--227, 2004.
• 16: Sumit Gulwani , Ashish Tiwari, Combining abstract interpreters, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 17: 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]
• 18: 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]
• 19: 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]
• 20: Martin Hofmann , Steffen Jost, Static prediction of heap space usage for first-order functional programs, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.185-197, January 15-17, 2003, New Orleans, Louisiana, USA
• 21: John Hughes , Lars Pareto, Recursion and dynamic data-structures in bounded space: towards embedded ML programming, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.70-81, September 27-29, 1999, Paris, France
• 22: K. R. M. Leino and P. Müller. Object invariants in dynamic contexts. In ECOOP, volume 3086 of LNCS, pages 491--516, 2004.
• 23: S. Magill, J. Berdine, E. M. Clarke, and B. Cook. Arithmetic strengthening for shape analysis. In SAS, pages 419--436, 2007.
• 24: Daniel Le Métayer, ACE: an automatic complexity evaluator, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.2, p.248-266, April 1988 [doi>10.1145/42190.42347]
• 25: J. Navas, E. Mera, P. López-Garcıa, and M. V. Hermenegildo. User-definable resource bounds analysis for logic programs. In ICLP, pages 348--363, 2007.
• 26: Microsoft Phoenix Compiler Infrastructure, http://research.microsoft.com/phoenix/.
• 27: 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]
• 28: Mads Rosendahl, Automatic complexity analysis, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.144-156, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99381]
• 29: 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]
• 30: Reinhard Wilhelm , Björn Wachter, Abstract Interpretation with Applications to Timing Validation, 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_6]

INDEX TERMS

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

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

General Terms:
Performance, Verification

Keywords:
counter instrumentation, quantitative functions, symbolic complexity bounds, termination analysis