Elevator algorithms for high-contention mutual exclusion

Work done with Peter A. Buhr and David Dice.

Elevator algorithms for mutual exclusion are based on the idea that the thread in the critical section chooses his successor when it leaves the critical section. This can be done in a more efficient way than when the threads must themselves work for the competition. Of course, the idea requires a data structure where threads can announce that they are waiting, and arbitration for the case that new competing threads arrive when there is no thread in the critical section.

The idea is due to Attiya, Hendler, and Levy [PODC '13], who proposed a tree+queue for the data structure and an algorithm with two compare-and-swap (CAS) operations for the arbitration. We propose several variations. These have been tested with concurrent C. The performance compares well with all known software mutual exclusion algorithms, and also with the hardware-assisted solution MCS of Mellor-Crummey and Scott. A paper is in preparation.

Our variations are at three choice points.
1. The tree-queue datastructure. We propose an improvement of the tree-queue data structure of Attiya e.a. in which the tree is inspected at fewer points. Alternatively, the tree-queue can be replaced by a circular list. This is much simpler, and in the case of maximal contention, it is more efficient. It is less efficient when contention is moderate or minimal.
2. Arbitration. We propose arbitration by means of a single CAS operation, or by a variation of Lamport's Fast mutual exclusion algorithm (1987), or by a version of Burns-Lamport.
3. Remote memory references (RMRs). The paper of Attiyah e.a. emphasizes that their solution has very few remote memory references. The choice here is whether or not to include this feature.

Several of our algorithms are verified with the proof assistant PVS. Although the three choice points are orthogonal, we have not been able to prove them all together in a modular fashion. We therefore only provide a selection of the available proof scripts (the simplest case and the most difficult one).

• Proof script for the simple CAS elevator with a circular list, without RMR optimization.
• Proof script for the Tree LF Flag elevator, i.e., the version with RMR optimization, and with arbitration done by Lamport's Fast algorithm.

Comments and questions are welcome.
Back to my home page.
Last modified: 10 June 2017.