一句话：首次形式化研究 WebGPU 着色语言的 uniformity 分析，定义 barrier divergence，修正 WGSL 规范并发现 Chromium 实现缺陷。
WebGPU 将通用 GPU 编程引入 Web，允许不受信任的 JavaScript 向客户端 GPU 提交并行负载；为保证可靠性，它强制实施 uniformity 分析，静态拒绝可能引发 barrier divergence（屏障发散）的程序，而传统 GPU 模型通常把这种发散视为未定义行为。论文首次对 WGSL 中的 uniformity 分析进行系统形式化与实证研究，并识别出四个关键问题：缺乏独立定义、规范复杂、健全性与精度不足、难以测试实现。作者为 TinyWGSL 核心演算建立操作语义，首次在 WGSL 语境下严格定义 barrier divergence；用简洁形式规则重新表述分析，并论证其相对于该语义的健全性；据此发现 WGSL 规范中的缺陷，提出四项规范修改且均被接受；还在 Alloy 中机器化该分析，利用测试生成压力测试 Chromium 实现，揭示规范与实现差异以及一个 Chromium 缺陷。该工作将形式化 PL 技术应用于重要工业 GPU 语言规范并产生实际影响。
The WebGPU programming model brings general-purpose GPU programming to the web, allowing untrusted JavaScript to issue parallel workloads to client GPUs. To ensure reliability, WebGPU mandates uniformity analysis —a static check that rejects programs that could cause barrier divergence , a GPU control-flow error that can hang execution and require OS-level recovery. While traditional GPU models treat barrier divergence as undefined behaviour, WebGPU’s need for safety and reliability makes this unacceptable. We present the first comprehensive formal and practical study of uniformity analysis in WebGPU, identifying four key issues and making corresponding contributions: (1) Lack of definition: The analysis currently defines non-uniform programs only as those it rejects, without an independent notion of barrier divergence. We provide an operational semantics for TinyWGSL, a core calculus of the WebGPU Shading Language (WGSL), developed in consultation with WGSL specification editors and implementers. This semantics rigorously defines barrier divergence in the context of WGSL for the first time. (2) Complex specification: The current description of uniformity analysis in WGSL is lengthy and imprecise. We reformulate it via concise formal rules for TinyWGSL and argue their soundness with respect to our semantics. (3) Lack of soundness and precision: Using our semantics, we expose soundness and precision flaws in the analysis as presented in the WGSL specification. In response, we have proposed four significant changes to the specification (all accepted). (4) Testing difficulty: The complex, semi-formal definition of uniformity in the WGSL specification makes it hard to test implementations. We mechanise uniformity analysis in Alloy and use Alloy’s test generation to stress-test the Chromium implementation, revealing specification–implementation discrepancies and a bug in the Chromium implementation. Overall, our work resolves an important GPU programming problem (rigorously defining barrier divergence), brings an interesting new analysis to the attention of the PL community, and demonstrates the impact of applying formal PL techniques to an important industrial language specification.
@article{Lee-JonesWD26,
title = {Uniformity Analysis in the WebGPU Shading Language},
author = {James Lee-Jones and John Wickerson and Alastair F. Donaldson},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808331}
}