## Fast mutual exclusion by the Triangle Algorithm

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.

Last modified: 10 June 2017