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.
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
@inproceedings{DBLP:conf/vmcai/BodenmullerDDSW24,
author = {Stefan Bodenm{\"{u}}ller and John Derrick and Brijesh Dongol and Gerhard Schellhorn and Heike Wehrheim},
editor = {Rayna Dimitrova and Ori Lahav and Sebastian Wolff},
title = {A Fully Verified Persistency Library},
booktitle = {Verification, Model Checking, and Abstract Interpretation - 25th International Conference, {VMCAI} 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
volume = {14500},
pages = {26--47},
publisher = {Springer},
year = {2024},
url = {https://doi.org/10.1007/978-3-031-50521-8\_2},
doi = {10.1007/978-3-031-50521-8\_2},
timestamp = {Fri, 26 Jan 2024 07:55:26 +0100},
biburl = {https://dblp.org/rec/conf/vmcai/BodenmullerDDSW24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
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
@article{DBLP:journals/corr/abs-2305-08486,
author = {Ori Lahav and Brijesh Dongol and Heike Wehrheim},
title = {Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)},
journal = {CoRR},
volume = {abs/2305.08486},
year = {2023},
url = {https://doi.org/10.48550/arXiv.2305.08486},
doi = {10.48550/ARXIV.2305.08486},
eprinttype = {arXiv},
eprint = {2305.08486},
timestamp = {Mon, 05 Feb 2024 20:18:40 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2305-08486.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
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
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{DBLP:conf/cav/LahavDW23,
author = {Ori Lahav and Brijesh Dongol and Heike Wehrheim},
editor = {Constantin Enea and Akash Lal},
title = {Rely-Guarantee Reasoning for Causally Consistent Shared Memory},
booktitle = {Computer Aided Verification - 35th International Conference, {CAV} 2023, Paris, France, July 17-22, 2023, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {13964},
pages = {206--229},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-37706-8\_11},
doi = {10.1007/978-3-031-37706-8\_11},
timestamp = {Fri, 22 Sep 2023 15:13:40 +0200},
biburl = {https://dblp.org/rec/conf/cav/LahavDW23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
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{DBLP:conf/fm/WehrheimBD23,
author = {Heike Wehrheim and Lara Bargmann and Brijesh Dongol},
editor = {Marsha Chechik and Joost{-}Pieter Katoen and Martin Leucker},
title = {Reasoning About Promises in Weak Memory Models with Event Structures},
booktitle = {Formal Methods - 25th International Symposium, {FM} 2023, L{\"{u}}beck, Germany, March 6-10, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14000},
pages = {282--300},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-27481-7\_17},
doi = {10.1007/978-3-031-27481-7\_17},
timestamp = {Sat, 11 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/fm/WehrheimBD23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
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{DBLP:conf/ifm/BargmannW23,
author = {Lara Bargmann and Heike Wehrheim},
editor = {Paula Herber and Anton Wijs},
title = {Lifting the Reasoning Level in Generic Weak Memory Verification},
booktitle = {iFM 2023 - 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13-15, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14300},
pages = {175--192},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-47705-8\_10},
doi = {10.1007/978-3-031-47705-8\_10},
timestamp = {Sun, 10 Dec 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ifm/BargmannW23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
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
@inproceedings{DBLP:conf/tase/BargmannW23,
author = {Lara Bargmann and Heike Wehrheim},
editor = {Cristina David and Meng Sun},
title = {View-Based Axiomatic Reasoning for {PSO}},
booktitle = {Theoretical Aspects of Software Engineering - 17th International Symposium, {TASE} 2023, Bristol, UK, July 4-6, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13931},
pages = {286--304},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-35257-7\_17},
doi = {10.1007/978-3-031-35257-7\_17},
timestamp = {Fri, 07 Jul 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tase/BargmannW23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
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
@article{DBLP:journals/corr/abs-2211-16330,
author = {Heike Wehrheim and Lara Bargmann and Brijesh Dongol},
title = {Reasoning about Promises in Weak Memory Models with Event Structures (Extended Version)},
journal = {CoRR},
volume = {abs/2211.16330},
year = {2022},
url = {https://doi.org/10.48550/arXiv.2211.16330},
doi = {10.48550/ARXIV.2211.16330},
eprinttype = {arXiv},
eprint = {2211.16330},
timestamp = {Fri, 02 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2211-16330.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
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
@article{DBLP:journals/jar/DalvandiDDW22,
author = {Sadegh Dalvandi and Brijesh Dongol and Simon Doherty and Heike Wehrheim},
title = {Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL},
journal = {J. Autom. Reason.},
volume = {66},
number = {1},
pages = {141--171},
year = {2022},
url = {https://doi.org/10.1007/s10817-021-09610-2},
doi = {10.1007/S10817-021-09610-2},
timestamp = {Fri, 21 Jan 2022 22:01:13 +0100},
biburl = {https://dblp.org/rec/journals/jar/DalvandiDDW22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
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
@article{10.1145/3545117,
author = {Doherty, Simon and Dalvandi, Sadegh and Dongol, Brijesh and Wehrheim, Heike},
title = {Unifying Operational Weak Memory Verification: An Axiomatic Approach},
year = {2022},
issue_date = {October 2022},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {23},
number = {4},
issn = {1529-3785},
url = {https://doi.org/10.1145/3545117},
doi = {10.1145/3545117},
journal = {ACM Trans. Comput. Logic},
month = {oct},
articleno = {27},
numpages = {39},
keywords = {Isabelle/HOL, Owicki-Gries, Hoare logic, verification, axiom hierarchy, Weak memory models}
