We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
A queue based mutual exclusion algorithm.
- Authors
Aravind, Alex; Hesselink, Wim
- Abstract
A new elegant and simple algorithm for mutual exclusion of N processes is proposed. It only requires shared variables in a memory model where shared variables need not be accessed atomically. We prove mutual exclusion by reformulating the algorithm as a transition system (automaton), and applying simulation of automata. The proof has been verified with the higher-order interactive theorem prover PVS. Under an additional atomicity assumption, the algorithm is starvation free, and we conjecture that no competing process is passed by any other process more than once. This conjecture was verified by model checking for systems with at most five processes.
- Subjects
ALGORITHMS; MATHEMATICAL variables; MATHEMATICAL models; ROBOTS; SIMULATION methods &; models
- Publication
Acta Informatica, 2009, Vol 46, Issue 1, p73
- ISSN
0001-5903
- Publication type
Article
- DOI
10.1007/s00236-008-0086-z