1. Revisiting Mutual Exclusion by Lycklama-Hadzilacos

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.

2. Mutual Exclusion by Lycklama-Hadzilacos-Aravind

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