Unifying Weak Memory Verification Using Potentials

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.