Compositional Reasoning for Non-multicopy Atomic Architectures
Compositional Reasoning for Non-multicopy Atomic Architectures
复制标题
非多拷贝原子架构的组合推理
DOI：
--
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Graeme Smith
中科院分区：
文献类型：
--
作者：
Nicholas Coughlin;Kirsten Winter;Graeme Smith
依赖/保证推理提供了一种组合方法来推理并发程序。然而，这种推理传统上假设了顺序一致的内存模型，因此在存在数据竞争的现代硬件上是不可靠的。在本文中，我们为非多拷贝原子弱内存模型提供了一种基于依赖/保证的方法，即线程的存储不会同时传播到所有其他线程，因此其他线程无法同时观察到。这些内存模型包括早期版本的ARM处理器和POWER处理器。本文建立在我们对多副本原子体系结构进行组合推理的方法之上，即一个线程的存储同时传播给所有其他线程。在这种情况下，操作语义可以基于线程本地指令重排序。我们利用这一点来提供一种有效的组合证明技术，在这种技术中，弱记忆行为可以显示在顺序一致的记忆模型上保持依赖/保证推理。为了实现这一目标，我们引入了一个侧条件，在每个线程上重新排序干扰自由，减少了对可重新排序指令对进行检查的弱内存的复杂性。在本文中，我们将这种方法扩展到非多拷贝原子弱内存模型。我们利用了平行分量间干涉自由度重排序的思想。这本身会破坏组合性，但可以作为在依赖条件和保证条件之间派生精细兼容性检查的工具，它考虑了仅部分存储（即不覆盖所有线程）传播的影响。我们的方法的所有方面都在Isabelle/HOL中进行了编码和验证。
Rely/guarantee reasoning provides a compositional approach to reasoning about concurrent programs. However, such reasoning traditionally assumes a sequentially consistent memory model and hence is unsound on modern hardware in the presence of data races. In this article, we present a rely/guarantee-based approach for non-multicopy atomic weak memory models, i.e., where a thread’s stores are not simultaneously propagated to all other threads and hence are not observable by other threads at the same time. Such memory models include those of the earlier versions of the ARM processor as well as the POWER processor. This article builds on our approach to compositional reasoning for multicopy atomic architectures, i.e., where a thread’s stores are simultaneously propagated to all other threads. In that context, an operational semantics can be based on thread-local instruction reordering. We exploit this to provide an efficient compositional proof technique in which weak memory behaviour can be shown to preserve rely/guarantee reasoning on a sequentially consistent memory model. To achieve this, we introduce a side-condition, reordering interference freedom on each thread, reducing the complexity of weak memory to checks over pairs of reorderable instructions. In this article, we extend our approach to non-multicopy atomic weak memory models. We utilise the idea of reordering interference freedom between parallel components. This by itself would break compositionality but serves as a vehicle to derive a refined compatibility check between rely and guarantee conditions, which takes into account the effects of propagations of stores that are only partial, i.e., not covering all threads. All aspects of our approach have been encoded and proved sound in Isabelle/HOL.
登录
查看更多内容
DOI：
10.1145/2837614.2837615
发表时间：
2016-01
期刊：
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Shaked Flur;Kathryn E. Gray;Christopher Pulte;Susmit Sarkar;A. Sezgin;Luc Maranget;Will Deacon;Peter Sewell
通讯作者：
Shaked Flur;Kathryn E. Gray;Christopher Pulte;Susmit Sarkar;A. Sezgin;Luc Maranget;Will Deacon;Peter Sewell
了解 POWER 多处理器
影响因子：
--
作者：
Sarkar S
通讯作者：
Sarkar S
具有宽松依赖性的 C11 程序的 Owicki-Gries 推理（扩展版本）
DOI：
10.48550/arxiv.2108.01418
发表时间：
2021
期刊：
--
影响因子：
--
作者：
Wright D
通讯作者：
Wright D
C/C 并发的库抽象
DOI：
10.1145/2429069.2429099
发表时间：
2013
期刊：
--
影响因子：
--
作者：
Batty M
通讯作者：
Batty M