be converted into questions of fair termination—termination proving were
certain non-terminating executions
are deemed unfair via given fairness
constraints, and thus ignored. Current tools, in fact, either perform this
reduction, or simply require the user to
express liveness constraints directly as
the set of fairness constraints. 12, 29 Neither approach is optimal: the reduction from liveness to fairness is inefficient in the size of the conversion, and
fairness constraints are difficult for
humans to understand when used directly. An avenue for future work would
be to directly prove liveness properties,
perhaps as an adaption of existing termination proving techniques.
Dynamic analysis and crash dumps
for liveness bugs. In this article we have
focused only on static, or compile-time,
proof techniques rather than techniques for diagnosing divergence during execution. Some effort has been
placed into the area of automatically
detecting deadlock during execution
time. With new developments in the
area of program termination proving
we might find that automatic methods
of discovering livelock could also now
be possible. Temporary modifications
to scheduling, or other techniques,
might also be employed to help programs not diverge even in cases where
they do not guarantee termination or
other liveness properties. Some preliminary work has begun to emerge
in this area (see Jula et al. 23) but more
work is needed.
Scalability, performance, and precision. Scalability to large and complex
programs is currently a problem for
modern termination provers—
current techniques are known, at best, to
scale to simple systems code of 30,000
lines of code. Another problem we face
is one of precision. Some small programs currently cannot be proved terminating with existing tools. Turing’s
undecidability result, of course, states
that this will always be true, but this
does preclude us from improving precision for various classes of programs
and concrete examples. The most famous example is that of the Collatz’
problem, which amounts to proving
the termination or non-termination
of the program in Figure 11. Currently
no proof of this program’s termination
behavior is known.
Conclusion
This article has surveyed recent advances in program termination proving techniques for sequential programs, and pointed toward ongoing
work and potential areas for future
development. The hope of many tool
builders in this area is that the current
and future termination proving techniques will become generally available for developers wishing to directly
prove termination or liveness. We also
hope that termination-related applications—such as detecting livelock at
runtime or Wang’s tiling problem—
will also benefit from these advances.
acknowledgments
The authors would like to thank Lucas Bourdeaux, Abigail See, Tim Harris, Ralf Herbrich, Peter O’Hearn, and
Hongseok Yang for their reading of
early drafts of this article and suggestions for improvement.
References
1. Babic, D., Hu, a. J., rakamaric, Z., and Cook, B. Proving
termination by divergence. In SEFM, 2007.
2. Ball, T., Bounimova, e., Cook, B., levin, V., lichtenberg,
J., McGarvey, C., ondrusek, B., rajamani, S.K. and
ustuner, a. Thorough static analysis of device drivers.
In Proceedings of EuroSys, 2006.
3. Berdine, J., Chawdhary, a., Cook, B., Distefano, D.
and o’Hearn, P. Variance analyses from invariance
analyses. In Proceedings of POPL, 2007.
4. Berdine, J., Cook, B., Distefano, D. and o’Hearn, P.
automatic termination proofs for programs with
shape-shifting heaps. In Proceedings of CAV, 2006.
5. Bouajjani, a., Bozga, M., Habermehl, P., Iosif, r., Moro,
P. and Vojnar, T. Programs with lists are counter
automata. In Proceedings of CAV, 2006.
6. Bradley, a., Manna, Z. and Sipma, H. Termination of
polynomial programs. In Proceedings of VMCAI, 2005.
7. Bradley, a., Manna, Z. and Sipma, H. B. linear ranking
with reachability. In Proceedings of CAV, 2005.
8. Bradley, a., Manna, Z. and Sipma, H. B. The polyranking
principle. In Proceedings of ICALP, 2005.
9. Chawdhary, C., Cook, B., Gulwani, S., Sagiv, M. and
yang, H. ranking abstractions. In Proceedings of
ESOP, 2008.
10. Codish, M., Genaim, S., Bruynooghe, M., Gallagher, J.
and Vanhoof, W. one loop at a time. In Proceedings of
WS T, 2003.
11. Colón, M. and Sipma, H. Synthesis of linear ranking
functions. In Proceedings of TACAS, 2001.
12. Cook, B., Gotsman, a., Podelski, a., rybalchenko, a.
and Vardi, M. Proving that programs eventually do
something good. In Proceedings of POPL, 2007.
13. Cook, B., Gulwani, S., lev-ami, T., rybalchenko, a.
and Sagiv, M. Proving conditional termination. In
Proceedings of CAV, 2008.
14. Cook, B., Podelski, a. and rybalchenko, a. Termination
proofs for systems code. In Proceedings of PLDI, 2006.
15. Dershowitz, n., lindenstrauss, n., Sagiv, y. and
Serebrenik, a. a general framework for automatic
termination analysis of logic programs. Appl. Algebra
Eng. Commun. Comput., 2001.
16. Farkas, J. uber die Theorie der einfachen
ungleichungen. Journal für die reine und angewandte
Mathematik, 1902.
17. Geser, a. relative termination. PhD dissertation, 1990.
18. Giesl, J., Swiderski, S., Schneider-Kamp, P. and
Thiemann, r. automated termination analysis
for Haskell: From term rewriting to programming
languages. In Proceedings of R TA, 2006.
19. Giesl, J. Thiemann, r., Schneider-Kamp, P. and Falke,
S. automated termination proofs with aProVe. In
Proceedings of RTA, 2004.
20. Gotsman, a., Cook, B., Parkinson, M. and Vafeiadis, V.
Proving that non-blocking algorithms don’t block. In
Proceedings of POPL, 2009.
21. Gupta, a., Henzinger, T., Majumdar, r., rybalchenko, a.,
and Xu, r. Proving non-termination. In Proceedings of
POPL, 2008.
22. Jones, C.B. Tentative steps toward a development
method for interfering programs. ACM Trans. Program.
Lang. Syst., 1983.
23. Jula, H., Tralamazza, D., Zamfir, C. and Candea, G.
Deadlock immunity: enabling systems to defend
against deadlocks. In Proceedings of OSDI, 2008.
24. lee, C. S., Jones, n.D. and Ben-amram, a. M.. The
size-change principle for program termination. In
Proceedings of POPL, 2001.
25. Magill, S., Berdine, J., Clarke, e. and Cook, B.
arithmetic strengthening for shape analysis. In
Proceedings of SAS, 2007.
26. Manolios, P. and Vroon, D. Termination analysis with
calling context graphs. In Proceedings of CAV, 2006.
27. McMillan, K.l. Circular compositional reasoning about
liveness. In Proceedings of CHARME, 1999.
28. Misra, J and Chandy, K.M. Proofs of networks of
processes. IEEE Trans. Soft ware Eng., 1981.
29. Pnueli, a., Podelski, a., and rybalchenko, a. Separating
fairness and well-foundedness for the analysis of fair
discrete systems. In Proceedings of TACAS, 2005.
30. Podelski, a, and rybalchenko, a. a complete method
for the synthesis of linear ranking functions. In
Proceedings of VMCAI, 2004.
31. Podelski, a, and rybalchenko, a. Transition invariants.
In Proceedings of LICS, 2004.
32. Podelski, a. and rybalchenko, a. Transition predicate
abstraction and fair termination. In Proceedings of
POPL, 2005.
33. Podelski, a., rybalchenko, a., and Wies, T. Heap
assumptions on demand. In Proceedings of CAV, 2008.
34. ramsey, F. on a problem of formal logic. London Math.
Soc., 1930.
35. Stix, G. Send in the Terminator. Scientific American
(nov. 2006).
36. Strachey, C. an impossible program. Computer
Journal, 1965.
37. Tiwari, a. Termination of linear programs. In
Proceedings of CAV, 2004.
38. Turing, a. on computable numbers, with an application
to the entscheidungsproblem. London Mathematical
Society, 1936.
39. Turing, a. Checking a large routine. In report of a
Conference on High Speed automatic Calculating
Machines, 1949.
40. yang, H., lee, o., Berdine, J., Calcagno, C., Cook, B.,
Distefano, D. and o’Hearn, P. Scalable shape analysis
for systems code. In Proceedings of CAV, 2008.
Byron Cook is a Principal researcher at Microsoft’s
research laboratory at Cambridge university, and a
professor of computer science at Queen Mary, university
of london, england.
Andreas Podelski is a professor of computer science at
the university of Freiburg, Germany.
Andrey Rybalchenko is a professor of computer science
at the Technische universität München, Germany.