Modular Relaxed Dependencies in Weak Memory Concurrency
Modular Relaxed Dependencies in Weak Memory Concurrency
复制标题
DOI：
10.1007/978-3-030-44914-8_22
复制
发表时间：
2020-04-18
期刊：
影响因子：
--
通讯作者：
Batty M
中科院分区：
文献类型：
--
作者：
Paviotti M;Cooksey S;Paradis A;Wright D;Owens S;Batty M
我们提出了一个指称语义弱内存并发，避免稀薄的空气读取，提供数据竞争免费的程序与顺序一致的语义（DRF-SC），并支持组合优化关系验证优化。我们的语义识别错误的程序依赖关系，可能会被删除的编译器优化，并在适当的地方只留下必要的依赖关系，以排除稀薄的空气读取。我们表明，我们的依赖关系计算可以用来排除稀薄的空气读任何公理并发模型，特别是C++。我们提出了一个工具，自动评估石蕊测试，表明我们可以增强C++来解决稀薄的空气问题，我们证明我们的增强是兼容的关键处理器架构与以前使用的编译映射。我们认为，我们的依赖计算提供了一个实用的路线，以解决长期存在的问题，稀薄的空气读在C++规范。
We present a denotational semantics for weak memory concurrency that avoids thin-air reads, provides data-race free programs with sequentially consistent semantics (DRF-SC), and supports a compositional refinement relation for validating optimisations. Our semantics identifies false program dependencies that might be removed by compiler optimisation, and leaves in place just the dependencies necessary to rule out thin-air reads. We show that our dependency calculation can be used to rule out thin-air reads in any axiomatic concurrency model, in particular C++. We present a tool that automatically evaluates litmus tests, show that we can augment C++ to fix the thin-air problem, and we prove that our augmentation is compatible with the previously used compilation mappings over key processor architectures. We argue that our dependency calculation offers a practical route to fixing the longstanding problem of thin-air reads in the C++ specification.
登录
查看更多内容
影响因子：
--
作者：
Manson, J;Pugh, W;Adve, SV
通讯作者：
Adve, SV
影响因子：
0.6
作者：
Jeffrey, Alan;Riely, James
通讯作者：
Riely, James
影响因子：
--
作者：
Pichon-Pharabod, Jean;Sewell, Peter
通讯作者：
Sewell, Peter
影响因子：
1
作者：
Leroy, Xavier;Grall, Herve
通讯作者：
Grall, Herve
影响因子：
1.3
作者：
Lochbihler, Andreas
通讯作者：
Lochbihler, Andreas