A formal reduction for lock-free parallel algorithms

DOI10.1007/978-3-540-27813-9_4MaRDI QIDQ5312931zbMATH OpenOpenAlexFDO

Authors Hui Gao, W. H. Hesselink

Publication date 25 August 2005

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

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

zbMATH Keywords

Distributed algorithmsLock-freeRefinement mappingSimulation

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15)

Recommendations

• A general lock-free algorithm using compare-and-swap
• A general technique for proving lock-freedom
• Lock-free dynamic hash tables with open addressing
• Lock-free parallel and concurrent garbage collection by mark\&sweep

Cited in

(14)

• A general technique for proving lock-freedom
• Trace-based derivation of a scalable lock-free stack algorithm
• Lock coarsening: Eliminating lock overhead in automatically parallelized object-based programs
• Lock-free dynamic hash tables with open addressing
• Designing irregular parallel algorithms with mutual exclusion and lock-free protocols
• Efficient and practical constructions of LL/SC variables
• Verifying Lock-Freedom Using Well-Founded Orders
• Characterizing the performance of algorithms for lock-free objects
• The repeat offender problem: A mechanism for supporting dynamic-sized, lock-free data structures
• Simulation Refinement for Concurrency Verification
• Distributed Computing – IWDC 2005
• Proving a non-blocking algorithm for process renaming with TLA\textsuperscript{+}
• Lock-free parallel and concurrent garbage collection by mark\&sweep
• A general lock-free algorithm using compare-and-swap

Describes a project that uses

Uses Software

• PVS

This page was built for publication: A formal reduction for lock-free parallel algorithms

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