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 more than twenty invariants. A paper is in preparation. The proof is verified with the proof assistant PVS. A PVS proof script is available.

MCSH, a lock with the standard interface

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 very efficient synchronization algorithm that uses the hardware primitives fetch-and-store and compare-and-swap. It has the disadvantage, that it the calling thread has to provide a pointer to an allocated record. The standard interface for locks, say in a library, does not expect additional parameters. We are therefore developing a variation of MCS that has the standard interface, to be called MCSH. One key ingredient is that the pointer to an allocated record is replaced by the address of a variable in the locking procedure. This practice is known by practitioners, but rarely justified by verification. A second key ingredient of the design is a program transformation that eliminates an obstacle for the standard interface. This ingredient is also well-known but, as far as we know, only proved by hand waving. The correctness of MCSH is verified rigorously here, with the proof assistant PVS. A paper is in preparation. Available is a PVS proof script of the algorithm.

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

Last modified: Wed Jun 29 17:13:24 CEST 2022