Verification of Hardware Locks

A variation of Anderson's Spinlock

In 1990, T. E. Anderson introduced a spinlock algorithm in which each waiting thread is waiting at its own slot in a shared Boolean array of size N, where N is the maximum number of concurrently competing threads. The algorithm uses the modulo operator to reduce integers to indices in this array. The modulo operator is not efficient if N is not a power of 2. If N is not a divisor of maxint+1, overflow leads to errors. Therefore, a variation of the algorithm is proposed, in which the main shared integer variable is reset after every Nth call of its incrementation. The correctness of the implementation is verified by means of invariants. A paper is in preparation. A PVS proof script is available.

CLH: Craig, Landin, Hagersten

The simplest queuing hardware lock for an arbitrary number of threads is CLH. It uses a single special hardware instruction, viz. fetch-and-store (i.e. swap). It has less than ten lines, but its proof needs some thirty invariants. A paper is in preparation. The proof is verified with the proof assistant PVS. A PVS proof script is available.

Verifying MCS for mutual exclusion

The MCS algorithm for mutual exclusion was proposed by Mellor-Crummey and Scott in "Algorithms for Scalable Synchronization on shared-memory Multiprocessors", ACM Transactions on Computer Systems 9: 21-65, 1991. It is a hardware lock, because it uses fetch-and-store and compare-and-swap instructions. The algorithm is verified here by means of history variables and invariants. A paper is in preparation. A PVS proof script is available.

In the same paper, the authors propose a second version, MCS2, which uses the same Acquire function but a different Release function. While MCS proper uses a compare-and-swap instruction in Release, MCS2 simplifies this to a fetch-and-store. This destroys the FIFO behaviour, and makes the algorithm much more complicated. The proof of mutual exclusion is straightforward but cumbersome. The proof of absence of deadlock is a challenge. The algorithm does allow starvation of threads. A paper is in preparation. A PVS proof script is available.

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

Last modified: Thu Dec 30 13:28:43 CET 2021