Uniformity Analysis in the WebGPU Shading Language
summary
Provides a rigorous operational semantics for TinyWGSL that defines barrier divergence, formalizes the WGSL uniformity rules, and proves soundness sketches; mechanises the static taint analysis in an Alloy model and uses Alloy-driven test generation to fuzz Chromium’s WGSL compiler; finds multiple specification flaws, proposes four accepted spec changes for soundness and precision, and discovers a real Chromium parser/analysis bug that gets fixed, with artifacts and tests archived.
AI-written summary · about
chapters (9)
- 0:00WebGPU shading language intro
- 1:26Barriers in GPU programs
- 3:10WebGPU and Wixel
- 4:56Uniformity analysis for barriers
- 6:42Uniform vs non-uniform control flow
- 8:50Uniformity analysis in Wixel
- 11:37Testing with Alloy
- 13:21Fixing analysis soundness bugs
- 15:09Summary
related talks
16mW2GPU: Toward WebAssembly-to-WebGPU Program Translation via Small Language Models
16mBringing the WebAssembly Standard up to Speed with SpecTec
19mProgram Reconditioning: Avoiding Undefined Behaviour When Finding and(…)
21mDivergence-Aware Testing of Graphics Shader Compiler Back-Ends
26mSpecTec, a Single Source of Truth
55mGenerating Executable Specification from Formal Semantics of WebAssembly
22mDynamic Analysis Extending a Shadow Runtime for Profit
24mWebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing