Concurrency Reasoning for Weak Memory

Participants:

Heike Wehrheim, Simon Doherty, Brijesh Dongol, Sadegh Dalvandi, Lara Bargmann

Funding:

German Research Council (DFG), 2021 - 2024

Concurrency Reasoning for Weak Memory

Program verification aims at formal proofs of program correctness with respect to specified properties. For parallel programs, correctness does not only depend on the program itself, but also on the memory model of the executing hardware. Many and multi core architectures possess so called weak (or relaxed) memory models which significantly influence the semantics of parallel programs. The majority of verification techniques developed so far are specialized to one such memory model.

The objective of this project is the development of a generic verification technique which allows to generate correctness proofs independent of a memory model and is then able to transfer a proof to some specific model. To this end, we want to set verification on an axiomatic basis capturing the operational behaviour of parallel programs common to memory models while abstracting from their technical differences. Based on this, we will develop (a) a language for property specification and (b) a proof calculus for parallel programs. By exemplarily showing the validity of our axioms for three memory models and the realization of a number of proof case studies, we intend to demonstrate the genericity of the approach.

Publications

  • [inproceedings] bibtex | Go to document Go to document
    S. Bodenmüller, J. Derrick, B. Dongol, G. Schellhorn, and H. Wehrheim, "A Fully Verified Persistency Library" in Proc. Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part II, 2024.
    doi: 10.1007/978-3-031-50521-8_2
  • L. Bargmann and H. Wehrheim, "View-Based Axiomatic Reasoning for PSO (Extended Version)" CoRR, vol. abs/2301.07967.
    doi: 10.48550/ARXIV.2301.07967
  • O. Lahav, B. Dongol, and H. Wehrheim, "Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)" CoRR, vol. abs/2305.08486.
    doi: 10.48550/ARXIV.2305.08486
  • L. Bargmann and H. Wehrheim, "Lifting the Reasoning Level in Generic Weak Memory Verification (Extended Version)" CoRR, vol. abs/2309.01433.
    doi: 10.48550/ARXIV.2309.01433
  • [inproceedings] bibtex | Go to document Go to document
    O. Lahav, B. Dongol, and H. Wehrheim, "Rely-Guarantee Reasoning for Causally Consistent Shared Memory" in Proc. Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I, 2023.
    doi: 10.1007/978-3-031-37706-8_11
  • [inproceedings] bibtex | Go to document Go to document
    H. Wehrheim, L. Bargmann, and B. Dongol, "Reasoning About Promises in Weak Memory Models with Event Structures" in Proc. Formal Methods - 25th International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, Proceedings, 2023.
    doi: 10.1007/978-3-031-27481-7_17
  • [inproceedings] bibtex | Go to document Go to document
    L. Bargmann and H. Wehrheim, "Lifting the Reasoning Level in Generic Weak Memory Verification" in Proc. iFM 2023 - 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13-15, 2023, Proceedings, 2023.
    doi: 10.1007/978-3-031-47705-8_10
  • [inproceedings] bibtex | Go to document Go to document
    L. Bargmann and H. Wehrheim, "View-Based Axiomatic Reasoning for PSO" in Proc. Theoretical Aspects of Software Engineering - 17th International Symposium, TASE 2023, Bristol, UK, July 4-6, 2023, Proceedings, 2023.
    doi: 10.1007/978-3-031-35257-7_17
  • H. Wehrheim, L. Bargmann, and B. Dongol, "Reasoning about Promises in Weak Memory Models with Event Structures (Extended Version)" CoRR, vol. abs/2211.16330.
    doi: 10.48550/ARXIV.2211.16330
  • S. Dalvandi, B. Dongol, S. Doherty, and H. Wehrheim, "Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL" J. Autom. Reason. vol. 66, iss. 1.
    doi: 10.1007/S10817-021-09610-2
  • S. Doherty, S. Dalvandi, B. Dongol, and H. Wehrheim, "Unifying Operational Weak Memory Verification: An Axiomatic Approach" ACM Trans. Comput. Logic, vol. 23, iss. 4.
    doi: 10.1145/3545117
(Changed: 12 Jul 2024)  | 
Zum Seitananfang scrollen Scroll to the top of the page