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