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）缩放的减速需要计算，以便在可接受的功率预算下实现计算机绩效缩放，从而对芯片并行性进行巨大的转变。 在进一步的回应中，使用不同的处理元件和专业加速器的使用也有所增加。许多智能手机处理器或片上系统（SOCS）包括4-6种不同的指令集体系结构（ISA）和内存一致性模型（MCMS）。 面对这种越来越多的异质性，该项目的研究旨在驯服这种快速增长的复杂性的体系结构，验证和软件含义。请避免在正确的时间对计算数据进行计算对于计算系统可靠性的基础，而MCM则旨在保证在多线程的系统中保证这一点，但需要更好的验证和翻译支持。 特别是，这项工作正在开发一个具有元素的工具包，其中包括：（i）用于指定MCMS和硬件实现的语法，以及从现有设计描述中得出这些规格的工具，如果需要，可以适当注释。 （ii）用于枚举和检查实现级别（即微结构级）的模块发生在图之前，以生成用于任意MCMS和实现的验证器。 （iii）用于自动从一个MCM转换为另一个MCM的模块。 （iv）组合上述模块以自动生成石榴石测试，进行二进制翻译（包括MCM翻译）和其他有用示例，以进行二进制翻译。 （v）一种教学工具（MCM动画师和插图画家），用于教授计算机体系结构和并行编程课程的学生。 为了促进这项工作的广泛使用，基本模块和组成的工具将作为免费软件分发。