Document Open Access Logo

Optimal Concolic Dynamic Partial Order Reduction

Authors Mohammad Hossein Khoshechin Jorshari , Michalis Kokologiannakis , Rupak Majumdar , Srinidhi Nagendra

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.26.pdf
  • Filesize: 1.18 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Verification by model checking
Keywords
  • Stateless model checking
  • dynamic symbolic execution

Metrics

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

Abstract

Stateless model checking (SMC) software implementations requires exploring both concurrency- and data nondeterminism. Unfortunately, most SMC algorithms focus on efficient exploration of concurrency nondeterminism, thereby neglecting an important source of bugs.
We present ConDpor, an SMC algorithm for unmodified Java programs that combines optimal dynamic partial order reduction (DPOR) for concurrency nondeterminism, with concolic execution for data nondeterminism. ConDpor is sound, complete, optimal, and parametric w.r.t. the memory consistency model. Our experiments confirm that ConDpor is exponentially faster than DPOR with small-domain enumeration. Overall, ConDpor opens the door for efficient exploration of concurrent programs with data nondeterminism.

Cite As Get BibTex

Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar, and Srinidhi Nagendra. Optimal Concolic Dynamic Partial Order Reduction. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.26

Author Details

Mohammad Hossein Khoshechin Jorshari
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Michalis Kokologiannakis
  • ETH Zurich, Switzerland
Rupak Majumdar
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Srinidhi Nagendra
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany

Funding

This research was funded in part by the DFG project 389792660 TRR 248–CPEC.

Acknowledgements

We thank the anonymous reviewers for their detailed and constructive feedback, and Iason Marmanis for helpful feedback and suggestions.

Supplementary Materials

