A sound and complete proof technique for linearizability of concurrent data structures
From MaRDI portal
Recommendations
Cites work
- A criterion for atomicity revisited
- A separation logic for refining concurrent objects
- Abstraction for concurrent objects
- Aspect-oriented linearizability proofs
- Atomic actions, and their refinements to isolated protocols
- Atomic snapshots of shared memory
- Comparison Under Abstraction for Verifying Linearizability
- Completeness of ASM refinement
- Completeness of fair ASM refinement
- Data Refinement
- Formal Techniques for Networked and Distributed Systems – FORTE 2004
- Formal verification of a lock-free stack with hazard pointers
- Forward and backward simulations. I. Untimed Systems
- scientific article; zbMATH DE number 1615985 (Why is no real title available?)
- scientific article; zbMATH DE number 996442 (Why is no real title available?)
- scientific article; zbMATH DE number 3943003 (Why is no real title available?)
- scientific article; zbMATH DE number 605917 (Why is no real title available?)
- scientific article; zbMATH DE number 1552508 (Why is no real title available?)
- Modular Safety Checking for Fine-Grained Concurrency
- Nonblocking Algorithms and Backward Simulation
- Reasoning about optimistic concurrency using a program logic for history
- Reduction
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs
- Simplifying linearizability proofs with reduction and abstraction
- Temporal Logic Verification of Lock-Freedom
- The existence of refinement mappings
- Trace-based derivation of a scalable lock-free stack algorithm
- Universal extensions to simulate specifications
- Using refinement calculus techniques to prove linearizability
- Verifying concurrent data structures by simulation
- Verifying linearizability with hindsight
Cited in
(34)- A constructive approach for proving data structures' linearizability
- Modular verification of concurrency-aware linearizability
- Mechanized proofs of opacity: a comparison of two techniques
- Relating trace refinement and linearizability
- \textsc{Poling}: SMT aided linearizability proofs
- Analysing lock-free linearizable datatypes using CSP
- Testing and verifying concurrent objects
- Using refinement calculus techniques to prove linearizability
- Verifying correctness of persistent concurrent data structures: a sound and complete method
- Proving linearizability using forward simulations
- A mechanized refinement proof of the Chase-Lev deque using a proof system
- Formalization and correctness of a concurrent linear hash structure algorithm using nested transactions and I/O automata
- Towards a thread-local proof technique for starvation freedom
- Aspect-oriented linearizability proofs
- Verifying concurrent data structures by simulation
- Proving linearizability using partial orders
- Proving Linearizability Via Non-atomic Refinement
- Model checking simulation rules for linearizability
- Local linearizability for concurrent container-type data structures
- Order out of chaos: proving linearizability using local views
- Checking linearizability of concurrent priority queues
- Wait-free linearization with an assertional proof
- Wait-free linearization with a mechanical proof
- Verifying opacity of a transactional mutex lock
- A framework for correctness criteria on weak memory models
- Aspect-oriented linearizability proofs
- An integrated specification and verification technique for highly concurrent data structures
- Proving linearizability with temporal logic
- Formal Techniques for Networked and Distributed Systems – FORTE 2004
- scientific article; zbMATH DE number 7774258 (Why is no real title available?)
- Making Linearizability Compositional for Partially Ordered Executions
- Verifying correctness of persistent concurrent data structures
- Visibility and separability for a declarative linearizability proof of the timestamped stack
- A compositional theory of linearizability
This page was built for publication: A sound and complete proof technique for linearizability of concurrent data structures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946743)
