Decidability of liveness for concurrent objects on the TSO memory model

DOI10.1007/978-3-031-21213-0_10MaRDI QIDQ6168984zbMATH OpenFDO

Authors Chao Wang, Gustavo Petri, Yi Lv, Teng Long, Zhiming Liu

Publication date 10 August 2023

Published in Dependable Software Engineering. Theories, Tools, and Applications (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2107.09930

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

• TSO-to-TSO linearizability is undecidable
• TSO-to-TSO linearizability is undecidable
• Bounded TSO-to-SC linearizability is decidable
• On the verification problem for weak memory models
• Overcoming memory weakness with unified fairness. Systematic verification of liveness in weak memory models

Cites work

• A variant of a recursively unsolvable problem
• Characterizing progress properties of concurrent objects via contextual refinements
• Checking and enforcing robustness against TSO
• Concurrent Library Correctness on the TSO Memory Model
• Handbook of model checking
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Mathematizing C++ concurrency
• On some variants of Post's correspondence problem
• On the verification problem for weak memory models
• Show no weakness: sequentially consistent specifications of TSO libraries
• The Java memory model
• TSO-to-TSO linearizability is undecidable
• Undecidable verification problems for programs with unreliable channels

Cited in

(1)

• Concurrent Library Correctness on the TSO Memory Model

This page was built for publication: Decidability of liveness for concurrent objects on the TSO memory model

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6168984)