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

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

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.