A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
From MaRDI portal
Publication:2946743
DOI10.1145/2629496zbMath1354.68066OpenAlexW2017559473MaRDI QIDQ2946743
Gerhard Schellhorn, John Derrick, Heike Wehrheim
Publication date: 17 September 2015
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: http://eprints.whiterose.ac.uk/90972/1/main.pdf
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Data structures (68P05)
Related Items
Model Checking Simulation Rules for Linearizability, Mechanized proofs of opacity: a comparison of two techniques, Relating trace refinement and linearizability, Making Linearizability Compositional for Partially Ordered Executions, Proving Linearizability Using Partial Orders, Verifying correctness of persistent concurrent data structures: a sound and complete method, Verifying Opacity of a Transactional Mutex Lock, A Framework for Correctness Criteria on Weak Memory Models
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Completeness of fair ASM refinement
- Abstraction for concurrent objects
- The existence of refinement mappings
- A criterion for atomicity revisited
- Trace-based derivation of a scalable lock-free stack algorithm
- Forward and backward simulations. I. Untimed Systems
- Using refinement calculus techniques to prove linearizability
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs
- Atomic actions, and their refinements to isolated protocols
- Universal extensions to simulate specifications
- Aspect-Oriented Linearizability Proofs
- Formal Verification of a Lock-Free Stack with Hazard Pointers
- Simplifying Linearizability Proofs with Reduction and Abstraction
- Temporal Logic Verification of Lock-Freedom
- Reasoning about Optimistic Concurrency Using a Program Logic for History
- Modular Safety Checking for Fine-Grained Concurrency
- Nonblocking Algorithms and Backward Simulation
- Reduction
- Atomic snapshots of shared memory
- Data Refinement
- Verifying linearizability with hindsight
- Completeness of ASM Refinement
- A separation logic for refining concurrent objects
- Comparison Under Abstraction for Verifying Linearizability
- Formal Techniques for Networked and Distributed Systems – FORTE 2004
