arXiv 2409.120132024-09cs.PL

内存一致性与程序变换

Memory Consistency and Program Transformations

Akshay Gopalakrishnan, Clark Verbrugge, Mark Batty

DOI：: 10.1145/3721143

阅读 PDF

arXiv 页面 ↗HTML 原文 ↗

AI总结：

本文通过将程序优化分解为执行轨迹上的基本效应，提出一种形式化框架来刻画内存一致性与优化安全性的组合关系，并证明顺序一致性与允许读-读重排序的模型之间满足完备性，为以优化为导向的内存模型设计奠定基础。

摘要：

内存一致性模型规定了共享内存并发程序所允许的行为。在语言层面，已知这些模型对程序优化的安全性具有非平凡的影响，限制了在不引入新行为的情况下重新排列或重构代码的能力。现有的编程语言内存模型试图通过允许更多（松弛/弱）并发行为来解决这一问题，但仍然无法允许所有期望的优化。一个核心问题是，较弱的一致性模型也可能使优化变得不安全，这一结论与它们允许更多行为的直觉相悖。这暴露了一个关于内存一致性语义与优化之间组合交互的开放问题：语义的哪些部分对应于允许或不允许哪些优化集合尚不清楚。在这项工作中，我们建立了一个足够适合理解这种组合性质的形式化基础，将优化分解为对程序执行轨迹的有限一组基本效应，并可在这些效应上评估安全性的各个方面。我们利用这一分解来识别一个期望的组合性质（完备性），该性质将保证从一个内存模型到另一个内存模型的优化安全性。我们通过证明顺序一致性（SC）与 $SC_{RR}$ 之间的这一性质来展示其实际可行性，后者在 $SC$ 之上允许独立的读-读重排序。我们的工作可能为编程语言内存模型的一种新设计方法铺平道路，该方法强调期望执行的优化。

英文摘要：

A memory consistency model specifies the allowed behaviors of shared memory concurrent programs. At the language level, these models are known to have a non-trivial impact on the safety of program optimizations, limiting the ability to rearrange/refactor code without introducing new behaviors. Existing programming language memory models try to address this by permitting more (relaxed/weak) concurrent behaviors but are still unable to allow all the desired optimizations. A core problem is that weaker consistency models may also render optimizations unsafe, a conclusion that goes against the intuition of them allowing more behaviors. This exposes an open problem of the compositional interaction between memory consistency semantics and optimizations: which parts of the semantics correspond to allowing/disallowing which set of optimizations is unclear. In this work, we establish a formal foundation suitable enough to understand this compositional nature, decomposing optimizations into a finite set of elementary effects on program execution traces, over which aspects of safety can be assessed. We use this decomposition to identify a desirable compositional property (complete) that would guarantee the safety of optimizations from one memory model to another. We showcase its practicality by proving such a property between Sequential Consistency (SC) and $SC_{RR}$, the latter allowing independent read-read reordering over $SC$. Our work potentially paves way to a new design methodology of programming-language memory models, one that places emphasis on the optimizations desired to be performed.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

AI总结：

摘要：

英文摘要：

相关论文