When formally verifying the correctness of mutual exclusion algorithms it is often assumed that interaction with the shared registers (i.e., reads and writes) are atomic. For instance, it is well-known that the correctness of Peterson’s algorithm relies on the atomicity assumption. Already in 1986, however, Lamport argued that implementing atomic interaction with shared registers basically requires mutual exclusion at the lower level. To get out of this chicken-and-egg problem, we need mutual exclusion algorithms that do not rely on the atomicity assumption.

Myrthe Spronck and I have developed a method to verify mutual exclusion algorithms without the atomicity assumption with the mCRL2 toolset. We used our method to verify several mutual exclusion algorithms for which it was claimed (in print) that they were robust for non-atomic register interactions. We found that several of these algorithms are actually not as robust as they were claimed to be.