Trace-based derivation of a scalable lock-free stack algorithm
From MaRDI portal
Publication:1019022
DOI10.1007/s00165-008-0092-5zbMath1165.68064OpenAlexW1996684662MaRDI QIDQ1019022
Lindsay Groves, Robert J. Colvin
Publication date: 27 May 2009
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-008-0092-5
Related Items
A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures, Proving linearizability with temporal logic, A general technique for proving lock-freedom
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A scalable lock-free stack algorithm
- Relational concurrent refinement
- Data refinement by calculation
- Atomizer: A dynamic atomicity checker for multithreaded programs
- Nonblocking algorithms and preemption-safe locking on multiprogrammed shared memory multiprocessors
- The Rely-Guarantee method for verifying shared variable concurrent programs
- A refinement calculus for shared-variable parallel and distributed programming
- Forward and backward simulations. I. Untimed Systems
- Distributed cooperation with action systems
- Reduction
- Data Refinement
- Randomized wait-free concurrent objects (extended abstract)
- Practical implementations of non-blocking synchronization primitives
- Formal Techniques for Networked and Distributed Systems – FORTE 2004
- Encoding, decoding and data refinement
