Show no weakness: sequentially consistent specifications of TSO libraries

DOI10.1007/978-3-642-33651-5_3MaRDI QIDQ4909400zbMATH OpenOpenAlexFDO

Authors Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang

Publication date 13 March 2013

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-33651-5_3

Mathematics Subject Classification ID

Distributed systems (68M14)

Recommendations

• Concurrent Library Correctness on the TSO Memory Model
• A separation logic for fictional sequential consistency
• From total store order to sequential consistency: a practical reduction theorem
• Library abstraction for C/C++ concurrency
• Reasoning about TSO programs using reduction and abstraction

Cited in

(8)

• TSO-to-TSO linearizability is undecidable
• A separation logic for fictional sequential consistency
• Library abstraction for C/C++ concurrency
• Model checking simulation rules for linearizability
• A framework for correctness criteria on weak memory models
• Making Linearizability Compositional for Partially Ordered Executions
• Decidability of liveness for concurrent objects on the TSO memory model
• Linearizability on hardware weak memory models

This page was built for publication: Show no weakness: sequentially consistent specifications of TSO libraries

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