Document Open Access Logo

Compositional Correctness and Completeness for Symbolic Partial Order Reduction

Authors Åsmund Aqissiaq Arild Kløvstad , Eduard Kamburjan , Einar Broch Johnsen

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.9.pdf
  • Filesize: 0.75 MB
  • 16 pages

Document Identifiers

Author Details

Åsmund Aqissiaq Arild Kløvstad
  • University of Oslo, Norway
Eduard Kamburjan
  • University of Oslo, Norway
Einar Broch Johnsen
  • University of Oslo, Norway

Funding

This work was supported by the Research Council of Norway via SIRIUS (237898) and PeTWIN (294600).

Acknowledgements

The first author would like to thank Yannick Zakowski for help with Coq formatting and Erik Voogd for valuable insights on symbolic semantics.

Cite As Get BibTex

Åsmund Aqissiaq Arild Kløvstad, Eduard Kamburjan, and Einar Broch Johnsen. Compositional Correctness and Completeness for Symbolic Partial Order Reduction. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CONCUR.2023.9

Abstract

Partial Order Reduction (POR) and Symbolic Execution (SE) are two fundamental abstraction techniques in program analysis. SE is particularly useful as a state abstraction technique for sequential programs, while POR addresses equivalent interleavings in the execution of concurrent programs. Recently, several promising connections between these two approaches have been investigated, which result in symbolic partial order reduction: partial order reduction of symbolically executed programs. In this work, we provide compositional notions of completeness and correctness for symbolic partial order reduction. We formalize completeness and correctness for (1) abstraction over program states and (2) trace equivalence, such that the abstraction gives rise to a complete and correct SE, the trace equivalence gives rise to a complete and correct POR, and their combination results in complete and correct symbolic partial order reduction. We develop our results for a core parallel imperative programming language and mechanize the proofs in Coq.

Subject Classification

ACM Subject Classification
  • Theory of computation → Parallel computing models
Keywords
  • Symbolic Execution
  • Coq
  • Trace Semantics
  • Partial Order Reduction

Metrics

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

Supplementary Materials

