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