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

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

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.