Proving Linearizability Via Non-atomic Refinement

DOI10.1007/978-3-540-73210-5_11zbMATH Open1213.68370OpenAlexW2104046157MaRDI QIDQ3608884FDOQ3608884

Authors: John Derrick, Gerhard Schellhorn, Heike Wehrheim 

Publication date: 6 March 2009

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

Full work available at URL: https://doi.org/10.1007/978-3-540-73210-5_11

Recommendations

• Using refinement calculus techniques to prove linearizability
• Proving linearizability with temporal logic
• Proving linearizability using forward simulations
• A sound and complete proof technique for linearizability of concurrent data structures
• Strict linearizability and abstract atomicity

zbMATH Keywords

CSPrefinementlinearizabilityObject-Zconcurrent access

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)

Cited In (9)

• Proving linearizability with temporal logic
• Stabilization-preserving atomicity refinement
• TSO-to-TSO linearizability is undecidable
• Shape-Value Abstraction for Verifying Linearizability
• Relational concurrent refinement. III: Traces, partial relations and automata
• Comparison Under Abstraction for Verifying Linearizability
• Making Linearizability Compositional for Partially Ordered Executions
• Intermediate value linearizability: a quantitative correctness criterion
• A general technique for proving lock-freedom

This page was built for publication: Proving Linearizability Via Non-atomic Refinement

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