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

点击翻译按钮获取中文摘要

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.