Modeling and Formal Verification of a Distributed Mutual Exclusion Algorithm

This paper presents the modeling and verification of a fully anonymous Mutual Exclusion (ME) algorithm, which implies that processes and memory are indistinguishable. The study utilizes Colored Petri Nets (CPN) to model the ME algorithm hierarchically, comprising low and top levels. Analysis of the state space diagram demonstrates that typically, only one process enters the critical section while others wait. Additionally, the study shows that different processes identify an arbitrary in-memory register with distinct identifiers. However, it reveals a potential deadlock scenario where two processes simultaneously acquire an equal number of registers and fail to release them, leading to deadlock. This paper presents the first modeling and verification of an ME algorithm using state-space analysis, highlighting the novelty of employing colored Petri nets. The presented model, encapsulating the essential property of full anonymity, can serve as a foundation for modeling similar distributed algorithms, thus establishing its significance as a reference framework in this domain.