Abstract Reasoning about concurrent programs executed on weak memory models is an inherently complex task. So far, existing proof calculi for weak memory models only cover safety properties. In this paper, we provide the first proof calculus for reasoning about liveness . Our proof calculus is based on Manna and Pnueli’s proof rules for response under weak fairness, formulated in linear temporal logic. Our extension includes the incorporation of memory fairness into rules as well as the usage of ranking functions defined over weak memory state. We have applied our reasoning technique to the Ticket lock algorithm and have proved it to guarantee starvation freedom under memory models Release-Acquire and Strong Coherence for any number of concurrent threads.

Weak memory models describe the semantics of concurrent programs in modern multicore architectures. As these semantics deviate from the commonly assumed model of sequential consistency, reasoning techniques like Owicki-Gries-style proof calculi need to be adapted to specific memory models. To avoid having to design a new proof calculus for every new memory model, a uniform approach for axiomatic reasoning has recently been proposed. This approach bases reasoning on memory-model independent axioms about thread views and how they are changed by program actions like reads and writes. It allows to prove program correctness based on axioms only. Such proofs are valid for all memory models instantiating the axioms. In this paper, we study instantiations of the axioms for two memory models, the Partial Store Order (PSO) and the Strong Release Acquire (SRA) model. We see that both models fulfil all but one axiom, a different one though. For PSO, the missing axiom refers to message-passing abilities of memory models; for SRA, the missing axiom refers to the independence of actions on executing threads. We discuss the consequences of these missing axioms and illustrate the reasoning technique on a specific litmus test.

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.