SPEED Symbolic Resource (e.g., Time, Space) Bounds Analysis

Introduction

Performance measurement of software is a critical component of software development. Performance is traditionally measured using profiling, which is often too little (only certain inputs are profiled) or too late (to make requisite changes to address the root cause before shipping). The SPEED project attempts to address these limitations by static estimation of symbolic computational complexity of programs. It builds over recent advances in static program analysis, which has traditionally been used for checking correctness as opposed to measuring performance.

Computing symbolic complexity bounds is a challenging problem since such bounds for even simple sequential programs are usually disjunctive, non-linear, and involve numerical properties of heaps. Sometimes even proving termination is hard (Remember halting problem is undecidable!), and computing bounds ought to be a harder problem. The SPEED tool implements several algorithmic techniques for statically estimating the worst-case symbolic computational complexity of procedures in terms of their scalar inputs and user-defined quantitative functions of input data-structures (such as length of a list, or height of a tree). It attempts to generate complexity bounds that are usually precise not only in terms of the computational complexity, but also in terms of the constant factors.

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.

Selected Talks

• The Reachability-Bound Problem [ppt], Invited Talk at FOPARA 2009
• Art of Invariant Generation applied to Symbolic Bound Computation [Lecture 1, Lecture 2, Lecture 3], Lectures at Oregon Summer School 2009 (Extended version of CAV 2009 talk below)
• The Art of Invariant Generation for Symbolic Loop Bound Analysis [ppt], Invited Talk at CAV 2009

• Bound Analysis of Imperative Programs with the Size-change Abstraction, SAS 2011, Florian Zuleger, Moritz Sinn, Sumit Gulwani and Helmut Veith [abstract |pdf]
• The Reachability Bound Problem , PLDI 2010, Sumit Gulwani, Florian Zuleger [abstract |ps |pdf ]
  Reachability bound problem is defined to be the problem of computing a worst-case symbolic bound on the number of times a given control location is visited inside a procedure. The paper presents an algorithm for the reachability bound problem. The algorithm is based on a variety of fixed-point computation techniques (namely abstract interpretation, contraint based, and proof-rule based). As part of this algorithm, this paper also describes a novel abstract-interpretation based algorithm for computing disjunctive invariants.
• SPEED: Symbolic Complexity Bound Analysis , Invited Talk Paper, CAV 2009, Sumit Gulwani, [abstract |ps |pdf ]
  This invited talk paper gives a brief summary of the key technical results developed in the SPEED project.
• Control-Flow Refinement and Progress Invariants for Bound Analysis , PLDI 2009, Sumit Gulwani, Sagar Jain, and Eric Koskinen, [abstract |ps |pdf ]
  This paper describes two orthogonal techniques for bound computation: (i) A program transformation that transforms a loop with complicated control-flow into a (semantically equivalent and bound-preserving) code-fragment with simpler loops whose bound can be computed using simple techniques such as those based on pattern matching. (ii) The notion of progress invariants that characterize relationships between successive program states that arise at a given program location; these invariants are used to compute precise amortized bounds, especially for nested loops.
• SPEED: Precise and Efficient Static Estimation of Program Computational Complexity, POPL 2009, Sumit Gulwani, Krishna Mehra, and Trishul Chilimbi, [abstract |pdf |ps |ppt slides]
  This paper describes two orthogonal techniques for bound computation: (i) A proof methodology based on multiple counter instrumentation that allows use of off-the-shelf numerical invariant generation tools to compute bounds. (ii) The notion of user-defined quantitative functions for data-structures, which are useful to express bounds of procedures that iterate over data-structures.
  • Full version appears as Microsoft Technical Report, MSR-TR-2008-95 [ps |pdf]
• A Combination Framework for Tracking Partition Sizes, POPL 2009, Sumit Gulwani, Tal Lev-Ami, and Mooly Sagiv, [abstract |ps |pdf |ppt slides]
  This paper describes an abstract-interpretation based invariant generation tool for computing numerical invariants over sizes of memory partitions - Such an abstract domain can be used to compute invariants required for say proving upper bounds on an implementation of bubblesort routine.
  • Full version appears as Microsoft Technical Report, TR-2008-158 [ps |pdf]
• A Numerical Abstract Domain based on "Expression Abstraction" and "Max Operator" with Application in Timing Analysis, CAV 2008, Bhargav Gulavani and Sumit Gulwani, [abstract |pdf |ppt slides]
  This paper describes an abstract-interpretation based invariant generation tool for computing numerical invariants involving operators such as logarithm and exponentiation - these invariants are useful for proving upper bounds on procedures like binary search, and Fibonacci respectively.

• Trishul Chilimbi (MSR Redmond)
• Bhargav Gulavani (IIT Bombay)
• Sumit Gulwani (MSR Redmond)
• Sagar Jain (UC Berkeley)
• Eric Koskinen (University of Cambridge)
• Florian Zuleger (TU Darmstadt)