XPS: EXPL: CCA: Verification and Optimization Tools for Heterogeneous Memory Consistency Models

在过去的十年里，摩尔定律和Dennard伸缩的减速要求计算向片上并行进行戏剧性的转变，以便在可接受的功率预算下实现计算机性能伸缩。作为进一步的回应，对不同处理元件和专用加速器的使用也有所增加；许多智能手机处理器或片上系统(SoC)包括4-6种不同的指令集体系结构(ISA)和存储器一致性模型(MCM)。面对这种日益增长的异构性，该项目的研究旨在驯服这种快速增长的复杂性的体系结构、验证和软件含义。确保在正确的时间对正确的数据进行计算是计算系统可靠性的基础，MCM旨在确保多线程系统中的这一点，但需要更好的验证和转换支持。特别是，这项工作正在开发一个工具包，其元素包括：(I)用于指定MCM和硬件实现的语法，以及从现有设计描述中推导出这些规范的工具，如果需要，可进行适当注释。(Ii)用于枚举和检查实现级(即微体系结构级)在图之前发生的模块，以生成用于任意MCM和实现的验证器。(Iii)用于从一种MCM自动转换到另一种MCM的模块。(Iv)组成上述模块的工具，以自动生成Litmus测试，进行二进制翻译，包括MCM翻译，以及其他有用的例子。(V)向学生教授计算机体系结构和并行编程课程的教学工具(MCM动画师和插画师)。为了促进这项工作的广泛使用，基本模块和组合工具将作为自由软件分发。

Over the past decade, the deceleration of Moore's Law and Dennard Scaling has required computing to make a dramatic shift towards on-chip parallelism in order to achieve computer performance scaling at acceptable power budgets. In further response, the use of diverse processing elements and specialized accelerators has also increased; many smartphone processors or systems-on-chip (SoCs) include 4-6 different instruction set architectures (ISAs) and memory consistency models (MCMs). In the face of this increasing heterogeneity, this project's research aims to tame the architecture, verification, and software implications of this fast-growing complexity.Ensuring that computations occur on the right data at the right time is fundamental to computing system reliability, and MCMs are intended to guarantee this in multi-threaded systems, but better verification and translation support is needed. In particular, this work is developing a toolkit with elements including: (i) Grammars for specifying MCMs and hardware implementations, as well as tools to derive these specifications from existing design descriptions, appropriately annotated if needed. (ii) Modules for enumerating and checking implementation-level (i.e. microarchitecture-level) Happens-Before-Graphs to generate verifiers for arbitrary MCMs and implementations. (iii) Modules for automatically translating from one MCM to another. (iv) Tools that compose the above modules to automatically generate litmus tests, to do binary translation including MCM translation, and other useful examples. (v) A pedagogical tool (an MCM animator and illustrator) for teaching students in computer architecture and parallel programming classes. To facilitate broad use of this work, basic modules and composed tools will be distributed as free software.