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 is in preparation. It presents two versions. In either case, we present the PVS dump file for PVS users to inspect, and for the non-PVS users the PVS theory for safety (which is also in the dump, but which 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.

In either case, the dump contains three theories, one for the safety of the algorithm, one for progress, and an auxiliary theories about integer functions.

Comments and questions are welcome.
Back to my home page.
Wim H. Hesselink

Last modified: Mon Feb 7 11:18:39 CET 2011