skip to main content
article

Dynamic partial-order reduction for model checking software

Published: 12 January 2005 Publication History

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]
T. Ball and S. Rajamani. The SLAM Toolkit. In Proceedings of CAV'2001 (13th Conference on Computer Aided Verification), volume 2102 of Lecture Notes in Computer Science, pages 260--264, Paris, July 2001. Springer-Verlag.]]
[2]
E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.]]
[3]
P. R. Cohen and E. A. Feigenbaum. Handbook of Artificial Intelligence. Pitman, London, 1982.]]
[4]
J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Pasareanu, Robby, and H. Zheng. Bandera: Extracting Finite-State Models from Java Source Code. In Proceedings of the 22nd International Conference on Software Engineering, 2000.]]
[5]
M. B. Dwyer, J. Hatcliff, V. R. Prasad, and Robby. Exploiting Object Escape and Locking Information in Partial Order Reduction for Concurrent Object-Oriented Programs. To appear in Formal Methods in System Design, 2004.]]
[6]
J. Esparza. Model Checking Using Net Unfoldings. Science of Computer Programming, 23:151--195, 1994.]]
[7]
J. Esparza and K. Heljanko. Implementing LTL model checking with net unfoldings. In Proceedings of the 8th SPIN Workshop (SPIN'2001), volume 2057 of Lecture Notes in Computer Science, pages 37--56, Toronto, May 2001. Springer-Verlag.]]
[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]
P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems -- An Approach to the State-Explosion Problem, volume 1032 of Lecture Notes in Computer Science. Springer-Verlag, January 1996.]]
[10]
P. Godefroid. Model Checking for Programming Languages using VeriSoft. In Proceedings of POPL'97 (24th ACM Symposium on Principles of Programming Languages), pages 174--186, Paris, January 1997.]]
[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]
P. Godefroid and D. Pirottin. Refining dependencies improves partial-order verification methods. In Proceedings of CAV'93 (5th Conference on Computer Aided Verification), volume 697 of Lecture Notes in Computer Science, pages 438--449, Elounda, June 1993. Springer-Verlag.]]
[13]
P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design, 2(2):149--164, April 1993.]]
[14]
T. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy Abstraction. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages, pages 58--70, Portland, January 2002.]]
[15]
S. Katz and D. Peled. Defining conditional independence using collapses. Theoretical Computer Science, 101:337--359, 1992.]]
[16]
L. Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558--564, 1978.]]
[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. In Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course, volume 255 of Lecture Notes in Computer Science, pages 279--324. Springer-Verlag, 1986.]]
[19]
K. McMillan. Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits. In Proc. 4th Workshop on Computer Aided Verification, volume 663 of Lecture Notes in Computer Science, pages 164--177, Montreal, June 1992. Springer-Verlag.]]
[20]
D. Peled. All from one, one for all: on model checking using representatives. In Proc. 5th Conference on Computer Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 409--423, Elounda, June 1993. Springer-Verlag.]]
[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]
S. D. Stoller, L. Unnikrishnan, and Y. A. Liu. Efficient Detection of Global Properties in Distributed Systems Using Partial-Order Methods. In Proceedings of the 12th Conference on Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 264--279, Chicago, July 2000. Springer-Verlag.]]
[24]
C.A. Thekkath, T. Mann, and E.K. Lee. Frangipani: A scalable distributed file system. In Proceedings of the 16th ACM Symposium on Operating Systems Principles, pages 224--237, October 1997.]]
[25]
A. Valmari. Stubborn sets for reduced state space generation. In Advances in Petri Nets 1990, volume 483 of Lecture Notes in Computer Science, pages 491--515. Springer-Verlag, 1991.]]
[26]
A. Valmari. On-the-fly verification with stubborn sets. In Proc. 5th Conference on Computer Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 397--408, Elounda, June 1993. Springer-Verlag.]]
[27]
W. Visser, K. Havelund, G. Brat, and S. Park. Model Checking Programs. In Proceedings of ASE'2000 (15th International Conference on Automated Software Engineering), Grenoble, September 2000.]]

Cited By

View all
  • (2025)Selectively Uniform Concurrency TestingProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3669940.3707214(1003-1019)Online publication date: 30-Mar-2025
  • (2024)MONARCHProceedings of the 2024 USENIX Conference on Usenix Annual Technical Conference10.5555/3691992.3692025(529-543)Online publication date: 10-Jul-2024
  • (2024)Greybox Fuzzing for Concurrency TestingProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 210.1145/3620665.3640389(482-498)Online publication date: 27-Apr-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 40, Issue 1
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2005
391 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1047659
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
    January 2005
    402 pages
    ISBN:158113830X
    DOI:10.1145/1040305
    • General Chair:
    • Jens Palsberg,
    • Program Chair:
    • Martín Abadi
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 January 2005
Published in SIGPLAN Volume 40, Issue 1

Check for updates

Author Tags

  1. partial-order reduction
  2. software model checking

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)128
  • Downloads (Last 6 weeks)16
Reflects downloads up to 23 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2025)Selectively Uniform Concurrency TestingProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3669940.3707214(1003-1019)Online publication date: 30-Mar-2025
  • (2024)MONARCHProceedings of the 2024 USENIX Conference on Usenix Annual Technical Conference10.5555/3691992.3692025(529-543)Online publication date: 10-Jul-2024
  • (2024)Greybox Fuzzing for Concurrency TestingProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 210.1145/3620665.3640389(482-498)Online publication date: 27-Apr-2024
  • (2024)Intrathread Method Orders Based Adaptive Testing of Concurrent ObjectsTheoretical Aspects of Software Engineering10.1007/978-3-031-64626-3_6(91-108)Online publication date: 29-Jul-2024
  • (2023)Hippodrome: Data Race Repair Using Static Analysis SummariesACM Transactions on Software Engineering and Methodology10.1145/354694232:2(1-33)Online publication date: 31-Mar-2023
  • (2023)Partial-order reduction in reachability-based response-time analyses of limited-preemptive DAG tasksReal-Time Systems10.1007/s11241-023-09398-x59:2(201-255)Online publication date: 8-Jun-2023
  • (2023)Towards Practical Partial Order Reduction for High-Level FormalismsVerified Software. Theories, Tools and Experiments.10.1007/978-3-031-25803-9_5(72-91)Online publication date: 1-Feb-2023
  • (2023)Formale Verifikation von SystemC-basierten Entwürfen durch symbolische SimulationVerbessertes virtuelles Prototyping10.1007/978-3-031-18174-0_4(63-125)Online publication date: 1-Jan-2023
  • (2023)Efficient linearizability checking for actor‐based systemsSoftware: Practice and Experience10.1002/spe.325153:11(2163-2199)Online publication date: 22-Aug-2023
  • (2022)Controlled concurrency testing via periodical schedulingProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510178(474-486)Online publication date: 21-May-2022
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media