Proving Linearizability Via Non-atomic Refinement

DOI10.1007/978-3-540-73210-5_11MaRDI QIDQ3608884zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

concurrent accessCSPlinearizabilityObject-Zrefinement

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)

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

Cited in

(18)

• A general technique for proving lock-freedom
• TSO-to-TSO linearizability is undecidable
• Relating trace refinement and linearizability
• Analysing lock-free linearizable datatypes using CSP
• Using refinement calculus techniques to prove linearizability
• Proving linearizability using forward simulations
• A mechanized refinement proof of the Chase-Lev deque using a proof system
• Characterizing progress properties of concurrent objects via contextual refinements
• Shape-Value Abstraction for Verifying Linearizability
• Wait-free linearization with an assertional proof
• Wait-free linearization with a mechanical proof
• Proving linearizability with temporal logic
• Comparison Under Abstraction for Verifying Linearizability
• Strict linearizability and abstract atomicity
• Making Linearizability Compositional for Partially Ordered Executions
• Intermediate value linearizability: a quantitative correctness criterion
• Stabilization-preserving atomicity refinement
• Relational concurrent refinement. III: Traces, partial relations and automata

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)