Document Open Access Logo

Partial-Order Reduction Is Hard

Authors Frédéric Herbreteau , Sarah Larroze-Jardiné , Igor Walukiewicz

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.22.pdf
  • Filesize: 1.56 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Formal verification
  • Concurrent systems
  • Partial-order reduction
  • Complexity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

The goal of partial-order methods is to accelerate the exploration of concurrent systems by examining only a representative subset of all possible runs. The stateful approach builds a transition system with representative runs, while the stateless method simply enumerates them. The stateless approach may be preferable if the transition system is tree-like; otherwise, the stateful method is more effective.
In the last decade, optimality has been a guiding principle for developing stateless partial-order reduction algorithms, and without doubt contributed to big progress in the field. In this paper we ask if we can get a similar principle for the stateful approach. We show that in stateful exploration, a polynomially close to optimal partial-order algorithm cannot exist unless P=NP. The result holds even for acyclic programs with just await instructions. This lower bound result justifies systematic study of heuristics for stateful partial-order reduction. We propose a notion of IFS oracle as a useful abstraction. The oracle can be used to get a very simple optimal stateless algorithm, which can then be adapted to a non-optimal stateful algorithm. While in general the oracle problem is NP-hard, we show a simple case where it can be solved in linear time.

Cite As Get BibTex

Frédéric Herbreteau, Sarah Larroze-Jardiné, and Igor Walukiewicz. Partial-Order Reduction Is Hard. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.22

Author Details

Frédéric Herbreteau
  • Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400 Talence, France
Sarah Larroze-Jardiné
  • Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400 Talence, France
Igor Walukiewicz
  • Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400 Talence, France

Funding

  • Herbreteau, Frédéric: Supported by the French government in the framework of the France 2030 programme IdEx université de Bordeaux / RRI ROBSYS.
  • Walukiewicz, Igor: Supported by ANR grant PaVeDys, ANR-23-CE48-0005.

