Mutual exclusion by four shared bits with not more than quadratic complexity

• Verification of the mutual exclusion algorithm of Lycklama–Hadzilacos–Aravind.
• The verification is complete, and completely assertional.
• The first-come-first-served property, progress, and fault tolerance are proved.
• We introduce a measure of concurrent complexity related to UNITY.
• The concurrent complexity of the algorithm is proved to be at most quadratic.

For years, the mutual exclusion algorithm of Lycklama and Hadzilacos (1991) [21] was the optimal mutual exclusion algorithm with the first-come-first-served property, with a minimal number of (non-atomic) communication variables (5 bits per thread). Recently, Aravind published an improvement of it, which uses 4 bits per thread and has simplified waiting conditions. This algorithm is extended here with fault tolerance, and it is verified by assertional methods, using the proof assistant PVS. Progress is proved by means of UNITY logic. The paper proposes a new measure of concurrent time complexity, and proves that the concurrent complexity for throughput of the present algorithm is not more than quadratic in the number of threads.