Many famous mutual exclusion algorithms, such as Dekker’s algorithm and Peterson’s algorithm are designed for a shared-memory setting. Such algorithms have been studied and verified using the mCRL2 toolset.
For mutual exclusion in a distributed system, also several algorithms have been designed. The first algorithm is Lamport’s distributed mutual exclusion algorithm , which uses global clocks to order the messages. The Ricart-Agrawala algorithm  is an optimization of this.
In this project, you investigate the following:
- Formalize Lamport’s distributed mutual exclusion algorithm using mCRL2, for a small number of nodes (e.g. 3 nodes).
- Identify the requirements that the algorithm should satisfy, and formalize these using the modal mu-calculus.
- Verify whether your model of the algorithm satisfies the requirements.
If time permits, you can also investigate the Ricart-Agrawala algorithm.
 Groote, J.F., Keiren, J.J.A.: Tutorial: Designing Distributed Software in mCRL2. In: Peters, K. and Willemse, T.A.C. (eds.) Formal Techniques for Distributed Objects, Components, and Systems., pp. 226-243. Springer International Publishing, Cham (2021). Invited tutorial paper.  Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM. 21, 7, 558-565 (1978).  Ricart, G., Agrawala, A.K.: An optimal algorithm for mutual exclusion in computer networks. Commun. ACM. 24, 1, 9-17 (1981).