TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA
TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA
复制标题
TriCheck：软件、硬件和 ISA 三部分的内存模型验证
DOI：
10.1145/3037697.3037719
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
M. Martonosi
中科院分区：
文献类型：
--
作者：
Caroline Trippel;Yatin A. Manerkar;Daniel Lustig;Michael Pellauer;M. Martonosi
在共享内存系统中控制模块间相互作用的内存一致性模型（MCMS）是系统设计的重要但经常被低估的方面。 MCM在硬件软件堆栈的各个层上定义，需要在层之间的接口上进行彻底验证的规格，编译器和实现。当前的验证技术评估了系统堆栈的片段，例如证明了从高级语言（HLL）到ISA的编译器映射到ISA的微体系进行实施的有效性。本文提供了全栈MCM验证的理由，并提供了一个工具流，即tricheck，能够验证HLL，编译器，ISA和实施是否共同坚持MCM要求。该作品展示了Tricheck评估所提出的ISA MCM的能力，以确保每个层和每个映射都是正确且完整的。具体来说，我们将Tricheck应用于开源RISC-V ISA [55]，试图验证C11的准确，高效和法律汇编。我们在当前的RISC-V ISA文档中发现了较低的特异性和潜在效率低下，并确定了每个文档的可能解决方案。例如，我们发现符合RISC-V符合的微体系结构允许在检查的1,701个LITMUS测试中观察到C11禁止的144个结果。总体而言，本文展示了需要全堆栈验证以检测硬件软件堆栈中与MCM相关的错误的必要性。
Memory consistency models (MCMs) which govern inter-module interactions in a shared memory system, are a significant, yet often under-appreciated, aspect of system design. MCMs are defined at the various layers of the hardware-software stack, requiring thoroughly verified specifications, compilers, and implementations at the interfaces between layers. Current verification techniques evaluate segments of the system stack in isolation, such as proving compiler mappings from a high-level language (HLL) to an ISA or proving validity of a microarchitectural implementation of an ISA. This paper makes a case for full-stack MCM verification and provides a toolflow, TriCheck, capable of verifying that the HLL, compiler, ISA, and implementation collectively uphold MCM requirements. The work showcases TriCheck's ability to evaluate a proposed ISA MCM in order to ensure that each layer and each mapping is correct and complete. Specifically, we apply TriCheck to the open source RISC-V ISA [55], seeking to verify accurate, efficient, and legal compilations from C11. We uncover under-specifications and potential inefficiencies in the current RISC-V ISA documentation and identify possible solutions for each. As an example, we find that a RISC-V-compliant microarchitecture allows 144 outcomes forbidden by C11 to be observed out of 1,701 litmus tests examined. Overall, this paper demonstrates the necessity of full-stack verification for detecting MCM-related bugs in the hardware-software stack.
登录
查看更多内容
彻底修改 C11 和 OpenCL 中的 SC 原子
DOI：
10.1145/2837614.2837637
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Batty M
通讯作者：
Batty M
同步 C/C 和 POWER
DOI：
10.1145/2254064.2254102
发表时间：
2012
期刊：
--
影响因子：
--
作者：
Sarkar S
通讯作者：
Sarkar S
DOI：
10.1145/3009837.3009838
发表时间：
2017
期刊：
--
影响因子：
--
作者：
Wickerson J
通讯作者：
Wickerson J
了解 POWER 多处理器
影响因子：
--
作者：
Sarkar S
通讯作者：
Sarkar S