Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers
CoRR(2023)
摘要
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.
更多查看译文
关键词
process-algebraic,multi-writer,multi-reader,non-atomic
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要