Specifying and Testing GPU Workgroup Progress Models
summary
A toolbox formalizes a tiny concurrent language, implements executable semantics in the CDP model checker, synthesizes 483 litmus tests, compiles them to CUDA/Metal/Vulkan and runs them on eight GPUs from five vendors. A termination oracle labels each test as guaranteed-to-terminate or not; experiments show Apple and ARM GPUs deadlock tests that violate the prior linear occupancy-bound (LOBE) model, while all devices tested conform to the HSA-style weakest fairness.
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:40How do you implement a mutex?
- 1:39Total correctness
- 2:21Liveness issues in a mutex
- 4:57Liveness issues in blocking concurrency
- 8:49Our focus: inter-workgroup
- 9:15Semi-fair progress models
- 10:38Executable progress models
- 11:35Test case synthesis
- 12:39Synthesis results (quantitative)
- 13:35Compiling to executable GPU code
- 14:01The GPUs we tested
- 14:17Surprising results
related talks
19mSIMT-Step Execution: A Flexible Operational Semantics For GPU Subgroup Behavior
21mKuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic
01h 00mBringing Clang and C++ to GPUs: An Open-Source, CUDA-Compatible GPU C++ Compiler
20mModular GPU Programming with Typed Perspectives
19mProgram Reconditioning: Avoiding Undefined Behaviour When Finding and(…)
21mDivergence-Aware Testing of Graphics Shader Compiler Back-Ends
18mUniformity Analysis in the WebGPU Shading Language
21mWeak Memory Demands Model-based Compiler Testing