MEA: A Framework for Model Checking of Mutual Exclusion Algorithms Focusing on Atomicity

The mutual exclusion problem is a classic and essential problem in computer science. Since its inception, many related algorithms and variants have been proposed. However, finding the atomicity requirement of mutual exclusion algorithms remains challenging. In this paper, we proposed a model-checking framework called MEA to solve this issue, which is implemented in Maude. MEA provides a workflow to model a mutual exclusion algorithm and can easily perform verification. We use two classic mutual exclusion algorithms as examples to elaborate on how it works. Both two cases denote that MEA is capable of basic modeling of mutual exclusion algorithms focusing on atomicity.