Just Verification of Mutual Exclusion Algorithms

2025/07/17 by Rob van Glabbeek, van Glabbeek, Rob, Bas Luttik +3
Computer Science · Biochemistry, Genetics and Molecular Biology · #Distributed systems and fault tolerance #DNA and Biological Computing #Formal Methods in Verification

paper · pdf · doi:10.48550/arxiv.2507.13198

Abstract

We verify the correctness of a variety of mutual exclusion algorithms through model checking. We look at algorithms where communication is via shared read/write registers, where those registers can be atomic or non-atomic. For the verification of liveness properties, it is necessary to assume a completeness criterion to eliminate spurious counterexamples. We use justness as completeness criterion. Justness depends on a concurrency relation; we consider several such relations, modelling different assumptions on the working of the shared registers. We present executions demonstrating the violation of correctness properties by several algorithms, and in some cases suggest improvements.

Citations

• Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers
• Tutorial: Designing Distributed Software in mCRL2
• Justness: A Completeness Criterion for Capturing Liveness Properties
• Progress, Justness and Fairness in Modal μ-Calculus Formulae

Related

• Memory-Anonymous Starvation-Free Mutual Exclusion: Possibility and Impossibility Results
• Two Mutual Exclusion Algorithms for Shared Memory
• Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers
• Parameterized safety verification of round-based shared-memory systems
• Deconstructing Queue-Based Mutual Exclusion