Just Verification of Mutual Exclusion Algorithms with (Non-)Blocking and (Non-)Atomic Registers

TL;DR

This paper employs model checking to verify the correctness of mutual exclusion algorithms using shared registers, considering atomic and non-atomic cases, and explores various assumptions on register behavior.

Contribution

It introduces a verification framework that accounts for different register assumptions and uses justness as a completeness criterion for liveness property verification.

Findings

Identified violations of correctness in several algorithms.

Suggested improvements for some mutual exclusion algorithms.

Demonstrated the impact of register assumptions on algorithm correctness.

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.