Overhauling SC atomics in C11 and OpenCL
Overhauling SC atomics in C11 and OpenCL
复制标题
彻底修改 C11 和 OpenCL 中的 SC 原子
DOI：
10.1145/2837614.2837637
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Batty M
中科院分区：
文献类型：
--
作者：
Batty M
尽管顺序一致性（SC）的概念简单，但C11和OpenCL内存模型中SC原子操作和围栏的语义是微妙的，导致复杂的散文描述转化为复杂的公理形式化。我们在C11中对SC原子进行了一次大修，减少了相关公理的数量和复杂性。我们简化的结果是，执行中的SC操作不再需要完全排序。这种放松使，第一次，有效和详尽的模拟石蕊测试，使用SC原子。我们扩展了我们改进的C11模型，以获得第一个严格的内存模型形式化的OpenCL（扩展C11支持异构众核编程）。在OpenCL设置中，我们进一步完善了SC公理，为SC操作提供了合理的语义，这些操作采用“内存范围”来限制其对特定线程的可见性。我们的大修需要稍微加强C11和OpenCL内存模型，导致一些行为变得不允许。我们认为这些增强是自然的，并且我们所知道的所有正式的C11和OpenCL编译方案（C11的Power和x86 CPU，OpenCL的AMD GPU）在我们修改后的模型中仍然有效。使用HERD记忆模型模拟器，我们表明，我们的大修导致C11石蕊测试的模拟时间与原始模型相比呈指数级改善，使 * 详尽 * 模拟具有竞争力，时间明智的，与 * 非详尽 * CDScore工具。
Despite the conceptual simplicity of sequential consistency (SC), the semantics of SC atomic operations and fences in the C11 and OpenCL memory models is subtle, leading to convoluted prose descriptions that translate to complex axiomatic formalisations. We conduct an overhaul of SC atomics in C11, reducing the associated axioms in both number and complexity. A consequence of our simplification is that the SC operations in an execution no longer need to be totally ordered. This relaxation enables, for the first time, efficient and exhaustive simulation of litmus tests that use SC atomics. We extend our improved C11 model to obtain the first rigorous memory model formalisation for OpenCL (which extends C11 with support for heterogeneous many-core programming). In the OpenCL setting, we refine the SC axioms still further to give a sensible semantics to SC operations that employ a ‘memory scope’ to restrict their visibility to specific threads. Our overhaul requires slight strengthenings of both the C11 and the OpenCL memory models, causing some behaviours to become disallowed. We argue that these strengthenings are natural, and that all of the formalised C11 and OpenCL compilation schemes of which we are aware (Power and x86 CPUs for C11, AMD GPUs for OpenCL) remain valid in our revised models. Using the HERD memory model simulator, we show that our overhaul leads to an exponential improvement in simulation time for C11 litmus tests compared with the original model, making *exhaustive* simulation competitive, time-wise, with the *non-exhaustive* CDSChecker tool.
登录
查看更多内容
DOI：
--
发表时间：
2015
期刊：
European Symposium on Programming
影响因子：
--
作者：
Mark Batty;Kayvan Memarian;Kyndylan Nienhuis;Jean Pichon;Peter Sewell
通讯作者：
Peter Sewell
影响因子：
1.3
作者：
Betts A
通讯作者：
Betts A
影响因子：
1.1
作者：
P. B. Hansen
通讯作者：
P. B. Hansen
使用远程范围提升进行同步
DOI：
--
发表时间：
2015
期刊：
International Conference on Architectural Support for Programming Languages and Operating Systems
影响因子：
--
作者：
Marc S. Orr;Shuai Che;Ayse Yilmazer;Bradford M. Beckmann;M. Hill;D. Wood
通讯作者：
D. Wood
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