从同步通信到同步锁的极小翻译
计算机科学中的逻辑
2021-08-26 v1
摘要
为了理解大型并发编程语言的相对表达能力，我们分析了建模并发过程通信与同步的小型进程演算的翻译。源语言SYNCSIMPLE是消息传递并发的极简模型，而目标语言LOCKSIMPLE是共享内存并发的极简模型。前者是一个具有进程同步通信的演算，而后者具有同步可变位置——称为锁——其行为类似于二元信号量。翻译的正确性标准是它们保持并反映进程的may-termination和must-termination。我们证明了，不存在使用一个或两个锁的从SYNCSIMPLE到LOCKSIMPLE的正确组合翻译，且这与锁的初始化无关。我们还证明了存在使用三个锁的正确翻译。此外，还考虑了具有不同阻塞行为的锁的变体。
引用
@article{arxiv.2108.11226,
title = {Minimal Translations from Synchronous Communication to Synchronizing Locks},
author = {Manfred Schmidt-Schauß and David Sabel},
journal= {arXiv preprint arXiv:2108.11226},
year = {2021}
}
备注
In Proceedings EXPRESS/SOS 2021, arXiv:2108.09624. Author version at 2107.14651