## Nonatomic Dual Bakery Algorithm with Bounded Tokens

This is joint work with Alex A. Aravind. It concerns a mutual
exclusion algorithm in which the threads (or processes) communicate by
bounded nonatomic shared variables. It is a variation of Lamport's
bakery algorithm (1974) and Taubenfeld's black-white bakery algorithm
(2004). The algorithm has appeared in:

A.A. Aravind, W.H. Hesselink:
Nonatomic Dual Bakery Algorithm with Bounded Tokens.
Acta Informatica **48** (2011) 67-96.

There are three PVS proof scripts:
one that proves mutual exclusion for a version of the algorithm
with atomic variables,
a second one in which vulnerable information is spread over more
shared variables (which are still atomic), and
a third one in which all shared variables are allowed to be safe
instead of atomic. This version also contains a full proof of
liveness under weak fairness. You can use PVS to inspect
them. First, *gunzip* the file. Start PVS, and *undump*
the file. This gives files adbak*, hadbak*, or nadbak*. You can now
inspect the files with extension pvs to see what is asserted, or call
PVS to prove them.

Comments and questions are welcome.

Back to my home page.

Wim H. Hesselink

Last modified: Tue Feb 7 12:31:09 CET 2012