一句话：提出首个可精确处理线程分歧的 GPU warp 级并行关系代价静态分析，支持资源度量与代价关系参数化，并实现 Rocq 验证工具 Pico。
GPU 是性能关键应用的首选加速器，但优化需理解内存架构与执行模型的交互。现有 GPU kernel 静态工具要么只报告性能缺陷而不量化代价，要么无法处理线程分歧的控制流，导致严重过近似。本文提出首个面向 GPU warp 级并行的静态关系代价分析，能在线程分歧下给出精确界，并对资源度量（非合并访问、bank 冲突）和代价关系（=、≤、≥）参数化。作者给出可靠性定理，在 Rocq 中机器化验证，并实现工具 Pico。可复现实验显示，Pico 在所有输入上界最紧，在 10 个 kernel 上比 RaCUDA 好 1.7 倍；RaCUDA 有 4 个错误界并在 2 个 kernel 上崩溃。对 226 个 kernel 的研究显示，至少 75.3% 的条件和 85.4% 的循环可被精确捕获。
Graphics Processing Units (GPUs) are the accelerator of choice for performance-critical applications, yet optimizing for performance requires mastery of the complex interactions between its memory architecture and its execution model. Existing static analysis tools for GPU kernels either identify performance bugs without quantifying costs or cannot handle thread-divergent control flow, leading to significant over-approximations. We present the first static relational-cost analysis for GPU warp-level parallelism that can give exact bounds even in the presence of thread divergence. Our analysis is general and flexible, as it is parametric on the resource metric (uncoalesced accesses, bank conflicts) and on the cost relation (=, ≤, ≥). We establish a soundness theorem for our technique, provide mechanized proofs in Rocq and implement our theory in a tool called Pico . In a reproducibility experiment, Pico produced the tightest bounds in every input, outperforming the state-of-the-art tool RaCUDA in 10 kernels (1.7× better), while RaCUDA produced 4 incorrect bounds and crashed on 2 kernels. In an experiment to measure the accuracy of Pico , we studied the impact of threaddivergence in control-flow in a dataset of 226 kernels. We found that at least 75.3% of conditionals and 85.4% of loops can be captured exactly, without introducing approximation.
@article{BlikeZSLC26,
title = {A Modular Static Cost Analysis for GPU Warp-Level Parallelism},
author = {Gregory Blike and Hannah Zicarelli and Udaya Sathiyamoorthy and Julien Lange and Tiago Cogumbreiro},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776693}
}