Just Verification of Mutual Exclusion Algorithms with (Non-)Blocking and (Non-)Atomic Registers
This work addresses verification challenges for mutual exclusion algorithms in concurrent systems, but it is incremental as it applies existing methods to specific algorithm variants.
The paper verifies the correctness of mutual exclusion algorithms using model checking with shared read/write registers, including atomic and non-atomic variants, and employs justness as a completeness criterion to address liveness properties, demonstrating violations and suggesting improvements in some cases.
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.