使用带信号的进程代数分析互斥
计算机科学中的逻辑
2017-09-05 v1
摘要
与普遍看法相反，通信系统演算（CCS）及类似的进程代数缺乏准确捕捉互斥协议的表达能力，除非用公平性假设来丰富语言。添加公平性假设来实现互斥协议似乎有违直觉。我们采用了一个信号算子，它可与 CCS 或其他进程演算结合，并表明这一极小扩展足以对互斥建模：在底层内存模型的合理假设下，我们确认了双进程 Peterson 互斥算法以及 Lamport 面包店算法的正确性。对于多于两个进程的 Peterson 算法，其正确性需要对底层内存模型更强、不太现实的假设。
引用
@article{arxiv.1709.00826,
title = {Analysing Mutual Exclusion using Process Algebra with Signals},
author = {Victor Dyseryn and Rob van Glabbeek and Peter Höfner},
journal= {arXiv preprint arXiv:1709.00826},
year = {2017}
}
备注
In Proceedings EXPRESS/SOS 2017, arXiv:1709.00049