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. The result appeared in our paper "MCSH, a lock with the
standard interface", ACM Transactions on Parallel Computing,
**10**:1–23, 2023. Available is a
PVS proof script of the algorithm.

The MCSH paper came on line in February 2023. Two months later Ting-Ching Li contacted us with an enhancement that reduces the number of assignments to shared variables. This enhanced algorithm is named MCSHLi. Its correctness is proved in the technical report whh596B, and supported by the PVS proof script. A paper is in preparation, with a sketch of the verification and the results of performance experiments.

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.

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.

Comments and questions are welcome.

Back to my home page.

Wim H. Hesselink