Distributed mutual exclusion protocols in mCRL2.

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 [2], which uses global clocks to order the messages. The Ricart-Agrawala algorithm [3] is an optimization of this.

In this project, you investigate the following:

1. Formalize Lamport’s distributed mutual exclusion algorithm using mCRL2, for a small number of nodes (e.g. 3 nodes).
2. Identify the requirements that the algorithm should satisfy, and formalize these using the modal mu-calculus.
3. Verify whether your model of the algorithm satisfies the requirements.

If time permits, you can also investigate the Ricart-Agrawala algorithm.

[1] 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. [2] Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM. 21, 7, 558-565 (1978). [3] Ricart, G., Agrawala, A.K.: An optimal algorithm for mutual exclusion in computer networks. Commun. ACM. 24, 1, 9-17 (1981).