Formal verification of a practical lock-free queue algorithm

DOI10.1007/978-3-540-30232-2_7MaRDI QIDQ5464482zbMATH OpenOpenAlexFDO

Authors Simon Doherty, Lindsay Groves, Victor Luchangco, Mark Moir

Publication date 18 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b100576

Mathematics Subject Classification ID

Data structures (68P05) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Formal verification of the MCS list-based queueing lock
• Automatically verifying concurrent queue algorithms
• Temporal Logic Verification of Lock-Freedom
• Verifying concurrent data structures by simulation
• A sound and complete proof technique for linearizability of concurrent data structures

Cited in

(20)

• A general technique for proving lock-freedom
• Trace-based derivation of a scalable lock-free stack algorithm
• Mechanized proofs of opacity: a comparison of two techniques
• Analysing lock-free linearizable datatypes using CSP
• An optimistic approach to lock-free FIFO queues
• Verifying correctness of persistent concurrent data structures: a sound and complete method
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• Automatically verifying concurrent queue algorithms
• Verifying concurrent data structures by simulation
• A sound and complete proof technique for linearizability of concurrent data structures
• Formal verification of a lock-free stack with hazard pointers
• Nonblocking Algorithms and Backward Simulation
• Formal verification of the MCS list-based queueing lock
• Model checking simulation rules for linearizability
• Towards formally specifying and verifying transactional memory
• Proving linearizability with temporal logic
• Verification of Flat FIFO Systems
• Making Linearizability Compositional for Partially Ordered Executions
• Verifying correctness of persistent concurrent data structures

Describes a project that uses

Uses Software

• PVS

This page was built for publication: Formal verification of a practical lock-free queue algorithm

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5464482)