Unifying Weak Memory Verification Using Potentials
Lara Bargmann, Brijesh Dongol, Heike Wehrheim · Lecture notes in computer science · 2024
Abstract Concurrency verification for weak memory models is inherently complex. Several deductive techniques based on proof calculi have recently been developed, but these are typically tailored towards a single memory model through specialised assertions and associated proof rules. In this paper, we propose an extension to the logic $${\textsf{Piccolo}}$$ Piccolo to generalise reasoning across different memory models. $${\textsf{Piccolo}}$$ Piccolo is interpreted on the semantic domain of thread potentials. By deriving potentials from weak memory model states, we can define the validity of $${\textsf{Piccolo}}$$ Piccolo formulae for multiple memory models. We moreover propose unified proof rules for verification on top of $${\textsf{Piccolo}}$$ Piccolo . Once (a set of) such rules has been shown to be sound with respect to a memory model $${\textsf{MM}} $$ MM , all correctness proofs employing this rule set are valid for $${\textsf{MM}}$$ MM . We exemplify our approach on the memory models $${\textsf{SC}}$$ SC , $${\textsf{TSO}}$$ TSO and $${\textsf{SRA}}$$ SRA using the standard litmus tests Message-Passing and IRIW.