Nonatomic dual bakery algorithm with bounded tokens

DOI10.1007/S00236-011-0132-0MaRDI QIDQ766163zbMATH OpenOpenAlexFDO

Authors Alex A. Aravind, W. H. Hesselink

Publication date 23 March 2012

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://pure.rug.nl/ws/files/2523090/2011ActaInfAravind.pdf

zbMATH Keywords

bounded sizefirst-come-first-servemutual exclusionnonatomic shared variables

Mathematics Subject Classification ID

Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Distributed algorithms (68W15)

Review text

Recent systems such as smart-phones, network processors, graphic chips use memories which allow nonatomic accesses. This paper presents (for the first time) and proves (by using PVS) a mutual exclusion algorithm that only uses nonatomic shared variables. Furthermore, these shared variables are of bounded size.

Recommendations

• scientific article; zbMATH DE number 2089981
• A queue based mutual exclusion algorithm
• The \(k\)-bakery, local-spin \(k\)-exclusion using non-atomic reads and writes
• scientific article; zbMATH DE number 2080925
• scientific article; zbMATH DE number 1696665

Cites work

• A challenge for atomicity verification
• A fine-grained solution to the mutual exclusion problem
• A new solution of Dijkstra's concurrent programming problem
• A New Solution to Lamport's Concurrent Programming Problem Using Small Shared Variables
• A new solution to the critical section problem
• A queue based mutual exclusion algorithm
• Bounded time-stamps
• scientific article; zbMATH DE number 4082934 (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?)
• Myths about the mutual exclusion problem
• Nonatomic mutual exclusion with local spinning
• On interprocess communication. I: Basic formalism
• The Black-White Bakery Algorithm and Related Bounded-Space, Adaptive, Local-Spinning and FIFO Algorithms
• The existence of refinement mappings
• The mutual exclusion problem

Cited in

(8)

• A queue based mutual exclusion algorithm
• Highly-fair bakery algorithm using symmetric tokens
• Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos
• scientific article; zbMATH DE number 868108 (Why is no real title available?)
• Logical classification of distributed algorithms (Bakery algorithms as an example)
• Towards an automatic proof of the bakery algorithm
• Just verification of mutual exclusion algorithms
• Simple, space-efficient, and fairness improved FCFS mutual exclusion algorithms

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: Nonatomic dual bakery algorithm with bounded tokens

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