Work done together with Peter A. Buhr and David Dice. It resulted in the paper "Fast mutual exclusion by the Triangle algorithm. Concurrency and Computation: Practice and Experience (in print, April 2017). DOI: 10.1002/cpe.4183".
Lamport (ACM TOPLAS 5 (1987) 1-11) designed and published the first fast mutual exclusion algorithm for N threads. Here fast means that, in the absence of contention, execution of the entry and exit protocols requires a number of atomic read and write operations that is independent of N. For Lamport's algorithm this number was 7. Lamport's algorithm has the disadvantage that it allows starvation: it is possible that a thread remains eternally in the entry protocol because it is infinitely often overtaken by competing threads. The Triangle algorithm is a starvation-free fast mutual exclusion algorithm, based on a mild variation of Lamport's fast algorithm, in combination with a starvation-free tournament algorithm and a starvation-free binary algorithm. A paper is in preparation. The verification is contained in a gzipped PVS dump file. The proof of safety is not much more than the verification of Lamport's algorithm. The verification of starvation-freedom is done in an axiomatic version of UNITY.
In the absence of contention, the algorithm needs 12 read and write operations. It is therefore fast, but not as fast as Lamport's algorithm. In the presence of contention it outperforms almost all software algorithms for mutual exclusion that we know of, and some hardware solutions as well.
Comments and questions are welcome.
Back to my home page.