SHF: Small: Automatic Qualitative and Quantitative Verification of CUDA Code

SHF：Small：CUDA代码的自动定性和定量验证

• 批准号: 2007784
• 负责人: Jan Hoffmann
• 金额: $ 50万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-10-01 至 2024-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2007784&HistoricalAwards=false
• 关键词: SHF; Small; Automatic; Qualitative; Quantitative

General-purpose programming on Graphics Processing Units (GPUs) has become prevalent in fields such as machine learning. As a result, NVIDIA has developed the CUDA (Compute Unified Device Architecture) framework to support programmers in effectively using GPUs by implementing specialized functions, called kernels, in a dialect of C++. However, the unusual executionmodel of CUDA may result in performance anomalies that would be difficult to predict for novice CUDA programmers. The objective of this project is to develop reasoning techniques and automated tools for predicting the resource usage of CUDA kernels. The outcomes of this project will greatly benefit software programmers, including novices, in writing more efficient kernels.The difficulty in analyzing the performance of CUDA, as opposed to other imperative languages, is that the same code runs in parallel on many threads that store independent copies of local program variables. This project is developing novel analyses that can reason about multiple copies of program variables when necessary for precision but elide this information when possible to maintain scalability. Furthermore, the performance of CUDA code crucially depends upon its ability to hide latency of, for example, memory operations, by quickly switching among many threads. Reasoning precisely about execution times of CUDA kernels therefore requires reasoning about the latency of such operations and the behavior of the GPU's thread scheduler. The tools and analyses developed in this project can open the emerging field of General-Purpose GPU programming to a wider array of developers and improve the quality and efficiency of code in several important domains of computing.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.

图形处理单元 (GPU) 上的通用编程在机器学习等领域已变得普遍。因此，NVIDIA 开发了 CUDA（统一计算设备架构）框架，通过以 C++ 语言实现称为内核的专用功能，支持程序员有效地使用 GPU。然而，CUDA 不寻常的执行模型可能会导致性能异常，而这对于 CUDA 新手程序员来说是难以预测的。该项目的目标是开发推理技术和自动化工具来预测 CUDA 内核的资源使用情况。该项目的成果将大大有利于软件程序员（包括新手）编写更高效的内核。与其他命令式语言相比，分析 CUDA 性能的困难在于，相同的代码在存储独立数据的许多线程上并行运行。局部程序变量的副本。该项目正在开发新颖的分析，可以在需要精度时推理程序变量的多个副本，但在可能的情况下忽略此信息以保持可扩展性。此外，CUDA 代码的性能关键取决于其通过在多个线程之间快速切换来隐藏延迟（例如内存操作）的能力。因此，精确推理 CUDA 内核的执行时间需要推理此类操作的延迟以及 GPU 线程调度程序的行为。该项目开发的工具和分析可以向更广泛的开发人员开放通用 GPU 编程的新兴领域，并提高几个重要计算领域的代码质量和效率。该奖项反映了 NSF 的法定使命，并被视为值得通过使用基金会的智力优点和更广泛的影响审查标准进行评估来支持。

项目成果

Modeling and analyzing evaluation cost of CUDA kernels

CUDA 内核评估成本建模与分析

• DOI: 10.1145/3434306
• 发表时间: 2021
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Muller, Stefan K.;Hoffmann, Jan
• 通讯作者: Hoffmann, Jan

Probabilistic Resource-Aware Session Types

• DOI: 10.1145/3571259
• 发表时间: 2020-11
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Ankush Das;Di Wang;Jan Hoffmann

Two decades of automatic amortized resource analysis

二十年的自动摊销资源分析

• DOI: 10.1017/s0960129521000487
• 发表时间: 2022
• 期刊: Mathematical Structures in Computer Science
• 影响因子: 0.5
• 作者: Hoffmann, Jan;Jost, Steffen
• 通讯作者: Jost, Steffen

Automatic Amortized Resource Analysis with Regular Recursive Types

• DOI: 10.1109/lics56636.2023.10175720
• 发表时间: 2023-04
• 期刊: 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
• 作者: Jessie Grosen;David M. Kahn;Jan Hoffmann

Static prediction of parallel computation graphs

并行计算图的静态预测

• DOI: 10.1145/3498708
• 发表时间: 2022
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Muller, Stefan K.