Towards Proving Liveness on Weak Memory (Extended Version)

TL;DR

The work addresses proving liveness for concurrent programs under weak memory by building a generic proof calculus based on MP rules for response properties and extending it with memory fairness and potential-based ranking. It uses the Piccolo logic to express weak-memory state and a lifting framework to instantiate proofs across memory models such as Release-Acquire and Strong Coherence, with formal soundness results. The approach is demonstrated by proving starvation freedom of the Ticket lock for any number of threads under RA and StrCOH, and is adaptable to parameterized programs via WELL-JP. This contributes a unified, model-agnostic method for liveness in weakly consistent concurrent systems with potential applicability to broader memory models and fairness notions.

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 StrongCoherence for any number of concurrent threads.

Figures (2)

• Figure 1: Program syntax
• Figure 2: Concurrent program Waiting; property at the end specifying thread $\mathtt{T}_2$ to terminate.