Trace-based derivation of a scalable lock-free stack algorithm

DOI10.1007/S00165-008-0092-5MaRDI QIDQ1019022zbMATH OpenOpenAlexFDO

Authors Lindsay Groves, Robert 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

zbMATH Keywords

elimination algorithmelimination processLipton's reduction method

Mathematics Subject Classification ID

Nonnumerical algorithms (68W05)

Recommendations

• A scalable lock-free stack algorithm
• Computer Aided Verification
• A general lock-free algorithm using compare-and-swap
• Formal verification of a lock-free stack with hazard pointers

Cites work

• scientific article; zbMATH DE number 996442 (Why is no real title available?)
• scientific article; zbMATH DE number 42431 (Why is no real title available?)
• scientific article; zbMATH DE number 497680 (Why is no real title available?)
• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• A refinement calculus for shared-variable parallel and distributed programming
• A scalable lock-free stack algorithm
• Atomizer: A dynamic atomicity checker for multithreaded programs
• Data Refinement
• Data refinement by calculation
• Distributed cooperation with action systems
• Encoding, decoding and data refinement
• Formal Techniques for Networked and Distributed Systems – FORTE 2004
• Forward and backward simulations. I. Untimed Systems
• Nonblocking algorithms and preemption-safe locking on multiprogrammed shared memory multiprocessors
• Practical implementations of non-blocking synchronization primitives
• Randomized wait-free concurrent objects (extended abstract)
• Reduction
• Relational concurrent refinement
• The Rely-Guarantee method for verifying shared variable concurrent programs

Cited in

(6)

• Reuse, don't recycle: transforming lock-free algorithms that throw away descriptors
• Proving linearizability with temporal logic
• A scalable lock-free stack algorithm
• A sound and complete proof technique for linearizability of concurrent data structures
• A general lock-free algorithm using compare-and-swap
• A general technique for proving lock-freedom

Describes a project that uses

Uses Software

• Z
• Atomizer
• PVS

This page was built for publication: Trace-based derivation of a scalable lock-free stack algorithm

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