A Modular Static Cost Analysis for GPU Warp-Level Parallelism

doi:10.1145/3776693

2026-01-01

PRE

DOI：10.1145/3776693

原文求助

摘要

En 中文

图形处理器（GPU）是性能关键应用的首选加速器，但性能优化需要掌握其内存架构与执行模型之间的复杂交互。现有的GPU核静态分析工具要么识别性能问题但不量化成本，要么无法处理线程发散的控制流，导致严重的过度近似。我们提出了首个针对GPU warp级并行的静态关系成本分析，即使在存在线程发散的情况下也能提供精确界限。我们的分析具有通用性和灵活性，因为它在资源度量（非合并访问、存储器冲突）和成本关系（=、<=、>=）上是参数化的。我们为我们的技术建立了可靠性定理，在Rocq中提供了机械化证明，并将我们的理论实现为一个名为Pico的工具。在可重复性实验中，Pico在所有输入中产生了最紧的界限，在10个核上优于当前最先进的RaCUDA工具（提升1.7倍），而RaCUDA产生了4个不正确的界限并在2个核上崩溃。在测量Pico精度的实验中，我们研究了控制流中线程发散对226个核数据集的影响。我们发现，至少75.3%的条件语句和85.4%的循环可以被精确捕获，而无需引入近似。

Keyword:

cost analysis

relational verification

GPU programming