Last week, Myrthe Spronck discussed mutual exclusion algorithms when using safe registers. In this week’s talk, I will stick with the topic of mutual exclusion algorithms, but switch back to using atomic registers. I will introduce Dekker’s algorithm for mutual exclusion. According to Dijkstra, this is the first algorithm to solve mutual exclusion between two processes.

In my talk, I will first discuss some of the historical context of Dekker’s algorithm. Subsequently, following Dijkstra’s 1962 paper “Over de sequentialiteit van procesbeschrijvingen” (EWD35), I will show how some simpler attempts fail, and, guided by the counterexamples that mCRL2 produces, develop this into Dekker’s algorithm.

During the talk, I will address several desirable requirements of mutual exclusion algorithms, as well as some modelling considerations.

This talk is based on the mCRL2 tutorial presentation “Designing Distributed Algorithms in mCRL2” that Jan Friso Groote and I will present at DisCoTec on June 14.