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

XPS：EXPL：CCA：异构内存一致性模型的验证和优化工具

• 批准号: 1533837
• 负责人: Margaret Martonosi
• 金额: $ 30万
• 依托单位: Princeton University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-09-01 至 2019-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1533837&HistoricalAwards=false
• 关键词: XPS; EXPL; CCA; Verification; Optimization

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.

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