一句话：提出 GPU 数据竞争检测的真阳性定理与近似分析，实现首个可靠且部分完备的检测器 FaialAA。
GPU 程序数据竞争难以避免，可靠但不完备的静态验证会产生需验证的误报。本文基于 CUDA 并发操作的形式化模型，提出数据竞争检测的真阳性定理。核心是近似分析：判断报告位置是否可达（控制独立性 CI）与是否精确（数据独立性 DI），并识别不精确值；对同时满足 CI 与 DI 的程序给出真阳性结果，同时刻画 CI/DI 缺失时误报的根因。作者实现首个可靠且部分完备的检测器 FaialAA。实验表明，它比现有工具确认更多无竞争程序，潜在告警少 1.9 倍，发现 10 个未记录竞争；在 OpenMM 与 MegaTron 的 6 个修复提交中确认 5 个的缺陷版与修复版；2,770 个程序中 59.5% 满足 CI 和 DI。
GPUs are progressively being integrated into modern society, playing a pivotal role in Artificial Intelligence and High-Performance Computing. Programmers need a deep understanding of the GPU programming model to avoid subtle data-races in their codes. Static verification that is sound and incomplete can guarantee data-race freedom, but the alarms it raises may be spurious and need to be validated. In this paper, we establish a True Positive Theorem for a static data-race detector for GPU programs, i.e., a result that identifies a class of programs for which our technique only raises true alarms. Our work builds on the formalism of memory access protocols , that models the concurrency operations of CUDA programs. The crux of our approach is an approximation analysis that can correctly identify true alarms, and pinpoint the conditions that make an alarm imprecise. Our approximation analysis detects when the reported locations are reachable (control independence, or CI), and when the reported locations are precise (data independence, or DI), as well identify inexact values in an alarm. In addition to a True Positive result for programs that are CI and DI, we establish the root causes of spurious alarms depending on whether CI or DI are present. We apply our theory to introduce FaialAA, the first sound and partially complete data-race detector. We evaluate FaialAA in three experiments. First, in a comparative study with the state-of-the-art tools, we show that FaialAA confirms more DRF programs than others while emitting 1.9 × fewer potential alarms. Importantly, the approximation analysis of FaialAA detects 10 undocumented data-races. Second, in an experiment studying 6 commits of data-race fixes in open source projects OpenMM and Nvidia’s MegaTron, FaialAA confirmed the buggy and fixed versions of 5 commits, while others were only able to confirm 2. Third, we show that 59.5 % of 2,770 programs are CI and DI, quantifying when the approximation analysis of FaialAA is complete. This paper is accompanied by the mechanized proofs of the theoretical results presented therein and a tool (FaialAA) implementing of our theory.
@article{LiewCL24,
title = {Sound and Partially-Complete Static Analysis of Data-Races in GPU Programs},
author = {Dennis Liew and Tiago Cogumbreiro and Julien Lange},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689797}
}