TY - GEN
T1 - Control-flow refinement and progress invariants for bound analysis
AU - Gulwani, Sumit
AU - Jain, Sagar
AU - Koskinen, Eric
PY - 2009
Y1 - 2009
N2 - Symbolic complexity bounds help programmers understand the performance characteristics of their implementations. Existing work provides techniques for statically determining bounds of procedures with 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 seman-tically 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 these two techniques goes 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 have applied our methodology to over 670,000 lines of code of 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.
AB - Symbolic complexity bounds help programmers understand the performance characteristics of their implementations. Existing work provides techniques for statically determining bounds of procedures with 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 seman-tically 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 these two techniques goes 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 have applied our methodology to over 670,000 lines of code of 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.
KW - Bound analysis
KW - Control-flow refinement
KW - Formal verification
KW - Program verification
KW - Progress invariants
KW - Termination
UR - http://www.scopus.com/inward/record.url?scp=70450277235&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70450277235&partnerID=8YFLogxK
U2 - 10.1145/1542476.1542518
DO - 10.1145/1542476.1542518
M3 - Conference contribution
AN - SCOPUS:70450277235
SN - 9781605583921
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 375
EP - 385
BT - PLDI'09 - Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation
T2 - 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'09
Y2 - 15 June 2009 through 20 June 2009
ER -