On Locality and the Exchange Law for Concurrent Processes
On Locality and the Exchange Law for Concurrent Processes
复制标题
论并发进程的局部性和交换律
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
G. Struth
中科院分区：
文献类型：
--
作者：
C. Hoare;A. Hussain;B. Möller;P. O'Hearn;R. Petersen;G. Struth
本文结合近年来在并发Kleene代数和分离逻辑方面的研究成果，对并发的代数模型进行了研究。它建立了分离逻辑的并发规则和框架规则之间的紧密联系，是范畴论交换规律的一种变体。我们研究了两个标准模型：一个使用跟踪集，另一个是基于状态的，使用断言和最弱前提条件。我们将后者作为部分函数与堆的标准模型联系起来。我们利用代数的力量来统一模型并对它们的变化进行分类。
This paper studies algebraic models for concurrency, in light of recent work on Concurrent Kleene Algebra and Separation Logic. It establishes a strong connection between the Concurrency and Frame Rules of Separation Logic and a variant of the exchange law of Category Theory. We investigate two standard models: one uses sets of traces, and the other is state-based, using assertions and weakest preconditions. We relate the latter to standard models of the heap as a partial function. We exploit the power of algebra to unify models and classify their variations.