Dynamic partial-order reduction for model checking software

ABSTRACT

We present a new approach to partial-order reduction for model checking software. This approach is based on initially exploring an arbitrary interleaving of the various concurrent processes/threads, and dynamically tracking interactions between these to identify backtracking points where alternative paths in the state space need to be explored. We present examples of multi-threaded programs where our new dynamic partial-order reduction technique significantly reduces the search space, even though traditional partial-order algorithms are helpless.

REFERENCES

• 1: Thomas Ball , Sriram K. Rajamani, The SLAM Toolkit, Proceedings of the 13th International Conference on Computer Aided Verification, p.260-264, July 18-22, 2001
• 2: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 3: P. R. Cohen and E. A. Feigenbaum. Handbook of Artificial Intelligence. Pitman, London, 1982.
• 4: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 5: 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]
• 6: Javier Esparza, Model checking using net unfoldings, Science of Computer Programming, v.23 n.2-3, p.151-195, Dec. 1994
• 7: Javier Esparza , Keijo Heljanko, Implementing LTL model checking with net unfoldings, Proceedings of the 8th international SPIN workshop on Model checking of software, p.37-56, May 2001, Toronto, Ontario, Canada
• 8: C. Flanagan and S. Qadeer. Transactions for Software Model Checking. In Proceedings of the Workshop on Software Model Checking, pages 338--349, June 2003.
• 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: P. Godefroid. Software Model Checking: The VeriSoft Approach. To appear in Formal Methods in System Design, 2005. Also available as Bell Labs Technical Memorandum ITD-03-44189G.
• 12: Patrice Godefroid , Didier Pirottin, Refining Dependencies Improves Partial-Order Verification Methods (Extended Abstract), Proceedings of the 5th International Conference on Computer Aided Verification, p.438-449, June 28-July 01, 1993
• 13: Patrice Godefroid , Pierre Wolper, Using partial orders for the efficient verification of deadlock freedom and safety properties, Formal Methods in System Design, v.2 n.2, p.149-164, April 1993 [doi>10.1007/BF01383879]
• 14: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 15: Shmuel Katz , Doron Peled, Defining conditional independence using collapses, Theoretical Computer Science, v.101 n.2, p.337-359, July 20, 1992 [doi>10.1016/0304-3975(92)90054-J]
• 16: Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
• 17: F. Mattern. Virtual Time and Global States of Distributed Systems. In Proc. Workshop on Parallel and Distributed Algorithms, pages 215--226. North-Holland / Elsevier, 1989.
• 18: A Mazurkiewicz, Trace theory, Advances in Petri nets 1986, part II on Petri nets: applications and relationships to other models of concurrency, p.279-324, February 1987, Bad Honnef
• 19: Kenneth L. McMillan, Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.164-177, June 29-July 01, 1992
• 20: Doron Peled, All from One, One for All: on Model Checking Using Representatives, Proceedings of the 5th International Conference on Computer Aided Verification, p.409-423, June 28-July 01, 1993
• 21: S. D. Stoller. Model-Checking Multi-Threaded Distributed Java Programs. International Journal on Software Tools for Technology Transfer, 4(1):71--91, October 2002.
• 22: S. D. Stoller and E. Cohen. Optimistic Synchronization-Based State-Space Reduction. In H. Garavel and J. Hatcliff, editors, Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2619 of Lecture Notes in Computer Science, pages 489--504. Springer-Verlag, April 2003.
• 23: Scott D. Stoller , Leena Unnikrishnan , Yanhong A. Liu, Efficient Detection of Global Properties in Distributed Systems Using Partial-Order Methods, Proceedings of the 12th International Conference on Computer Aided Verification, p.264-279, July 15-19, 2000
• 24: Chandramohan A. Thekkath , Timothy Mann , Edward K. Lee, Frangipani: a scalable distributed file system, Proceedings of the sixteenth ACM symposium on Operating systems principles, p.224-237, October 05-08, 1997, Saint Malo, France
• 25: Antti Valmari, Stubborn sets for reduced state generation, Proceedings on Advances in Petri nets 1990, p.491-515, March 1991
• 26: Antti Valmari, On-the-Fly Verification with Stubborn Sets, Proceedings of the 5th International Conference on Computer Aided Verification, p.397-408, June 28-July 01, 1993
• 27: 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

INDEX TERMS

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

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

General Terms:
Algorithms, Reliability, Verification

Keywords:
partial-order reduction, software model checking