一句话：提出全栈内存一致性模型验证工具流 TriCheck，并揭示 RISC-V 与 C11 间的规范漏洞与低效。
内存一致性模型（MCM）规定共享内存系统中模块间的交互，横跨软硬件栈多个层次，需要逐层充分验证。现有技术孤立评估栈中某一段，如编译器映射或微架构实现。本文主张全栈 MCM 验证，提出工具流 TriCheck，用于验证高级语言、编译器、ISA 与实现是否共同满足 MCM 要求。作者将 TriCheck 应用于开源 RISC-V ISA，验证从 C11 到 RISC-V 的编译是否准确、高效且合法。结果发现 RISC-V ISA 文档存在欠规范与潜在低效，并给出解决方案；在 1701 个 litmus 测试中，符合 RISC-V 的微架构允许 144 个被 C11 禁止的结果被观察到。这表明确保全栈验证对发现 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.