Proving thread termination

ABSTRACT

Concurrent programs are often designed such that certain functions executing within critical threads must terminate. Examples of such cases can be found in operating systems, web servers, e-mail clients, etc. Unfortunately, no known automatic program termination prover supports a practical method of proving the termination of threads. In this paper we describe such a procedure. The procedure's scalability is achieved through the use of environment models that abstract away the surrounding threads. The procedure's accuracy is due to a novel method of incrementally constructing environment abstractions. Our method finds the conditions that a thread requires of its environment in order to establish termination by looking at the conditions necessary to prove that certain paths through the thread represent well-founded relations if executed in isolation of the other threads. The paper gives a description of experimental results using an implementation of our procedureon Windows device drivers and adescription of a previously unknown bug found withthe tool.

REFERENCES

• 1: B. Alpern and F. Schneider. Defining liveness. Information processing letters, 21:181--185, 1985.
• 2: I. Balaban, A. Cohen, and A. Pnueli. Ranking abstraction of recursive programs. In VMCAI'06: Verification, Model Checking, and Abstract Interpretation, 2006.
• 3: Thomas Ball , Ella Bounimova , Byron Cook , Vladimir Levin , Jakob Lichtenberg , Con McGarvey , Bohus Ondrusek , Sriram K. Rajamani , Abdullah Ustuner, Thorough static analysis of device drivers, Proceedings of the ACM SIGOPS/EuroSys European Conference on Computer Systems 2006, April 18-21, 2006, Leuven, Belgium
• 4: Josh Berdine , Aziem Chawdhary , Byron Cook , Dino Distefano , Peter O'Hearn, Variance analyses from invariance analyses, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 5: J. Berdine, B. Cook, D. Distefano, and P. O'Hearn. Automatic termination proofs for programs with shape-shifting heaps. In CAV'06: International Conference on Computer Aided Verification, 2006.
• 6: A. Biere, C. Artho, and V. Schuppan. Liveness checking as safety checking. In FMICS'02: Formal Methods for Industrial Critical Systems, 2002.
• 7: Bruno Blanchet , Patrick Cousot , Radhia Cousot , Jérome Feret , Laurent Mauborgne , Antoine Miné , David Monniaux , Xavier Rival, A static analyzer for large safety-critical software, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 8: A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, and T. Vojnar. Programs with lists are counter automata. In CAV'06: International Conference on Computer Aided Verification, 2006.
• 9: A. Bradley, Z. Manna, and H. Sipma. Linear ranking with reachability. In CAV'05: Computer-Aided Verification, 2005.
• 10: A. Bradley, Z. Manna, and H. Sipma. The polyranking principle. In ICALP'05: International Colloquium on Automata, Languages and Programming, 2005.
• 11: A. Bradley, Z. Manna, and H. Sipma. Termination analysis of integer linear loops. In CONCUR'05: Concurrency Theory, 2005.
• 12: A. Bradley, Z. Manna, and H. Sipma. Termination of polynomial programs. In VMCAI'05: Verification, Model Checking, and Abstract Interpretation, 2005.
• 13: S. Chaki , E. Clarke , A. Groce , J. Ouaknine , O. Strichman , K. Yorav, Efficient Verification of Sequential and Concurrent C Programs, Formal Methods in System Design, v.25 n.2-3, p.129-166, September-November 2004 [doi>10.1023/B:FORM.0000040026.56959.91]
• 14: E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000.
• 15: E. M. Clarke, M. Talupur, and H. Veith. Environment abstraction for parameterized verification. In VMCAI'06: Verification, Model Checking, and Abstract Interpretation, 2006.
• 16: J. M. Cobleigh, D. Giannakopoulou, and C. S. Pasareanu. Learning assumptions for compositional verification. In TACAS'04: Tools and Algorithms for the Construction and Analysis of Systems, 2003.
• 17: M. Codish and C. Taboch. A semantic basis for the termination analysis of logic programs. The Journal of Logic Programming, 41(1):103--123, 1999.
• 18: Michael Colón , Henny Sipma, Practical Methods for Proving Program Termination, Proceedings of the 14th International Conference on Computer Aided Verification, p.442-454, July 27-31, 2002
• 19: E. Contejean, C. Marché, B. Monate, and X. Urbain. Proving Termination of Rewriting with sc CtextitiME. In WST'03: International Workshop on Termination, 2003.
• 20: Byron Cook , Alexey Gotsman , Andreas Podelski , Andrey Rybalchenko , Moshe Y. Vardi, Proving that programs eventually do something good, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 21: Byron Cook , Andreas Podelski , Andrey Rybalchenko, Termination proofs for systems code, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 22: P. Cousot. Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In VMCAI'05: Verification, Model Checking, and Abstract Interpretation, 2005.
• 23: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 24: Cormac Flanagan , Stephen N. Freund , Shaz Qadeer , Sanjit A. Seshia, Modular verification of multithreaded programs, Theoretical Computer Science, v.338 n.1-3, p.153-183, 10 June 2005 [doi>10.1016/j.tcs.2004.12.006]
• 25: Cormac Flanagan , Patrice Godefroid, Dynamic partial-order reduction for model checking software, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.110-121, January 12-14, 2005, Long Beach, California, USA
• 26: C. Flanagan and S. Qadeer. Thread-modular model checking. In SPIN'03, 2003.
• 27: P. Godefroid. Partial-order methods for the verification of concurrent systems - an approach to the state-explosion problem. PhD thesis, 1994.
• 28: K. Havelund and T. Pressburger. Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer, 2(4), 1998.
• 29: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Permissive interfaces, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 30: T. A. Henzinger, R. Jhala, R. Majumdar, and S. Qadeer. Thread-modular abstraction refinement. In CAV'03, 2003.
• 31: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 32: Bart Jacobs , Frank Piessens , K. Rustan M. Leino , Wolfram Schulte, Safe Concurrency for Aggregate Objects with Invariants, Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, p.137-147, September 07-09, 2005 [doi>10.1109/SEFM.2005.39]
• 33: C. Jones. Specification and design of (parallel) programs. In IFIP Congress, 1983.
• 34: V. Kahlon, A. Gupta, and N. Sinha. Symbolic model checking of concurrent programs using partial orders and on-the-fly transactions. In CAV'06: International Conference on Computer Aided Verification, 2006.
• 35: Richard J. Lipton, Reduction: a method of proving properties of parallel programs, Communications of the ACM, v.18 n.12, p.717-721, Dec. 1975 [doi>10.1145/361227.361234]
• 36: Z. Manna and A. Pnueli. Axiomatic approach to total correctness of programs. Acta Informatica, 1974.
• 37: Antoine Miné, The octagon abstract domain, Higher-Order and Symbolic Computation, v.19 n.1, p.31-100, March 2006 [doi>10.1007/s10990-006-8609-1]
• 38: A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI'04: Verification, Model Checking, and Abstract Interpretation, 2004.
• 39: John C. Reynolds, The Craft of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 40: A. Tiwari. Termination of linear programs. In CAV'04: Computer Aided Verification, 2004.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.5 Reliability

General Terms:
Reliability, Verification

Keywords:
concurrency, formal verification, model checking, program verification, termination, threads