Modeling and analyzing evaluation cost of CUDA kernels
Modeling and analyzing evaluation cost of CUDA kernels
复制标题
CUDA 内核评估成本建模与分析
DOI：
10.1145/3434306
复制
发表时间：
2021
影响因子：
--
通讯作者：
Hoffmann, Jan
中科院分区：
文献类型：
--
作者：
Muller, Stefan K.;Hoffmann, Jan
随着机器学习和科学计算等应用对向量并行应用的高吞吐量需求，GPU上的通用编程（GPGPU）正变得越来越流行。NVIDIA的CUDA工具包旨在通过允许程序员在C/C++的小型扩展中编写GPU函数（称为内核）来实现GPGPU编程。然而，由于CUDA的复杂的执行模型，CUDA内核的性能特性是很难预测的，特别是对于新手programmer.This本文介绍了一种新的定量程序逻辑CUDA内核，它允许程序员的理由都功能的正确性和资源使用的CUDA内核，特别注意一组常见的，但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.
登录
查看更多内容
CUDA 中线程分歧成本的基准测试
DOI：
--
发表时间：
2015
期刊：
Parallel Processing and Applied Mathematics
影响因子：
--
作者：
P. Bialas;A. Strzelecki
通讯作者：
A. Strzelecki
NESL 的可证明时间和空间高效的实现
DOI：
10.1145/232627.232650
发表时间：
1996
期刊：
Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming
影响因子：
--
作者：
G. Blelloch;John Greiner
通讯作者：
John Greiner
顺序函数语言中的并行性
DOI：
10.1145/224164.224210
发表时间：
1995
期刊：
Proceedings 16th Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
G. Blelloch;John Greiner
通讯作者：
John Greiner
线性相关类型和相对完整性
DOI：
10.2168/lmcs-8(4:11)2012
发表时间：
2011
期刊：
2011 IEEE 26th Annual Symposium on Logic in Computer Science
影响因子：
--
作者：
Ugo Dal Lago;Marco Gaboardi
通讯作者：
Marco Gaboardi
GPUDrano：检测 GPU 程序中的未合并访问
DOI：
10.1007/978-3-319-63387-9_25
发表时间：
2017
期刊：
Proceedings of the 4th International Workshop on OpenCL
影响因子：
--
作者：
R. Alur;Joseph Devietti;O. N. Leija;N. Singhania
通讯作者：
N. Singhania