Unifying Operational Weak Memory Verification: An Axiomatic Approach
Simon Doherty, Sadegh Dalvandi, Brijesh Dongol, Heike Wehrheim
Abstract
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.