References

  1. asm / asm · GitLab - gitlab.ow2.org. https://gitlab.ow2.org/asm/asm. [Accessed 29-01-2025].
  2. GitHub - openjdk/jcstress. https://github.com/openjdk/jcstress. [Accessed 31-01-2025].
  3. GitHub - Z3Prover/z3: The Z3 Theorem Prover - github.com. https://github.com/Z3Prover/z3. [Accessed 30-01-2025].
  4. Parosh Abdulla, Mohamed Faouzi Atig, S Krishna, Ashutosh Gupta, and Omkar Tuppe. Optimal stateless model checking for causal consistency. In TACAS, pages 105-125. Springer, 2023. Google Scholar
  5. Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. Stateless model checking for TSO and PSO. In TACAS 2015, volume 9035 of LNCS, pages 353-367, Berlin, Heidelberg, 2015. Springer. URL: https://doi.org/10.1007/978-3-662-46681-0_28.
  6. Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. Optimal dynamic partial order reduction. In POPL 2014, pages 373-384, New York, NY, USA, 2014. ACM. URL: https://doi.org/10.1145/2535838.2535845.
  7. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Sarbojit Das, Bengt Jonsson, and Konstantinos Sagonas. Parsimonious optimal dynamic partial order reduction. In CAV 2024, pages 19-43, Cham, 2024. Springer. URL: https://doi.org/10.1007/978-3-031-65630-9_2.
  8. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan Phong Ngo. Optimal stateless model checking under the release-acquire semantics. Proc. ACM Program. Lang., 2(OOPSLA):135:1-135:29, October 2018. URL: https://doi.org/10.1145/3276505.
  9. Parosh Aziz Abdulla, Ashutosh Gupta, Shankara Narayanan Krishna, and Omkar Tuppe. Dynamic partial order reduction for transactional programs on serializable platforms. In International Symposium on Automated Technology for Verification and Analysis, pages 181-202. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-78709-6_9.
  10. Yehuda Afek, Eli Gafni, and Adam Morrison. Common2 extended to stacks and unbounded concurrency. Distributed Comput., 20(4):239-252, 2007. URL: https://doi.org/10.1007/S00446-007-0023-3.
  11. Elvira Albert, Maria Garcia de la Banda, Miguel Gómez-Zamalloa, Miguel Isabel, and Peter J. Stuckey. Optimal dynamic partial order reduction with context-sensitive independence and observers. J. Syst. Softw., 202:111730, 2023. URL: https://doi.org/10.1016/J.JSS.2023.111730.
  12. Saswat Anand, Corina S. Păsăreanu, and Willem Visser. JPF-SE: A symbolic execution extension to java pathfinder. In TACAS 2007, pages 134-138, Berlin, Heidelberg, 2007. Springer. URL: https://doi.org/10.1007/978-3-540-71209-1_12.
  13. Daniel Baier, Dirk Beyer, and Karlheinz Friedberger. Javasmt 3: Interacting with SMT solvers in java. In Alexandra Silva and K. Rustan M. Leino, editors, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II, volume 12760 of Lecture Notes in Computer Science, pages 195-208. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-81688-9_9.
  14. Rudolf Bayer and Mario Schkolnick. Concurrency of operations on b-trees. Acta Informatica, 9:1-21, 1977. URL: https://doi.org/10.1007/BF00263762.
  15. Stefan Bucur, Johannes Kinder, and George Candea. Prototyping symbolic execution engines for interpreted languages. In ASPLOS 2014, pages 239-254, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2541940.2541977.
  16. Stefan Bucur, Vlad Ureche, Cristian Zamfir, and George Candea. Parallel symbolic execution for automated real-world software testing. In EuroSys 2011, pages 183-198, New York, NY, USA, 2011. ACM. URL: https://doi.org/10.1145/1966445.1966463.
  17. Sebastian Burckhardt, Chris Dern, Madanlal Musuvathi, and Roy Tan. Line-Up: A complete and automatic linearizability checker. In Benjamin G. Zorn and Alexander Aiken, editors, PLDI 2010, pages 330-340. ACM, 2010. URL: https://doi.org/10.1145/1806596.1806634.
  18. Sebastian Burckhardt, Pravesh Kothari, Madanlal Musuvathi, and Santosh Nagarakatte. A randomized scheduler with probabilistic guarantees of finding bugs. In ASPLOS 2010, ASPLOS XV, pages 167-178, New York, NY, USA, 2010. ACM. URL: https://doi.org/10.1145/1736020.1736040.
  19. Cristian Cadar, Daniel Dunbar, and Dawson Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI 2008, pages 209-224, USA, 2008. USENIX Association. URL: http://www.usenix.org/events/osdi08/tech/full_papers/cadar/cadar.pdf.
  20. Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, and Dawson R. Engler. Exe: Automatically generating inputs of death. ACM Trans. Inf. Syst. Secur., 12(2), December 2008. URL: https://doi.org/10.1145/1455518.1455522.
  21. Sang Kil Cha, Thanassis Avgerinos, Alexandre Rebert, and David Brumley. Unleashing mayhem on binary code. In IEEE Symposium on Security and Privacy, SP 2012, pages 380-394. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/SP.2012.31.
  22. Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. Data-centric dynamic partial order reduction. Proc. ACM Program. Lang., 2(POPL):31:1-31:30, December 2017. URL: https://doi.org/10.1145/3158119.
  23. Vitaly Chipounov, Volodymyr Kuznetsov, and George Candea. The S2E platform: Design, implementation, and applications. ACM Trans. Comput. Syst., 30(1):2:1-2:49, 2012. URL: https://doi.org/10.1145/2110356.2110358.
  24. Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs. In Kurt Jensen and Andreas Podelski, editors, TACAS 2004, volume 2988 of LNCS, pages 168-176, Berlin, Heidelberg, 2004. Springer. URL: https://doi.org/10.1007/978-3-540-24730-2_15.
  25. Cinzia Di Giusto, Davide Ferré, Laetitia Laversa, and Etienne Lozes. A partial order view of message-passing communication models. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571248.
  26. Mike Dodds, Andreas Haas, and Christoph M. Kirsch. A scalable, correct time-stamped stack. In POPL 2015, pages 233-246, New York, NY, USA, 2015. ACM. URL: https://doi.org/10.1145/2676726.2676963.
  27. Constantin Enea, Dimitra Giannakopoulou, Michalis Kokologiannakis, and Rupak Majumdar. Model checking distributed protocols in must. Proc. ACM Program. Lang., 8(OOPSLA2), October 2024. URL: https://doi.org/10.1145/3689778.
  28. Azadeh Farzan, Andreas Holzer, Niloofar Razavi, and Helmut Veith. Con2colic testing. In ESEC/FSE, pages 37-47. ACM, 2013. URL: https://doi.org/10.1145/2491411.2491453.
  29. Cormac Flanagan and Patrice Godefroid. Dynamic partial-order reduction for model checking software. In POPL 2005, pages 110-121, New York, NY, USA, 2005. ACM. URL: https://doi.org/10.1145/1040305.1040315.
  30. Patrice Godefroid. Model checking for programming languages using VeriSoft. In POPL 1997, pages 174-186, New York, NY, USA, 1997. ACM. URL: https://doi.org/10.1145/263699.263717.
  31. Patrice Godefroid, Nils Klarlund, and Koushik Sen. Dart: directed automated random testing. In PLDI 2005, pages 213-223, New York, NY, USA, 2005. ACM. URL: https://doi.org/10.1145/1065010.1065036.
  32. Patrice Godefroid, Michael Y. Levin, and David A. Molnar. Automated whitebox fuzz testing. In NDSS. The Internet Society, 2008. URL: https://www.ndss-symposium.org/ndss2008/automated-whitebox-fuzz-testing/.
  33. Henning Günther, Alfons Laarman, Ana Sokolova, and Georg Weissenbacher. Dynamic reductions for model checking concurrent software. In VMCAI 2017, Paris, France, Proceedings 18, pages 246-265. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-52234-0_14.
  34. Shengjian Guo, Markus Kusano, Chao Wang, Zijiang Yang, and Aarti Gupta. Assertion guided symbolic execution of multithreaded programs. In ESEC/FSE, pages 854-865. ACM, 2015. URL: https://doi.org/10.1145/2786805.2786841.
  35. Klaus Havelund and Thomas Pressburger. Model checking JAVA programs using JAVA pathfinder. Int. J. Soft. Tool. Tech. Transf., 2(4):366-381, 2000. URL: https://doi.org/10.1007/S100090050043.
  36. Steve Heller, Maurice Herlihy, Victor Luchangco, Mark Moir, William N. Scherer, and Nir Shavit. A lazy concurrent list-based set algorithm. In OPODIS 2005, pages 3-16, Berlin, Heidelberg, 2005. Springer-Verlag. URL: https://doi.org/10.1007/11795490_3.
  37. Danny Hendler, Nir Shavit, and Lena Yerushalmi. A scalable lock-free stack algorithm. In SPAA 2004, pages 206-215, New York, NY, USA, 2004. ACM. URL: https://doi.org/10.1145/1007912.1007944.
  38. Maurice Herlihy and Nir Shavit. The art of multiprocessor programming. Morgan Kaufmann Publishers Inc., 2008. Google Scholar
  39. G.J. Holzmann. The model checker spin. IEEE Trans. Software Eng., 23(5):279-295, 1997. URL: https://doi.org/10.1109/32.588521.
  40. Jeff Huang. Stateless model checking concurrent programs with maximal causality reduction. In PLDI 2015, pages 165-174, New York, NY, USA, 2015. ACM. URL: https://doi.org/10.1145/2737924.2737975.
  41. Karthick Jayaraman, David Harvison, Vijay Ganesh, and Adam Kiezun. jfuzz: A concolic whitebox fuzzer for java. In Ewen Denney, Dimitra Giannakopoulou, and Corina S. Pasareanu, editors, NFM 2009, Moffett Field, California, USA, April 6-8, 2009, volume NASA/CP-2009-215407 of NASA Conference Proceedings, pages 121-125, 2009. Google Scholar
  42. 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, CAV 2009, Grenoble, France, Proceedings, volume 5643 of Lecture Notes in Computer Science, pages 398-413. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02658-4_31.
  43. James C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385-394, July 1976. URL: https://doi.org/10.1145/360248.360252.
  44. Michalis Kokologiannakis, Mohammad Hossein Khoshechin Jorshari, Srinidhi Nagendra, and Rupak Majumdar. Optimal concolic dynamic partial order reduction, June 2025. URL: https://doi.org/10.5281/zenodo.15649583.
  45. Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis. Truly stateless, optimal dynamic partial order reduction. Proc. ACM Program. Lang., 6(POPL), January 2022. URL: https://doi.org/10.1145/3498711.
  46. Michalis Kokologiannakis, Iason Marmanis, and Viktor Vafeiadis. Unblocking dynamic partial order reduction. In Constantin Enea and Akash Lal, editors, CAV 2023, volume 13964 of LNCS, pages 230-250. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-37706-8_12.
  47. Michalis Kokologiannakis, Iason Marmanis, and Viktor Vafeiadis. SPORE: Combining symmetry and partial order reduction. Proc. ACM Program. Lang., 8(PLDI), June 2024. URL: https://doi.org/10.1145/3656449.
  48. Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis. Model checking for weakly consistent libraries. In PLDI 2019, New York, NY, USA, 2019. ACM. URL: https://doi.org/10.1145/3314221.3314609.
  49. Nikita Koval, Alexander Fedorov, Maria Sokolova, Dmitry Tsitelov, and Dan Alistarh. Lincheck: A practical framework for testing concurrent data structures on JVM. In Constantin Enea and Akash Lal, editors, CAV 2023, pages 156-169, Cham, 2023. Springer. URL: https://doi.org/10.1007/978-3-031-37706-8_8.
  50. Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. Repairing sequential consistency in C/C++11. In PLDI 2017, pages 618-632, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3062341.3062352.
  51. Leslie Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers, 28(9):690-691, September 1979. URL: https://doi.org/10.1109/TC.1979.1675439.
  52. Ao Li, Byeongjee Kang, Vasudev Vikram, Isabella Laybourn, Samvid Dharanikota, Shrey Tiwari, and Rohan Padhye. Fray: An efficient general-purpose concurrency testing platform for the jvm, 2025. URL: https://doi.org/10.48550/arXiv.2501.12618.
  53. Dongge Liu, Gidon Ernst, Toby Murray, and Benjamin I. P. Rubinstein. Legion: Best-first concolic testing (competition contribution). In Heike Wehrheim and Jordi Cabot, editors, FASE 2020, Dublin, Ireland, Proceedings, volume 12076 of Lecture Notes in Computer Science, pages 545-549. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45234-6_31.
  54. Antoni Mazurkiewicz. Trace theory. In PNAROMC 1987, volume 255 of LNCS, pages 279-324, Berlin, Heidelberg, 1987. Springer. URL: https://doi.org/10.1007/3-540-17906-2_30.
  55. Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gérard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. Finding and reproducing heisenbugs in concurrent programs. In OSDI 2008, pages 267-280. USENIX Association, 2008. URL: https://www.usenix.org/legacy/events/osdi08/tech/full_papers/musuvathi/musuvathi.pdf.
  56. Brian Norris and Brian Demsky. CDSChecker: Checking concurrent data structures written with C/C++ atomics. In OOPSLA 2013, pages 131-150. ACM, 2013. URL: https://doi.org/10.1145/2509136.2509514.
  57. Scott Owens, Susmit Sarkar, and Peter Sewell. A better x86 memory model: x86-TSO. In TPHOLs 2009, pages 391-407. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_27.
  58. Daniel Schemmel, Julian Büning, Cesar Rodriguez, David Laprell, and Klaus Wehrle. Symbolic partial-order execution for testing multi-threaded programs. In Shuvendu K. Lahiri and Chao Wang, editors, CAV, volume 12224, pages 376-400. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53288-8_18.
  59. Koushik Sen and Gul Agha. CUTE and jCUTE: concolic unit testing and explicit path model-checking tools. In CAV 2006, pages 419-423, Berlin, Heidelberg, 2006. Springer-Verlag. URL: https://doi.org/10.1007/11817963_38.
  60. Koushik Sen and Gul Agha. A race-detection and flipping algorithm for automated testing of multi-threaded programs. In HVC 2006, pages 166-182, Berlin, Heidelberg, 2006. Springer-Verlag. URL: https://doi.org/10.1007/978-3-540-70889-6_13.
  61. Koushik Sen, Darko Marinov, and Gul Agha. CUTE: a concolic unit testing engine for c. In ESEC/FSE 2013, pages 263-272, New York, NY, USA, 2005. ACM. URL: https://doi.org/10.1145/1081706.1081750.
  62. Dennis Shasha and Marc Snir. Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst., 10(2):282-312, April 1988. URL: https://doi.org/10.1145/42190.42277.
  63. Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Audrey Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Kruegel, and Giovanni Vigna. SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis. In IEEE Symposium on Security and Privacy, 2016. Google Scholar
  64. Shuttle. URL: https://github.com/awslabs/shuttle.
  65. Stephen F. Siegel, Manchun Zheng, Ziqing Luo, Timothy K. Zirkel, Andre V. Marianiello, John G. Edenhofner, Matthew B. Dwyer, and Michael S. Rogers. Civl: the concurrency intermediate verification language. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, SC '15, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2807591.2807635.
  66. Zachary Susag, Sumit Lahiri, Justin Hsu, and Subhajit Roy. Symbolic execution for randomized programs. Proc. ACM Program. Lang., 6(OOPSLA2):1583-1612, 2022. URL: https://doi.org/10.1145/3563344.
  67. SV-COMP. Competition on software verification (SV-COMP), 2019. URL: https://sv-comp.sosy-lab.org/2019/.
  68. Nikolai Tillmann and Jonathan de Halleux. Pex-White box test generation for .NET. In TAP 2008, pages 134-153, Berlin, Heidelberg, 2008. Springer. URL: https://doi.org/10.1007/978-3-540-79124-9_10.
  69. Qiuping Yi and Jeff Huang. Concurrency verification with maximal path causality. In ESEC/FSE 2018, pages 366-376, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3236024.3236048.
  70. Hengbiao Yu, Zhenbang Chen, Xianjin Fu, Ji Wang, Zhendong Su, Jun Sun, Chun Huang, and Wei Dong. Symbolic verification of message passing interface programs. In ICSE 2020, pages 1248-1260, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3377811.3380419.
  71. Xinhao Yuan, Junfeng Yang, and Ronghui Gu. Partial order aware concurrency sampling. In Hana Chockler and Georg Weissenbacher, editors, CAV 2018, pages 317-335, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-96142-2_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