Sumit Gulwani and Eric Koskinen
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.