从同步通信到同步锁的最小翻译（扩展版）
计算机科学中的逻辑
2021-10-04 v2
摘要
为了理解较大并发编程语言的相对表达能力，我们分析了建模并发进程通信与同步的小型进程演算的翻译。源语言 SYNCSIMPLE 是消息传递并发的极简模型，而目标语言 LOCKSIMPLE 是共享内存并发的极简模型。前者是一种具有进程同步通信的演算，后者具有称为锁的同步可变位置——其行为类似于二进制信号量。翻译正确性的准则是它们保持并反映进程的 may-termination 与 must-termination。我们证明了不存在从 SYNCSIMPLE 到 LOCKSIMPLE 的使用一个或两个锁且与锁初始化无关的正确组合翻译。我们还证明了存在一个使用三个锁的正确翻译。同时，具有不同阻塞行为的锁的变体也被考虑在内。
引用
@article{arxiv.2107.14651,
title = {Minimal Translations from Synchronous Communication to Synchronizing Locks (Extended Version)},
author = {Manfred Schmidt-Schauß and David Sabel},
journal= {arXiv preprint arXiv:2107.14651},
year = {2021}
}