发表机构
University of California at Santa Cruz; University of Massachusetts Boston; Microsoft Research（加州大学圣克鲁兹分校; 马萨诸塞大学波士顿分校; 微软研究院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
WarpDRF提出首个精确的抽象warp编程模型，定义数据竞争自由契约，通过形式化证明和模糊测试验证，并扩展静态分析器以检测GPU内核中的未知数据竞争。
AI 中文摘要
Warp原语（如张量核心操作、洗牌、归约和屏障）对于高性能GPU内核至关重要，每个主流GPU语言都支持其中一些原语。参与某个原语（从而进行同步）的线程由线程如何分歧和重新汇聚以及warp内调度（如独立线程调度）动态决定。在实践中，许多高性能内核使用这些原语并表现符合预期，遵循一种直观但未成文的数据竞争自由契约，该契约从未被精确陈述或经验测试。我们提出WarpDRF，这是第一个使该契约精确化的抽象warp编程模型，其参与规则以重新汇聚保证和每个原语的要求为参数，使得实例化能够匹配不同的GPU语言。我们证明（在Rocq中形式化）满足WarpDRF的内核以参考语义分配的参与者执行每个warp原语并产生相同结果，因此程序员可以仅依据参考语义进行推理。我们在MLIR中实现该模型并附带参考解释器，针对CUDA、HIP、HLSL、Metal和SPIR-V在16个设备和后端组合上对三种配置各进行10K一致性测试模糊测试；至少有一种WarpDRF配置描述每种情况，其中CUDA遵循严格最弱的配置。最后，我们将Faial（一个针对CUDA的静态数据竞争分析器）扩展为经验验证的warp模型的第一个DRF检查器，并将其应用于此http URL，其中大多数使用warp原语的内核已经满足该契约，但三个包含先前未知的数据竞争，表明需要工具来检查它。
英文摘要
Warp primitives such as tensor core operations, shuffles, reductions, and barriers are critical to high-performance GPU kernels, and every major GPU language supports some set of them. The threads that participate in a primitive, and therefore synchronize, are determined dynamically by how threads diverge and reconverge, and by intra-warp scheduling such as independent thread scheduling. In practice, many high-performance kernels use these primitives and behave as expected, following an intuitive but unwritten data-race-freedom contract that has never been stated precisely or empirically tested. We present WarpDRF, the first abstract warp programming model to make this contract precise, with participation rules parameterized by reconvergence guarantees and per-primitive requirements so that instantiations match different GPU languages. We prove (formalized in Rocq) that a kernel satisfying WarpDRF executes every warp primitive with the participants the reference semantics assigns and produces the same results, so a programmer can reason in the reference semantics alone. We implement the model in MLIR with a reference interpreter and fuzz 10K conformance tests for each of three configurations across CUDA, HIP, HLSL, Metal, and SPIR-V on 16 device and backend pairs; at least one WarpDRF configuration describes each, with CUDA honoring the strictly weakest configuration. Finally, we extend Faial, a static data-race analyzer for CUDA, into the first DRF checker for an empirically validated warp model, and apply it to llama.cpp, where most kernels that use warp primitives already satisfy the contract, but three contain previously unknown data races, showing the need for tools that check it.
