Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers

TL;DR

This paper develops process-algebraic models for multi-writer multi-reader registers and uses model checking to evaluate the robustness of mutual exclusion algorithms under relaxed atomicity, challenging previous correctness claims.

Contribution

It introduces formal process-algebraic models for multi-reader multi-writer registers and applies model checking to analyze algorithm correctness under relaxed atomicity.

Findings

Some mutual exclusion algorithms are not robust under relaxed atomicity.

The models clarify the relationship between different register specifications.

Correctness claims in literature are refuted based on model checking results.

Abstract

We present process-algebraic models of multi-writer multi-reader safe, regular and atomic registers. We establish the relationship between our models and alternative versions presented in the literature. We use our models to formally analyse by model checking to what extent several well-known mutual exclusion algorithms are robust for relaxed atomicity requirements. Our analyses refute correctness claims made about some of these algorithms in the literature.