SIMT-Step Execution: A Flexible Operational Semantics For GPU Subgroup Behavior
summary
Formal operational semantics defines subgroup behavior using dynamic basic blocks and a spectrum classifying instructions as independent, synchronous, or collective. An executable TLA+ model checks a suite of idiomatic tests (all verify in under one second) and a fuzzing campaign generates 10K variants per base pattern and runs across nine GPUs from seven vendors. Results show most devices behave strongly synchronously, but collective-memory semantics is not portable.
AI-written summary · about
chapters (12)
- 0:00SIMT-Step execution intro
- 1:04Motivation and problem
- 3:54GPU subgroup overview
- 6:18Subgroup behavior questions
- 8:44Lockstep assumptions evolution
- 9:50Memory model and testing
- 11:11Independent execution storms
- 12:34Synchronous control flow
- 13:38Subgroup sync models spectrum
- 14:41Empirical GPU results
- 15:22Summary and contributions
- 15:46Q&A
related talks
15mSpecifying and Testing GPU Workgroup Progress Models
36mFlexible Instruction-Set Semantics via Abstract Monads
31mFormal Specification
19mSystem-level weak memory models: The need for formalisation, ISA semantics integ...
17mTowards Semantics Lifting for Scientific Computing: A Case Study on FFT
12mISA Formal Task Group Update
16mAutomatically Deriving Control-Flow Graph Generators from Operational Semantics
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
