一句话：提出面向 CUDA 内核的定量程序逻辑与代价语义，可自动推导符号化资源上界并检测性能瓶颈。
随着机器学习与科学计算对向量并行高吞吐的需求增长，GPGPU 编程日益流行。NVIDIA 的 CUDA 允许程序员用 C/C++ 的小扩展编写 GPU 函数（kernel），但其执行模型复杂，性能特征难以预测，对新手尤为困难。本文提出一种新的面向 CUDA 内核的定量程序逻辑，使程序员能够同时推理内核的功能正确性与资源使用，并特别关注一组常见但 CUDA 特有的性能瓶颈。作者给出新的操作代价语义，并证明该逻辑相对于此语义是可靠的；语义、逻辑与可靠性证明均在 Coq 中形式化。基于 LP 求解的推断算法通过在逻辑中生成推导，自动合成符号化资源界。该算法是端到端内核资源分析工具 RaCuda 的基础，RaCuda 基于已有的命令式程序资源分析工具实现。在一组 CUDA 基准上的实验表明，该分析能有效帮助检测 CUDA 内核中的性能缺陷。
General-purpose programming on GPUs (GPGPU) is becoming increasingly in vogue as applications such as machine learning and scientific computing demand high throughput in vector-parallel applications. NVIDIA's CUDA toolkit seeks to make GPGPU programming accessible by allowing programmers to write GPU functions, called kernels, in a small extension of C/C++. However, due to CUDA's complex execution model, the performance characteristics of CUDA kernels are difficult to predict, especially for novice programmers. This paper introduces a novel quantitative program logic for CUDA kernels, which allows programmers to reason about both functional correctness and resource usage of CUDA kernels, paying particular attention to a set of common but CUDA-specific performance bottlenecks. The logic is proved sound with respect to a novel operational cost semantics for CUDA kernels. The semantics, logic and soundness proofs are formalized in Coq. An inference algorithm based on LP solving automatically synthesizes symbolic resource bounds by generating derivations in the logic. This algorithm is the basis of RaCuda, an end-to-end resource-analysis tool for kernels, which has been implemented using an existing resource-analysis tool for imperative programs. An experimental evaluation on a suite of CUDA benchmarks shows that the analysis is effective in aiding the detection of performance bugs in CUDA kernels.
@article{paperbot1161,
title = {Modeling and analyzing evaluation cost of CUDA kernels},
author = {Stefan K. Muller and Jan Hoffmann},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434306}
}