References

  1. Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction. Journal of the ACM, 64(4):1-49, 2017. URL: https://doi.org/10.1145/3073408.
  2. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Frederik Meyer Bønneland, Sarbojit Das, Bengt Jonsson, Magnus Lang, and Konstantinos Sagonas. Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs. In Étienne André and Jun Sun, editors, Automated Technology for Verification and Analysis, pages 176-198. Springer Nature Switzerland, 2023. URL: https://doi.org/10.1007/978-3-031-45332-8_9.
  3. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Sarbojit Das, Bengt Jonsson, and Konstantinos Sagonas. Parsimonious optimal dynamic partial order reduction. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part II, volume 14682 of Lecture Notes in Computer Science, pages 19-43. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65630-9_2.
  4. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Sarbojit Das, Bengt Jonsson, and Konstantinos Sagonas. Trading space for simplicity in stateless model checking. In Susanne Graf, Paul Pettersson, and Bernhard Steffen, editors, Real Time and Such - Essays Dedicated to Wang Yi to Celebrate His Scientific Career, volume 15230 of Lecture Notes in Computer Science, pages 79-97. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-73751-0_8.
  5. Pratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, and Viktor Toman. Stateless Model Checking Under a Reads-Value-From Equivalence. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification, volume 12759, pages 341-366. Springer International Publishing, 2021. URL: https://doi.org/10.1007/978-3-030-81685-8_16.
  6. Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. Data-centric dynamic partial order reduction. Proceedings of the ACM on Programming Languages, 2(POPL):1-30, 2018. URL: https://doi.org/10.1145/3158119.
  7. Berk Cirisci, Constantin Enea, Azadeh Farzan, and Suha Orhun Mutluergil. A Pragmatic Approach to Stateful Partial Order Reduction. In Cezara Dragoi, Michael Emmi, and Jingbo Wang, editors, Verification, Model Checking, and Abstract Interpretation, volume 13881, pages 129-154. Springer Nature Switzerland, 2023. URL: https://doi.org/10.1007/978-3-031-24950-1_7.
  8. Camille Coti, Laure Petrucci, César Rodríguez, and Marcelo Sousa. Quasi-optimal partial order reduction. Formal Methods in System Design, 57(1):3-33, 2021. URL: https://doi.org/10.1007/s10703-020-00350-4.
  9. Frank S. De Boer, Marcello Bonsangue, Einar Broch Johnsen, Violet Ka I Pun, S. Lizeth Tapia Tarifa, and Lars Tveito. SymPaths: Symbolic Execution Meets Partial Order Reduction. In Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, and Mattias Ulbrich, editors, Deductive Software Verification: Future Perspectives, volume 12345, pages 313-338. Springer International Publishing, 2020. URL: https://doi.org/10.1007/978-3-030-64354-6_13.
  10. Azadeh Farzan. Commutativity in Automated Verification. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-7. IEEE, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175734.
  11. Azadeh Farzan, Dominik Klumpp, and Andreas Podelski. Sound sequentialization for concurrent program verification. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 506-521. ACM, 2022. URL: https://doi.org/10.1145/3519939.3523727.
  12. Cormac Flanagan and Patrice Godefroid. Dynamic Partial-Order Reduction for Model Checking Software. In POPL'05, 2005. Google Scholar
  13. Patrice Godefroid. Using partial orders to improve automatic verification methods. In Edmund M. Clarke and Robert P. Kurshan, editors, Computer-Aided Verification, pages 176-185. Springer, 1991. URL: https://doi.org/10.1007/BFb0023731.
  14. Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems An Approach to the State-Explosion Problem. PhD thesis, Université de Liège, 1994. Google Scholar
  15. R. Govind, Frédéric Herbreteau, Srivathsan, and Igor Walukiewicz. Abstractions for the local-time semantics of timed automata: A foundation for partial-order methods. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 1-14. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533343.
  16. Maurice Herlihy. Wait-free synchronization. ACM Trans. Program. Lang. Syst., 13(1):124-149, 1991. URL: https://doi.org/10.1145/114005.102808.
  17. Casper S. Jensen, Anders Moller, Veselin Raychev, Dimitar Dimitrov, and Martin Vechev. Stateless model checking of event-driven applications. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, pages 57-73. Association for Computing Machinery, 2015. URL: https://doi.org/10.1145/2814270.2814282.
  18. Bengt Jonsson, Magnus Lang, and Konstantinos Sagonas. Awaiting for Godot Stateless Model Checking that Avoids Executions where Nothing Happens. In 22nd Formal Methods in Computer-Aided Design, FMCAD 2022. IEEE, 2022. Google Scholar
  19. Vineet Kahlon, Chao Wang, and Aarti Gupta. Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. In Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification, volume 5643, pages 398-413. Springer Berlin Heidelberg, 2009. URL: https://doi.org/10.1007/978-3-642-02658-4_31.
  20. Shmuel Katz and Doron Peled. Verification of distributed programs using representative interleaving sequences. Distributed Computing, 6(2):107-120, 1992. URL: https://doi.org/10.1007/BF02252682.
  21. Michalis Kokologiannakis, Rupak Majumdar, and Viktor Vafeiadis. Enhancing GenMC’s Usability and Performance. In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 66-84. Springer Nature Switzerland, 2024. URL: https://doi.org/10.1007/978-3-031-57249-4_4.
  22. Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis. Truly stateless, optimal dynamic partial order reduction. Proceedings of the ACM on Programming Languages, 6(POPL):1-28, 2022. URL: https://doi.org/10.1145/3498711.
  23. Michalis Kokologiannakis, Iason Marmanis, and Viktor Vafeiadis. Unblocking Dynamic Partial Order Reduction. In Constantin Enea and Akash Lal, editors, Computer Aided Verification, volume 13964, pages 230-250. Springer Nature Switzerland, 2023. URL: https://doi.org/10.1007/978-3-031-37706-8_12.
  24. Michalis Kokologiannakis, Iason Marmanis, and Viktor Vafeiadis. SPORE: combining symmetry and partial order reduction. Proc. ACM Program. Lang., 8(PLDI):1781-1803, 2024. URL: https://doi.org/10.1145/3656449.
  25. Pallavi Maiya, Rahul Gupta, Aditya Kanade, and Rupak Majumdar. Partial Order Reduction for Event-Driven Multi-threaded Programs. In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 680-697. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49674-9_44.
  26. Antoni W. Mazurkiewicz. Introduction to trace theory. In Volker Diekert and Grzegorz Rozenberg, editors, The Book of Traces, pages 3-41. World Scientific, 1995. URL: https://doi.org/10.1142/9789814261456_0001.
  27. Message Passing Interface Forum. MPI: A Message-Passing Interface Standard Version 4.1, November 2023. URL: https://www.mpi-forum.org/docs/mpi-4.1/mpi41-report.pdf.
  28. Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Simin Oraee. Trace aware random testing for distributed systems. Proceedings of the ACM on Programming Languages, 3(OOPSLA):1-29, 2019. URL: https://doi.org/10.1145/3360606.
  29. Doron Peled. Partial-order reduction. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 173-190. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_6.
  30. Doron A. Peled. All from one, one for all: on model checking using representatives. In Costas Courcoubetis, editor, Computer Aided Verification, 5th International Conference, CAV '93, Elounda, Greece, June 28 - July 1, 1993, Proceedings, volume 697 of Lecture Notes in Computer Science, pages 409-423. Springer, 1993. URL: https://doi.org/10.1007/3-540-56922-7_34.
  31. The Anh Pham. Efficient State-Space Exploration for Asynchronous Distributed Programs: Adapting Unfolding-Based Dynamic Partial Order Reduction to MPI Programs. These de doctorat, Rennes, Ecole normale superieure, 2019. Google Scholar
  32. César Rodríguez, Marcelo Sousa, Subodh Sharma, and Daniel Kroening. Unfolding-based Partial Order Reduction. LIPIcs, Volume 42, CONCUR 2015, 42:456-469, 2015. URL: https://doi.org/10.4230/LIPICS.CONCUR.2015.456.
  33. Samira Tasharofi, Rajesh K. Karmani, Steven Lauterburg, Axel Legay, Darko Marinov, and Gul Agha. TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs. In Holger Giese and Grigore Rosu, editors, Formal Techniques for Distributed Systems, pages 219-234. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-30793-5_14.
  34. Antti Valmari. Stubborn sets for reduced state space generation. In G. Goos, J. Hartmanis, D. Barstow, W. Brauer, P. Brinch Hansen, D. Gries, D. Luckham, C. Moler, A. Pnueli, G. Seegmüller, J. Stoer, N. Wirth, and Grzegorz Rozenberg, editors, Advances in Petri Nets 1990, volume 483, pages 491-515. Springer Berlin Heidelberg, 1991. URL: https://doi.org/10.1007/3-540-53863-1_36.
  35. Bjorn Wachter, Daniel Kroening, and Joel Ouaknine. Verifying multi-threaded software with impact. In 2013 Formal Methods in Computer-Aided Design, pages 210-217. IEEE, 2013. URL: https://doi.org/10.1109/FMCAD.2013.6679412.
  36. Chao Wang, Zijiang Yang, Vineet Kahlon, and Aarti Gupta. Peephole Partial Order Reduction. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 4963, pages 382-396. Springer Berlin Heidelberg, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_29.
  37. Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, and Robert M. Kirby. Efficient Stateful Dynamic Partial Order Reduction. In Klaus Havelund, Rupak Majumdar, and Jens Palsberg, editors, Model Checking Software, pages 288-305. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85114-1_20.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact