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.

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