Principles of Programming Seminar
- Remote Access Enabled - Zoom
- Virtual Presentation
- STEFAN MULLER
- Postdoctoral Fellow
- Computer Science Department
- Carnegie Mellon University
Modeling and Analyzing Evaluation Cost of CUDA Kernels OR
Modeling and Analyzing Evaluation Cost of CUDA Kernels OR How I Spent My Summer Vacation Postdoc
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 talk 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. We have proved the logic sound with respect to a novel operational cost semantics for CUDA kernels. An inference algorithm based on LP solving automatically synthesizes symbolic resource bounds by generating derivations in the logic. This algorithm is the basis of 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 such as inefficient memory accesses in CUDA kernels. Finally, techniques drawn from the study of task-parallel programs allow us to extend these techniques toward reasoning about even more complex properties such as execution time.
This is joint work with Jan Hoffmann.
Until the day after this talk, Stefan Muller is a postdoc in the Principles of Programming group at CMU. He completed his PhD, on interactive parallel programs, at CMU in 2018 and since then has been answering the question "Didn't you graduate already?" in the halls of GHC. This fall, he is starting as an assistant professor at the Illinois Institute of Technology.
Zoom Participation Enabled. See announcement.