2026-08-05T05:23:47Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18999 2024-03-06T11:03:14Z ddc:004 open_access

Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers Spronck, Myrthe S. C. Luttik, Bas mutual exclusion model checking non-atomic reads and writes regular register 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Myrthe S. C. Spronck and Bas Luttik 2023 Is Part Of LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2023.5 urn:nbn:de:0030-drops-189995 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.5 eng https://creativecommons.org/licenses/by/4.0/legalcode