License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2023.5
URN: urn:nbn:de:0030-drops-189995
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18999/
Spronck, Myrthe S. C. ;
Luttik, Bas
Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers
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.
BibTeX - Entry
@InProceedings{spronck_et_al:LIPIcs.CONCUR.2023.5,
author = {Spronck, Myrthe S. C. and Luttik, Bas},
title = {{Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers}},
booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)},
pages = {5:1--5:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-299-0},
ISSN = {1868-8969},
year = {2023},
volume = {279},
editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18999},
URN = {urn:nbn:de:0030-drops-189995},
doi = {10.4230/LIPIcs.CONCUR.2023.5},
annote = {Keywords: mutual exclusion, model checking, non-atomic reads and writes, regular register}
}
