TSO-to-TSO linearizability is undecidable

DOI10.1007/S00236-017-0305-6zbMath1408.68104OpenAlexW2766394693MaRDI QIDQ1629746

Chao Wang, Yi Lv, Peng Wu

Publication date: 12 December 2018

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00236-017-0305-6

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Uses Software

• Line-up

Cites Work

• Unnamed Item
• Model-checking of correctness conditions for concurrent objects
• Bounded TSO-to-SC Linearizability Is Decidable
• Tractable Refinement Checking for Concurrent Objects
• Concurrent Library Correctness on the TSO Memory Model
• Library abstraction for C/C++ concurrency
• Reasoning Algebraically About Refinement on TSO Architectures
• TSO-to-TSO Linearizability Is Undecidable
• Abstraction for Concurrent Objects
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Show No Weakness: Sequentially Consistent Specifications of TSO Libraries
• On the verification problem for weak memory models
• The Java memory model
• Verifying Concurrent Programs against Sequential Specifications
• Mathematizing C++ concurrency

This page was built for publication: TSO-to-TSO linearizability is undecidable