Towards Proving Liveness on Weak Memory (Extended Version)

TL;DR

This paper introduces the first proof calculus for liveness properties in concurrent programs under weak memory models, extending existing safety-focused methods with fairness and ranking functions.

Contribution

It presents a novel proof calculus for liveness in weak memory models, incorporating memory fairness and ranking functions, and demonstrates its application on the Ticket lock algorithm.

Findings

Proved starvation freedom of Ticket lock under Release-Acquire and StrongCoherence models.

Extended proof rules to include memory fairness and ranking functions.

Validated the approach on concurrent algorithms for liveness guarantees.

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.