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

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

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.