| Autor: |
DOHERTY, SIMON, DALVANDI, SADEGH, DONGOL, BRIJESH, WEHRHEIM, HEIKE |
| Předmět: |
|
| Zdroj: |
ACM Transactions on Computational Logic; Oct2022, Vol. 23 Issue 4, p1-39, 39p |
| Abstrakt: |
In this article, we propose an approach to program verification using an abstract characterisation of weak memory models. Our approach is based on a hierarchical axiom scheme that captures the observational properties of a memory model. In particular, we show that it is possible to prove correctness of a program with respect to a particular axiom scheme, and we show this proof to suffice for any memory model that satisfies the axioms. Our axiom scheme is developed using a characterisation of weakest liberal preconditions for weak memory. This characterisation naturally extends to Hoare logic and Owicki-Gries reasoning by lifting weakest liberal preconditions (defined over read/write events) to the level of programs. We study three memory models (SC, TSO, and RC11-RAR) as example instantiations of the axioms, then we demonstrate the applicability of our reasoning technique on a number of litmus tests. The majority of the proofs in this article are supported by mechanisation within Isabelle/HOL. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Complementary Index |
| Externí odkaz: |
|
