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.

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

Last modified: Tue Aug 17 16:23:07 CEST 2021