A Compositional Theory of Linearizability
A Compositional Theory of Linearizability
复制标题
DOI：
10.1145/3571231
复制
发表时间：
2023-01
影响因子：
--
通讯作者：
Arthur Oliveira Vale;Zhong Shao;Yixuan Chen
中科院分区：
文献类型：
--
作者：
Arthur Oliveira Vale;Zhong Shao;Yixuan Chen
组合性是编程语言研究的核心，并且已经成为大型系统可扩展验证的重要目标。尽管如此，仍然没有线性性的组合说明，而线性性是并发对象正确性的黄金标准。在本文中，我们开发了一种线性并发对象的组合语义。我们首先展示了一个常见的问题，它与线性性无关，在并发计算的组合模型的构建中：与组合的中性元素的交互可能导致紧急行为，这是组合性的障碍。范畴理论以卡鲁比包络的形式为这个问题提供了一个解决方案。令人惊讶的是，这是我们工作的主要发现，这个抽象的结构与线性化密切相关，并导致了它的新公式。值得注意的是，这个新公式既不依赖于原子性，也不直接依赖于排序之前发生的事件，而且只有由于组合性才有可能，这表明线性性和组合性在本质上是相互关联的。我们使用这种新的，复合的，对线性化的理解来重新审视线性化的理论，提供新颖的，简单的，局部性的代数证明，并与观测细化等效的模拟。通过将我们的语义与一个简单的程序逻辑连接起来，我们展示了我们的技术可以在实践中使用，该程序逻辑在这种广义线性化方面仍然是合理的。
Compositionality is at the core of programming languages research and has become an important goal toward scalable verification of large systems. Despite that, there is no compositional account of linearizability, the gold standard of correctness for concurrent objects. In this paper, we develop a compositional semantics for linearizable concurrent objects. We start by showcasing a common issue, which is independent of linearizability, in the construction of compositional models of concurrent computation: interaction with the neutral element for composition can lead to emergent behaviors, a hindrance to compositionality. Category theory provides a solution for the issue in the form of the Karoubi envelope. Surprisingly, and this is the main discovery of our work, this abstract construction is deeply related to linearizability and leads to a novel formulation of it. Notably, this new formulation neither relies on atomicity nor directly upon happens-before ordering and is only possible because of compositionality, revealing that linearizability and compositionality are intrinsically related to each other. We use this new, and compositional, understanding of linearizability to revisit much of the theory of linearizability, providing novel, simple, algebraic proofs of the locality property and of an analogue of the equivalence with observational refinement. We show our techniques can be used in practice by connecting our semantics with a simple program logic that is nonetheless sound concerning this generalized linearizability.