Iterative context bounding for systematic testing of multithreaded programs

ABSTRACT

Multithreaded programs are difficult to get right because of unexpected interaction between concurrently executing threads. Traditional testing methods are inadequate for catching subtle concurrency errors which manifest themselves late in the development cycle and post-deployment. Model checking or systematic exploration of program behavior is a promising alternative to traditional testing methods. However, it is difficult to perform systematic search on large programs as the number of possible program behaviors grows exponentially with the program size. Confronted with this state-explosion problem, traditional model checkers perform iterative depth-bounded search. Although effective for message-passing software, iterative depth-bounding is inadequate for multithreaded software.

This paper proposes iterative context-bounding, a new search algorithm that systematically explores the executions of a multithreaded program in an order that prioritizes executions with fewer context switches. We distinguish between preempting and nonpreempting context switches, and show that bounding the number of preempting context switches to a small number significantly alleviates the state explosion, without limiting the depth of explored executions. We show both theoretically and empirically that context-bounded search is an effective method for exploring the behaviors of multithreaded programs. We have implemented our algorithmin two model checkers and applied it to a number of real-world multithreaded programs. Our implementation uncovered 9 previously unknown bugs in our benchmarks, each of which was exposed by an execution with at most 2 preempting context switches. Our initial experience with the technique is encouraging and demonstrates that iterative context-bounding is a significant improvement over existing techniques for testing multithreaded programs.

REFERENCES

• 1: Derek Bruening and John Chapin. Systematic testing of multithreaded Java programs. Technical Report LCS-TM-607, MIT/LCS, 2000.
• 2: 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
• 3: Matthew B. Dwyer , John Hatcliff , Robby , Venkatesh Prasad Ranganath, Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs, Formal Methods in System Design, v.25 n.2-3, p.199-240, September-November 2004 [doi>10.1023/B:FORM.0000040028.49845.67]
• 4: Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran. Goldilocks: Efficiently computing the happens-before relation using locksets. In FATES/RV 06: Formal Approaches to Testing and Runtime Verification, volume 4262 of Lecture Notes in Computer Science, pages 193--208. Springer-Verlag, 2006.
• 5: E. Allen Emerson , A. Prasad Sistla, Symmetry and model checking, Formal Methods in System Design, v.9 n.1-2, p.105-131, Aug. 1996 [doi>10.1007/BF00625970]
• 6: Cormac Flanagan , Stephen N Freund, Atomizer: a dynamic atomicity checker for multithreaded programs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.256-267, January 14-16, 2004, Venice, Italy
• 7: 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
• 8: 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
• 9: Patrice Godefroid , J. van Leeuwen , J. Hartmanis , G. Goos , Pierre Wolper, Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 10: 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]
• 11: Alex Groce , Willem Visser, Model checking Java programs using structural heuristics, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 12: 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
• 13: C. Norris Ip , David L. Dill, Better verification through symmetry, Formal Methods in System Design, v.9 n.1-2, p.41-75, Aug. 1996 [doi>10.1007/BF00625968]
• 14: Michael Isard, Mihai Budiu, Yuan Yu, Andrew Birrell, and Dennis Fetterly. Dryad: Distributed data-parallel programs from sequential building blocks. Technical Report MSR-TR-2006-140, Microsoft Research, 2006.
• 15: Daan Leijen. Futures: a concurrency library for C#. Technical Report MSR-TR-2006-162, Microsoft Research, 2006.
• 16: 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]
• 17: Ratan Nalumasu , Ganesh Gopalakrishnan, An Efficient Partial Order Reduction Algorithm with an Alternative Proviso Implementation, Formal Methods in System Design, v.20 n.3, p.231-247, May 2002 [doi>10.1023/A:1014728912264]
• 18: Doron Peled, Partial Order Reduction: Model-Checking Using Representatives, Proceedings of the 21st International Symposium on Mathematical Foundations of Computer Science, p.93-112, September 02-06, 1996
• 19: S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS 05: Tools and Algorithms for the Construction and Analysis of Systems, volume 3440 of Lecture Notes in Computer Science, pages 93--107. Springer-Verlag, 2005.
• 20: Shaz Qadeer , Dinghao Wu, KISS: keep it simple and sequential, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 21: 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
• 22: Stuart J. Russell , Peter Norvig, Artificial intelligence: a modern approach, Prentice-Hall, Inc., Upper Saddle River, NJ, 1995
• 23: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 24: Hemanthkumar Sivaraj and Ganesh Gopalakrishnan. Random walk based heuristic algorithms for distributed memory model checking. Electronic Notes in Theoretical Computer Science, 89(1), 2003.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Assertion checkers; Validation

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Assertions

General Terms:
Algorithms, Reliability, Verification

Keywords:
concurrency, context-bounding, model checking, multithreading, partial-order reduction, shared-memory programs, software testing