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 \emph{uniformity analysis}—a static check that rejects programs that could cause \emph{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) \emph{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) \emph{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) \emph{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) \emph{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.