This work gives an assertional verification of a simplification of
the mutual exclusion algorithm of Lycklama-Hadzilacos (ACM TOPLAS 13
(1991) 558-576). The algorithm guarantees mutual exclusion with the
first-come-first-served property for N threads that communicate by
shared memory. A paper
Verifying a Simplification of Mutual Exclusion by
Lycklama-Hadzilacos has appeared in Acta Informatica **50** (3)
(2013) 199-228.
The final
publication is available at link.springer.com. It presents two
versions. In either case, we present the PVS dump file for inspection
by users of PVS (version 5.0). For the non-PVS users, we provide the
PVS theory for safety (which is also in the dump, but which is
readable without the PVS system).

- a simple version that uses four nonatomic Boolean shared variables but has possibly bad performance when N is large: dump file and safety theory.
- a version with five nonatomic Boolean shared variables and possibly better performance for large N: dump file and safety theory.

Concurrently with my exploration above, my former co-author Alex Aravind also investigated and improved the algorithm of Lycklama-Hadzilacos in a paper "Simple, space-efficient, and fairness improved FCFS mutual exclusion algorithms", which appeared in J. Parallel Distrib. Comput. 73(8): 1029-1038 (2013). His solution is more elegant than mine. It also needs only 4 nonatomic bits per thread. I have extended his algorithm with fault tolerance and fault recovery, and proved this extension by assertional means with the proof assistant PVS. A paper Mutual exclusion by four shared bits with not more than quadratic complexity appears in Science of Computer Programming, DOI:10.1016/j.scico.2015.01.001. Users of PVS can inspect the verification, a gzipped dump file.

The most interesting addition of mine is the idea of *concurrent
time complexity*. First, partition the steps of the algorithm
into two classes: the environment steps that model the task of the
algorithm, and the forward steps that model the solution. Define
a *round* to be a finite execution in which each of the forward
steps is at some time either disabled or taken. If the concurrent
time complexity of reaching some goal Q from precondition P is k, this
implies that every execution that starts in a state where P holds and
contains a concatenation of k rounds, contains a state where Q holds.
For the algorithm, the result is that the concurrent time complexity
of entering a critical section n times, is in the order of A*n, where
A is a constant that depends quadratically on the number of
threads.

Comments and questions are welcome.

Back to my home page.

Wim H. Hesselink