A queue based mutual exclusion algorithm

A. Aravind, W.H.A. Hesselink

Research output: Contribution to JournalArticleAcademicpeer-review

175 Downloads (Pure)


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. © 2008 Springer-Verlag.
Original languageEnglish
Pages (from-to)73-86
JournalActa Informatica
Issue number1
Publication statusPublished - 2009

Bibliographical note

Times Cited: 0


Dive into the research topics of 'A queue based mutual exclusion algorithm'. Together they form a unique fingerprint.

Cite this