Fair stateless model checking

ABSTRACT

Stateless model checking is a useful state-space exploration technique for systematically testing complex real-world software. Existing stateless model checkers are limited to the verification of safety properties on terminating programs. However, realistic concurrent programs are nonterminating, a property that significantly reduces the efficacy of stateless model checking in testing them. Moreover, existing stateless model checkers are unable to verify that a nonterminating program satisfies the important liveness property of livelock-freedom, a property that requires the program to make continuous progress for any input.

To address these shortcomings, this paper argues for incorporating a fair scheduler in stateless exploration. The key contribution of this paper is an explicit scheduler that is (strongly) fair and at the same time sufficiently nondeterministic to guarantee full coverage of safety properties.We have implemented the fair scheduler in the CHESS model checker. We show through theoretical arguments and empirical evaluation that our algorithm satisfies two important properties: 1) it visits all states of a finite-state program achieving state coverage at a faster rate than existing techniques, and 2) it finds all livelocks in a finite-state program. Before this work, nonterminating programs had to be manually modified in order to apply CHESS to them. The addition of fairness has allowed CHESS to be effectively applied to real-world nonterminating programs without any modification. For example, we have successfully booted the Singularity operating system under the control of CHESS.

REFERENCES

• 1: S. Aggarwal , C. Courcoubetis , P. Wolper, Adding liveness properties to coupled finite-state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.2, p.303-339, April 1990 [doi>10.1145/78942.78948]
• 2: K.R. Apt and E.-R. Olderog. Proof rules and transformations dealing with fairness. Science of Computer Programming, 3:65--100, 1983.
• 3: K. R. Apt , N. Francez , S. Katz, Appraising fairness in distributed languages, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.189-198, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41642]
• 4: Satish Chandra , Patrice Godefroid , Christopher Palm, Software model checking in practice: an industrial case study, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581393]
• 5: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 6: Nissim Francez, Fairness, Springer-Verlag New York, Inc., New York, NY, 1986
• 7: Matteo Frigo , Charles E. Leiserson , Keith H. Randall, The implementation of the Cilk-5 multithreaded language, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.212-223, June 17-19, 1998, Montreal, Quebec, Canada
• 8: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 9: Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. LNCS 1032. Springer-Verlag, 1996.
• 10: Orna Grumberg , Nissim Francez , Shmuel Katz, Fair termination of communicating processes, Proceedings of the third annual ACM symposium on Principles of distributed computing, p.254-265, August 27-29, 1984, Vancouver, British Columbia, Canada [doi>10.1145/800222.806752]
• 11: J. L. Hellerstein, Achieving Service Rate Objectives with Decay Usage Scheduling, IEEE Transactions on Software Engineering, v.19 n.8, p.813-825, August 1993 [doi>10.1109/32.238584]
• 12: 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]
• 13: Galen Hunt , Mark Aiken , Manuel Fähndrich , Chris Hawblitzel , Orion Hodson , James Larus , Steven Levi , Bjarne Steensgaard , David Tarditi , Ted Wobber, Sealing OS processes to improve dependability and safety, Proceedings of the 2nd ACM SIGOPS/EuroSys European Conference on Computer Systems 2007, March 21-23, 2007, Lisbon, Portugal
• 14: Radu Iosif, Exploiting Heap Symmetries in Explicit-State Model Checking of Software, Proceedings of the 16th IEEE international conference on Automated software engineering, p.254, November 26-29, 2001
• 15: Michael Isard , Mihai Budiu , Yuan Yu , Andrew Birrell , Dennis Fetterly, Dryad: distributed data-parallel programs from sequential building blocks, Proceedings of the 2nd ACM SIGOPS/EuroSys European Conference on Computer Systems 2007, March 21-23, 2007, Lisbon, Portugal
• 16: J. Kay , P. Lauder, A fair share scheduler, Communications of the ACM, v.31 n.1, p.44-55, Jan. 1988 [doi>10.1145/35043.35047]
• 17: Charles Edwin Killian, James W. Anderson, Ranjit Jhala, and Amin Vahdat. Life, death, and the critical transition: Finding liveness bugs in systems code. In NSDI 07: Symposium on Networked Systems Design and Implementation, pages 243--256, 2007.
• 18: M. Z. Kwiatkowska, Survey of fairness notions, Information and Software Technology, v.31 n.7, p.371-386, Sept. 1989 [doi>10.1016/0950-5849(89)90159-6]
• 19: Daniel J. Lehmann , Amir Pnueli , Jonathan Stavi, Impartiality, Justice and Fairness: The Ethics of Concurrent Termination, Proceedings of the 8th Colloquium on Automata, Languages and Programming, p.264-277, July 13-17, 1981
• 20: Daan Leijen. Futures: a concurrency library for C#. Technical Report MSR-TR-2006-162, Microsoft Research, 2006.
• 21: Madanlal Musuvathi , David Y. W. Park , Andy Chou , Dawson R. Engler , David L. Dill, CMC: a pragmatic approach to model checking real code, Proceedings of the 5th symposium on Operating systems design and implementation

  Due to copyright restrictions we are not able to make the PDFs for this conference available for downloading

  , December 09-11, 2002, Boston, Massachusetts [doi>10.1145/1060289.1060297]
• 22: Madanlal Musuvathi , Shaz Qadeer, Iterative context bounding for systematic testing of multithreaded programs, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 23: Amir Pnueli, The temporal logic of programs, Proceedings of the 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), p.46-57, September 30-October 31, 1977
• 24: Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
• 25: M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS 86: Logic in Computer Science, pages 322--331. IEEE Computer Society Press, 1986.
• 26: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000
• 27: Carl A. Waldspurger , William E. Weihl, Lottery scheduling: flexible proportional-share resource management, Proceedings of the 1st USENIX conference on Operating Systems Design and Implementation, p.1-es, November 14-17, 1994, Monterey, California
• 28: Junfeng Yang , Paul Twohey , Dawson Engler , Madanlal Musuvathi, Using model checking to find serious file system errors, ACM Transactions on Computer Systems (TOCS), v.24 n.4, p.393-423, November 2006 [doi>10.1145/1189256.1189259]

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation
      D.2.5 Testing and Debugging
          Subjects: Tracing; Monitors; Diagnostics; Debugging aids

General Terms:
Algorithms, Reliability, Verification

Keywords:
concurrency, fairness, liveness, model checking, multi-threading, shared-memory programs, software testing