Decidability of Liveness on the TSO Memory Model

TL;DR

This paper investigates the decidability of various liveness properties of concurrent programs under the TSO memory model, revealing that most are undecidable except obstruction-freedom.

Contribution

It proves that several key liveness properties are undecidable on TSO, while identifying obstruction-freedom as decidable, advancing understanding of program verification under relaxed memory models.

Findings

Lock-freedom, wait-freedom, deadlock-freedom, starvation-freedom are undecidable on TSO.

Obstruction-freedom is decidable on TSO.

Results apply to finite state concurrent programs with bounded processes.

Abstract

An important property of concurrent objects is whether they support progress -a special case of liveness-guarantees, which ensure the termination of individual method calls under system fairness assumptions. Liveness properties have been proposed for concurrent objects. Typical liveness properties includelock-freedom,wait-freedom,deadlock-freedom,starvation-freedom and obstruction-freedom. It is known that the five liveness properties above are decidable on the Sequential Consistency (SC) memory model for a bounded number of processes. However, the problem of decidability of liveness for finite state concurrent programs running on relaxed memory models remains open. In this paper we address this problem for the Total Store Order (TSO) memory model,as found in the x86 architecture. We prove that lock-freedom, wait-freedom,deadlock-freedom and starvation-freedom are undecidable on TSO for a bounded number of processes, while obstruction-freedom is decidable.