Taking Back Control in an Intermediate Representation for GPU Computing
summary
Formal modeling of SPIR-V control flow encodes the rules in an Alloy model, replaces brittle dominance rules with structural dominance that counts control, merge and continue edges, and yields a much simpler, cheaper-to-compute spec fragment now adopted in the SPIR-V release. Validation iterates against conformance tests and the Khronos validator; a model-driven fuzzer generates self-checking shader tests and uncovers 20 distinct bugs across Google, Khronos, Intel and Mozilla compilers (15 from the model), most already fixed or acknowledged.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 2:12Shaders and control flow
- 4:22Formalizing SPIR-V rules
- 8:19Validating formal model
- 11:27Dominance in control flow
- 15:46Problematic control flow example
- 17:53Simplifying SPIR-V rules
- 18:14Novel fuzzing for GPU compilers
- 22:12Summary of contributions
- 23:13Q&A
related talks
18mPreparing for a Valid Performance Evaluation of RISC-V AP, in the Mobile Space
32mState of the Union
32mV8 by example: A journey through the compilation pipeline
14mHoneycomb: Secure and Efficient GPU Executions via Static Validation
12mRISC-V QoS: CBQRI, RQSC and resctrl
07mBuilding Robust GPU Performance Validation into CI/CD Pipelines
47mRethinking compilers with live coding
30mRaspberry Pi 5: Challenges and Solutions in Bringing up an OpenGL/...