Document Open Access Logo

Automating Memory Model Metatheory with Intersections

Authors Aristotelis Koutsouridis , Michalis Kokologiannakis , Viktor Vafeiadis

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.33.pdf
  • Filesize: 0.85 MB
  • 16 pages

Document Identifiers

Author Details

Aristotelis Koutsouridis
  • MPI-SWS, Kaiserslautern and Saarbrücken, Germany
Michalis Kokologiannakis
  • MPI-SWS, Kaiserslautern and Saarbrücken, Germany
Viktor Vafeiadis
  • MPI-SWS, Kaiserslautern and Saarbrücken, Germany

Funding

This work was supported by a European Research Council (ERC) Consolidator Grant for the project "PERSIST" under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 101003349).

Acknowledgements

We would like to thank the anonymous reviewers for their feedback.

Cite AsGet BibTex

Aristotelis Koutsouridis, Michalis Kokologiannakis, and Viktor Vafeiadis. Automating Memory Model Metatheory with Intersections. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.33

Abstract

In the weak memory consistency literature, the semantics of concurrent programs is typically defined as a constraint on execution graphs, expressed in relational algebra. Prior work has shown that basic metatheoretic questions about memory models are decidable as long as they can be expressed as irreflexivity and emptiness constraints over Kleene Algebra with Tests (KAT), a condition that rules out practical memory models such the C/C++ and the Linux kernel models. In this paper, we extend these results to memory models containing arbitrary intersections with uninterpreted relations. We can thus automatically establish compilation correctness and derive efficient incremental consistency checkers for RC11, LKMM, and other memory models.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Concurrency
Keywords
  • Kleene Algebra
  • Weak Memory Models

Metrics

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

Supplementary Materials

References

  1. Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and Alan Stern. Frightening small children and disconcerting grown-ups: Concurrency in the Linux kernel. In ASPLOS 2018, pages 405-418, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3173162.3177156.
  2. Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst., 36(2):7:1-7:74, July 2014. URL: https://doi.org/10.1145/2627752.
  3. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. NetKAT: Semantic foundations for networks. In Suresh Jagannathan and Peter Sewell, editors, POPL 2014, 2014, pages 113-126. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535862.
  4. Paul Brunet and Damien Pous. Petri automata for Kleene allegories. In LICS 2015, pages 68-79. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.17.
  5. Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms, 3rd Edition. MIT Press, 2009. URL: http://mitpress.mit.edu/books/introduction-algorithms.
  6. Zoltán Ésik and L. Bernátsky. Equational properties of Kleene algebras of relations with conversion. Theor. Comput. Sci., 137(2):237-251, 1995. URL: https://doi.org/10.1016/0304-3975(94)00041-G.
  7. 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.
  8. Niels Bjørn Bugge Grathwohl, Dexter Kozen, and Konstantinos Mamouras. KAT + B! In Thomas A. Henzinger and Dale Miller, editors, LICS 2014, pages 44:1-44:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603095.
  9. C. A. R. Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman. Concurrent Kleene algebra. In Mario Bravetti and Gianluigi Zavattaro, editors, CONCUR 2009, volume 5710 of LNCS, pages 399-414. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_27.
  10. Peter Jipsen. Concurrent Kleene algebra with tests. In Peter Höfner, Peter Jipsen, Wolfram Kahl, and Martin Eric Müller, editors, RAMiCS 2014, volume 8428 of LNCS, pages 37-48. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-06251-8_3.
  11. Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. URL: https://doi.org/10.1016/0304-3975(94)90242-9.
  12. Tobias Kappé, Paul Brunet, Jurriaan Rot, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Kleene algebra with observations. In Wan J. Fokkink and Rob van Glabbeek, editors, CONCUR 2019, volume 140 of LIPIcs, pages 41:1-41:16. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.41.
  13. Tobias Kappé, Paul Brunet, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Concurrent Kleene algebra with observations: From hypotheses to completeness. CoRR, abs/2002.09682, 2020. URL: https://doi.org/10.48550/arXiv.2002.09682.
  14. Michalis Kokologiannakis, Ori Lahav, and Viktor Vafeiadis. Kater: Automating weak memory model metatheory and consistency checking. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571212.
  15. 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.
  16. Dexter Kozen. Kleene algebra with tests. ACM Trans. Program. Lang. Syst., 19(3), 1997. URL: https://doi.org/10.1145/256167.256195.
  17. 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.
  18. 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.
  19. Damien Pous, Jurriaan Rot, and Jana Wagemaker. On tools for completeness of Kleene algebra with hypotheses. CoRR, abs/2210.13020, 2022. URL: https://doi.org/10.48550/arXiv.2210.13020.
  20. Damien Pous and Valeria Vignudelli. Allegories: Decidability and graph homomorphisms. In Anuj Dawar and Erich Grädel, editors, LICS 2018, pages 829-838. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209172.
  21. Damien Pous and Jana Wagemaker. Completeness theorems for Kleene algebra with tests and top. CoRR, abs/2304.07190, 2023. URL: https://doi.org/10.48550/arXiv.2304.07190.
  22. SPARC International Inc. SPARC architecture manual - version 8. Prentice Hall, 1992. Google Scholar
  23. Jana Wagemaker, Nate Foster, Tobias Kappé, Dexter Kozen, Jurriaan Rot, and Alexandra Silva. Concurrent NetKAT - modeling and analyzing stateful, concurrent networks. In Ilya Sergey, editor, ESOP 2022, volume 13240 of LNCS, pages 575-602. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99336-8_21.
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 Imprint Privacy Contact