Control-flow Refinement and Progress Invariants for Bound Analysis

Sumit Gulwani and Eric Koskinen

Abstract

Symbolic complexity bounds help programmers understand the

performance characteristics of their implementations. Existing work

provides techniques for statically determining bounds of procedures

with only 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 each of the above techniques go 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 also discuss applications of

progress invariants to proving fair termination.

We have applied our methodology to 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.

Details

Publication typeTechReport
NumberMSR-TR-2009-32
> Publications > Control-flow Refinement and Progress Invariants for Bound Analysis