Automatically comparing memory consistency models
Automatically comparing memory consistency models
复制标题
自动比较内存一致性模型
DOI：
10.1145/3009837.3009838
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Wickerson J
中科院分区：
文献类型：
--
作者：
Wickerson J
内存一致性模型(MCM)是编程语言或计算机体系结构规范的一部分，它定义了哪些值可以合法地从共享内存位置读取。由于MCM考虑了体系结构和编译器所采用的各种优化，因此它们往往是复杂和违反直觉的，这使得它们的设计和理解具有挑战性。我们确定了设计和理解MCM涉及的四项任务：生成一致性测试、区分两个MCM、检查编译器优化和检查编译器映射。我们证明了所有四个任务都是一般约束满足问题的实例，其解要么是一个程序，要么是一对程序。虽然这个问题对于自动求解器来说是棘手的，当直接在程序上分段时，我们展示了如何在程序执行时解决类似的约束，然后构造满足原始约束的程序。我们的技术在合金建模框架中实现，在几个软件和体系结构级别的MCM上进行了说明，从公理和操作上定义了这一点。我们自动重新创建几个已知的结果，通常是以更简单的形式，包括：C11 MCM变体之间的区别；早期C11草案中“SC-DRF保证”的失败；x86是“多副本原子”而Power不是；常见C11编译器优化中的错误；以及从OpenCL到AMD风格的GPU的编译器映射中的错误。我们还使用我们的技术为NVIDIA图形处理器开发和验证了新的MCM，它支持来自OpenCL的自然映射。
Amemory consistency model(MCM) is the part of a programming language or computer architecture specification that defines which values can legally be read from shared memory locations. Because MCMs take into account various optimisations employed by architectures and compilers, they are often complex and counterintuitive, which makes them challenging to design and to understand.We identify four tasks involved in designing and understanding MCMs: generating conformance tests, distinguishing two MCMs, checking compiler optimisations, and checking compiler mappings. We show that all four tasks are instances of a general constraint-satisfaction problem to which the solution is either a program or a pair of programs. Although this problem is intractable for automatic solvers when phrased over programs directly, we show how to solve analogous constraints over programexecutions, and then construct programs that satisfy the original constraints.Our technique, which is implemented in the Alloy modelling framework, is illustrated on several software- and architecture-level MCMs, both axiomatically and operationally defined. We automatically recreate several known results, often in a simpler form, including: distinctions between variants of the C11 MCM; a failure of the "SC-DRF guarantee" in an early C11 draft; that x86 is "multi-copy atomic" and Power is not; bugs in common C11 compiler optimisations; and bugs in a compiler mapping from OpenCL to AMD-style GPUs. We also use our technique to develop and validate a new MCM for NVIDIA GPUs that supports a natural mapping from OpenCL.
登录
查看更多内容
用于比较内存一致性模型的 Litmus 测试：它们需要多长时间？
DOI：
--
发表时间：
2011
期刊：
Design Automation Conference
影响因子：
--
作者：
Sela Mador;R. Alur;Milo M. K. Martin
通讯作者：
Milo M. K. Martin
使用远程范围提升进行同步
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
彻底修改 C11 和 OpenCL 中的 SC 原子
DOI：
10.1145/2837614.2837637
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Batty M
通讯作者：
Batty M
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
处理器一致性的力量
DOI：
10.1145/165231.165264
发表时间：
1993
期刊：
Proceedings of the eleventh annual ACM symposium on Theory of computing
影响因子：
--
作者：
M. Ahamad;R. Bazzi;Ranjit John;Prince Kohli;G. Neiger
通讯作者：
G. Neiger