# 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