A general technique for proving lock-freedom

DOI10.1016/j.scico.2008.09.013zbMath1157.68024OpenAlexW1973894849MaRDI QIDQ1001810

Brijesh Dongol, Robert J. Colvin

Publication date: 19 February 2009

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2008.09.013

zbMATH Keywords

verificationtemporal logicconcurrencylock-free programs

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Related Items

Transactional memory

Uses Software

• PVS
• CalcCheck
• UNITY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A general lock-free algorithm using compare-and-swap
• Trace-based derivation of a scalable lock-free stack algorithm
• Nonblocking algorithms and preemption-safe locking on multiprogrammed shared memory multiprocessors
• Verifying Lock-Freedom Using Well-Founded Orders
• Proving Linearizability Via Non-atomic Refinement
• Verification of temporal properties
• Practical implementations of non-blocking synchronization primitives
• Formal Techniques for Networked and Distributed Systems – FORTE 2004