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

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

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.