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

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的法定任务，并被认为是值得通过基金会的知识分子优点和更广泛影响的评估审查标准来通过评估来获得支持的。