
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, nonlinear, 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 worstcase symbolic computational complexity of procedures in terms of their scalar inputs and userdefined quantitative functions of input datastructures (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 ReachabilityBound 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
Papers

Bound Analysis of Imperative Programs with the Sizechange 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 worstcase 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 fixedpoint computation techniques (namely abstract interpretation, contraint based, and proofrule based). As part of this algorithm, this paper also describes a novel abstractinterpretation 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.

ControlFlow 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 controlflow into a (semantically equivalent and boundpreserving) codefragment 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 offtheshelf numerical invariant generation tools to compute bounds. (ii) The notion of userdefined quantitative functions for datastructures, which are useful to express bounds of procedures that iterate over datastructures.

Full version appears as Microsoft Technical Report, MSRTR200895
[ps
pdf]

A Combination Framework for Tracking Partition Sizes, POPL 2009,
Sumit Gulwani, Tal LevAmi, and Mooly Sagiv,
[abstract
ps
pdf
ppt slides]
This paper describes an abstractinterpretation 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, TR2008158
[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 abstractinterpretation 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.
People Involved