  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.
