Collaborative Research: SHF: Medium: High-Performance, Verified Accelerator Programming

合作研究：SHF：中：高性能、经过验证的加速器编程

• 批准号: 2313023
• 负责人: Adam Chlipala
• 金额: $ 53.3万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-07-01 至 2026-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2313023&HistoricalAwards=false
• 关键词: Collaborative; Research; SHF; Medium; Performance

Emerging applications are pushing the limits of high-performance computing. New hardware accelerators are being developed to handle particular workloads much more efficiently than can be achieved in software, but it is expensive to develop these hardware units and the software that connects to them. In fact, today the majority of hardware-development budgets go to the combination of finding and fixing hardware bugs and developing software support for the new hardware. This project studies how to improve that whole development process with end-to-end formal verification, where machine-checked mathematical proofs establish correct behavior for the whole hardware-software stack. The research team is specifically concerned with tensor computations, as appear in graphics and machine learning. The project's novelties are in extending the idea of end-to-end mechanized proof for the first time to cover hardware accelerators, specifically tensor processing units (TPU). The project's impacts are the potential for dramatic lowering of the costs of developing new hardware accelerators or iterating on their implementations over time, while providing strong mathematical correctness guarantees to applications, e.g., the tools to show that a machine-learning system protects user privacy, despite the use of complex performance optimizations.Three main levels of computing system are covered by the project, all with logical specifications and proofs that are to be composed into system-level theorems in the Coq proof assistant. The top level is a source programming language called Exo, which allows programmer-guided optimization of nested-loop programs, where appropriate use of accelerators is gradually introduced through rewrite rules. General optimization tactics, or reusable transformation procedures, are being developed alongside their proofs. The middle level is the Bedrock2 programming language, which is similar to the C language, with formal support for external functions that can be used to model hardware facilities. That mechanism is being extended to support modern accelerator interfaces, in contrast to the simpler, embedded-systems-oriented interfaces of past work. Finally, processors and accelerators are verified, requiring new developments in modular specification and proof of hardware.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

新兴应用正在突破高性能计算的极限。人们正在开发新的硬件加速器，以比软件更有效地处理特定的工作负载，但开发这些硬件单元以及连接到它们的软件的成本很高。事实上，如今大部分硬件开发预算都用于查找和修复硬件错误以及开发新硬件的软件支持。该项目研究如何通过端到端形式验证来改进整个开发过程，其中机器检查的数学证明为整个硬件软件堆栈建立了正确的行为。该研究团队特别关注图形和机器学习中出现的张量计算。该项目的新颖之处在于首次将端到端机械化证明的理念扩展到硬件加速器，特别是张量处理单元（TPU）。该项目的影响是有可能大幅降低开发新硬件加速器或随着时间的推移迭代其实现的成本，同时为应用程序提供强大的数学正确性保证，例如，显示机器学习系统保护用户隐私的工具，尽管使用了复杂的性能优化。该项目涵盖了计算系统的三个主要级别，所有级别都具有逻辑规范和证明，这些逻辑规范和证明将在 Coq 证明助手中组成系统级定理。顶层是一种名为 Exo 的源编程语言，它允许程序员引导优化嵌套循环程序，其中通过重写规则逐渐引入加速器的适当使用。一般的优化策略或可重用的转换程序正在与它们的证明一起开发。中间层是Bedrock2编程语言，它类似于C语言，正式支持可用于对硬件设施进行建模的外部函数。与过去工作中更简单、面向嵌入式系统的接口相比，该机制正在扩展以支持现代加速器接口。最后，处理器和加速器经过验证，需要模块化规范和硬件证明方面的新发展。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力优点和更广泛的影响审查标准进行评估，被认为值得支持。