Decidability of liveness for concurrent objects on the TSO memory model
From MaRDI portal
Publication:6168984
DOI10.1007/978-3-031-21213-0_10zbMath1528.68073arXiv2107.09930MaRDI QIDQ6168984
Chao Wang, Gustavo Petri, Teng Long, Zhi-Ming Liu, Yi Lv
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
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)
Cites Work
- Undecidable verification problems for programs with unreliable channels
- On some variants of Post's correspondence problem
- Characterizing Progress Properties of Concurrent Objects via Contextual Refinements
- Concurrent Library Correctness on the TSO Memory Model
- TSO-to-TSO Linearizability Is Undecidable
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- Handbook of Model Checking
- Show No Weakness: Sequentially Consistent Specifications of TSO Libraries
- On the verification problem for weak memory models
- The Java memory model
- Checking and Enforcing Robustness against TSO
- Mathematizing C++ concurrency
- A variant of a recursively unsolvable problem
This page was built for publication: Decidability of liveness for concurrent objects on the TSO memory model