References

  1. Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. Optimal dynamic partial order reduction. In Suresh Jagannathan and Peter Sewell, editors, Proc. 41st Annual Symposium on Principles of Programming Languages (POPL'14), pages 373-384. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535845.
  2. Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich, editors. Deductive Software Verification - The KeY Book - From Theory to Practice, volume 10001 of Lecture Notes in Computer Science. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-49812-6.
  3. Roberto Baldoni, Emilio Coppa, Daniele Cono D’elia, Camil Demetrescu, and Irene Finocchi. A survey of symbolic execution techniques. ACM Computing Surveys (CSUR), 51(3):1-39, 2018. Google Scholar
  4. Yves Bertot and Pierre Castéran. Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer, 2013. Google Scholar
  5. Frank S de Boer and Marcello Bonsangue. Symbolic execution formally explained. Formal Aspects of Computing, 33(4):617-636, 2021. Google Scholar
  6. 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 Deductive Software Verification: Future Perspectives, pages 313-338. Springer, 2020. Google Scholar
  7. Robert S. Boyer, Bernard Elspas, and Karl N. Levitt. SELECT - a formal system for testing and debugging programs by symbolic execution. In Martin L. Shooman and Raymond T. Yeh, editors, Proc. International Conference on Reliable Software 1975, pages 234-245. ACM, 1975. URL: https://doi.org/10.1145/800027.808445.
  8. Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Richard Draves and Robbert van Renesse, editors, Proc. 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008), pages 209-224. USENIX Association, 2008. URL: http://www.usenix.org/events/osdi08/tech/full_papers/cadar/cadar.pdf.
  9. Cristian Cadar and Koushik Sen. Symbolic execution for software testing: three decades later. Commun. ACM, 56(2):82-90, 2013. URL: https://doi.org/10.1145/2408776.2408795.
  10. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott, editors. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of Lecture Notes in Computer Science. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71999-1.
  11. Crystal Chang Din, Reiner Hähnle, Ludovic Henrio, Einar Broch Johnsen, Violet Ka I Pun, and Silvia Lizeth Tapia Tarifa. LAGC semantics of concurrent programming languages. arXiv preprint arXiv:2202.12195, 2022. Google Scholar
  12. Matthias Felleisen and Robert Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 103(2):235-271, 1992. URL: https://doi.org/10.1016/0304-3975(92)90014-7.
  13. Cormac Flanagan and Patrice Godefroid. Dynamic partial-order reduction for model checking software. In Proc. 32nd Symposium on Principles of Programming Languages (POPL'05), pages 110-121. ACM, 2005. URL: https://doi.org/10.1145/1040305.1040315.
  14. José Fragoso Santos, Petar Maksimović, Sacha-Élie Ayoun, and Philippa Gardner. Gillian, part i: a multi-language platform for symbolic execution. In Proc. 41st ACM Conference on Programming Language Design and Implementation (PLDI'20), pages 927-942, 2020. Google Scholar
  15. 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. Google Scholar
  16. Patrice Godefroid. Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. Springer, 1996. Google Scholar
  17. Patrice Godefroid and Pierre Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design, 2:149-164, 1993. Google Scholar
  18. Shmuel Katz and Zohar Manna. Towards automatic debugging of programs. ACM SIGPLAN Notices, 10(6):143-155, 1975. Google Scholar
  19. James C King. Symbolic execution and program testing. Communications of the ACM, 19(7):385-394, 1976. Google Scholar
  20. Xavier Leroy. Mechanized semantics. Course materials, 2020. URL: https://github.com/xavierleroy/cdf-mech-sem.
  21. Dorel Lucanu, Vlad Rusu, and Andrei Arusoaie. A generic framework for symbolic execution: A coinductive approach. Journal of Symbolic Computation, 80:125-163, 2017. SI: Program Verification. URL: https://doi.org/10.1016/j.jsc.2016.07.012.
  22. Petar Maksimović, Sacha-Élie Ayoun, José Fragoso Santos, and Philippa Gardner. Gillian, part ii: Real-world verification for JavaScript and C. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification, pages 827-850. Springer, 2021. Google Scholar
  23. Antoni Mazurkiewicz. Concurrent program schemes and their interpretations. DAIMI Report Series, 6(78), July 1977. URL: https://doi.org/10.7146/dpb.v6i78.7691.
  24. Benjamin C Pierce, A Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, A Tolmach, and B Yorgey. Software foundations, volume 2: Programming language foundations. 2017. Google Scholar
  25. César Rodríguez, Marcelo Sousa, Subodh Sharma, and Daniel Kroening. Unfolding-based partial order reduction. In Luca Aceto and David de Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, volume 42 of LIPIcs, pages 456-469. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2015.456.
  26. Grigore Rosu, Andrei Stefanescu, Stefan Ciobâcá, and Brandon M. Moore. One-path reachability logic. In Proc. 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'13), pages 358-367, 2013. URL: https://doi.org/10.1109/LICS.2013.42.
  27. José Fragoso Santos, Petar Maksimović, Théotime Grohens, Julian Dolby, and Philippa Gardner. Symbolic execution for JavaScript. In Proc. 20th International Symposium on Principles and Practice of Declarative Programming, PPDP '18. ACM, 2018. URL: https://doi.org/10.1145/3236950.3236956.
  28. Daniel Schemmel, Julian Büning, César Rodríguez, David Laprell, and Klaus Wehrle. Symbolic partial-order execution for testing multi-threaded programs. In International Conference on Computer Aided Verification, pages 376-400. Springer, 2020. Google Scholar
  29. Andrei Ştefănescu, Ştefan Ciobâcă, Radu Mereuta, Brandon M. Moore, Traian Florin Şerbănută, and Grigore Roşu. All-path reachability logic. In Gilles Dowek, editor, Rewriting and Typed Lambda Calculi, pages 425-440. Springer, 2014. Google Scholar
  30. Dominic Steinhöfel. Abstract execution: automatically proving infinitely many programs. PhD thesis, Technische Universität Darmstadt, 2020. Google Scholar
  31. Dominic Steinhöfel and Reiner Hähnle. The trace modality. In Dynamic Logic. New Trends and Applications, pages 124-140. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-38808-9_8.
  32. The Coq Development Team. The Coq proof assistant, September 2022. URL: https://doi.org/10.5281/zenodo.7313584.
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact