Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos

DOI10.1007/S00236-013-0178-2MaRDI QIDQ2377304zbMATH OpenOpenAlexFDO

Authors W. H. Hesselink

Publication date 28 June 2013

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00236-013-0178-2

zbMATH Keywords

mutual exclusion algorithm

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Nonnumerical algorithms (68W05)

Recommendations

• A queue based mutual exclusion algorithm
• Nonatomic dual bakery algorithm with bounded tokens
• scientific article; zbMATH DE number 1860625
• Peterson's mutual exclusion algorithm revisited
• scientific article; zbMATH DE number 2080213

Cites work

• A general lock-free algorithm using compare-and-swap
• A mechanical proof of Segall's PIF algorithm
• A mechanically verified incremental garbage collector
• A New Approach to Proving the Correctness of Multiprocess Programs
• A new solution of Dijkstra's concurrent programming problem
• A queue based mutual exclusion algorithm
• An axiomatic basis for computer programming
• An axiomatic proof technique for parallel programs
• Atomic semantics of nonatomic programs
• Bounded concurrent timestamp systems using vector clocks
• Bounded time-stamps
• Concurrency verification. Introduction to compositional and noncompositional methods
• Distributed algorithms. 8th international workshop, WDAG 1994, Terschelling, The Netherlands, September 29 -- October 1, 1994. Proceedings
• Efficient and practical constructions of LL/SC variables
• scientific article; zbMATH DE number 996442 (Why is no real title available?)
• scientific article; zbMATH DE number 4082934 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 2080925 (Why is no real title available?)
• scientific article; zbMATH DE number 2089981 (Why is no real title available?)
• Lazy caching in TLA
• Lock-free dynamic hash tables with open addressing
• Lock-free parallel and concurrent garbage collection by mark\&sweep
• Nonatomic dual bakery algorithm with bounded tokens
• Nonatomic mutual exclusion with local spinning
• On interprocess communication. I: Basic formalism
• On interprocess communication. II: Algorithms
• Proving assertions about parallel programs
• Proving the Correctness of Multiprocess Programs
• Self-stabilizing systems in spite of distributed control
• Shared-memory mutual exclusion: major research trends since 1986
• Temporal verification of reactive systems: response
• The Black-White Bakery Algorithm and Related Bounded-Space, Adaptive, Local-Spinning and FIFO Algorithms
• The existence of refinement mappings
• The mutual exclusion problem
• The verified incremental design of a distributed spanning tree algorithm: Extended abstract
• Universal extensions to simulate specifications
• Using eternity variables to specify and prove a serializable database interface
• Verification of sequential and concurrent programs
• Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos
• Wait-free linearization with a mechanical proof

Cited in

(3)

• A queue based mutual exclusion algorithm
• Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos
• Correctness and concurrent complexity of the black-white bakery algorithm

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos

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