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

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)

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)

• Wait-free linearization with an assertional proof
• A mechanized refinement proof of the Chase-Lev deque using a proof system
• Wait-free linearization with a mechanical proof
• Strict linearizability and abstract atomicity
• 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
• Using refinement calculus techniques to prove linearizability
• Proving linearizability using forward simulations
• Characterizing progress properties of concurrent objects via contextual refinements
• Comparison Under Abstraction for Verifying Linearizability
• Making Linearizability Compositional for Partially Ordered Executions
• Intermediate value linearizability: a quantitative correctness criterion
• Analysing lock-free linearizable datatypes using CSP
• Relating trace refinement and linearizability
• 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)