A Modular Static Cost Analysis for GPU Warp-Level Parallelism
summary
Claims a new static, relational-cost analysis that translates warp semantics into a sequential cost program and is parametric on resource metric and relation, with proofs mechanized in Rocq and an implementation called Pico; Pico computes exact bounds despite divergence for many kernels. Evaluation: Pico gives the tightest bound in every reproduced input, averaging 1.7× better on 10 kernels vs RaCUDA while RaCUDA yields 4 incorrect bounds and 2 crashes. On 226 kernels, 75.3% of conditionals and 85.4% of loops are captured exactly.
AI-written summary · about
chapters (10)
- 0:00GPU warp-level cost analysis
- 1:06GPUs and performance challenges
- 3:14Thread divergence and memory
- 6:06Cost analysis framework
- 8:12Sequential translation correctness
- 12:27Pico tool evaluation
- 13:30Comparison with Rauda
- 14:54Precision on real-world kernels
- 15:35Conclusion and future work
- 16:39Q&A
related talks
15mA Modular Cost Analysis for Probabilistic Programs
16mPricing Python Parallelism: A Dynamic Language Cost Model for Heterogeneous Platforms
20mModular GPU Programming with Typed Perspectives
24mTowards Understanding the Costs of Avoiding Out-of-Thin-Air Results
21mKuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic
18mCompiling Strassen-like Matrix Multiplication Algorithms to Fast CUDA Kernels
15mRaising Expectations: Automating Expected Cost Analysis with Types
17mEvaluation of Speedup & Energy with Multigrain Parallelizing Compiler