Vulkan Memory Model
Khronos's formal, relaxed, scoped memory model for the Vulkan GPU API. Ordering is expressed through scoped synchronisation plus explicit availability and visibility operations that move writes through the cache hierarchy. Specified executably in Alloy, with the formalisation led largely by Jade Alglave and collaborators.
Properties
Property vector author-extrapolated — set only where the model’s definition pins the cell down (unknown cells are omitted); cells citing a specific source are marked.
- Reordering sound
- yes Store→Load
- yes Store→Store
- yes Load→Load
- yes Load→Store
- Reasoning guarantees
- yes Coherence
- no In-order execution
Ordering relationships
- Compiles correctly to
- NVIDIA PTX Memory Model — Vulkan/SPIR-V compute shaders compile to PTX on NVIDIA GPUs.
- AMD GPU Memory Model — Vulkan/SPIR-V compute shaders compile to AMD's GPU ISA.
- Compilation target of
- WebGPU / WGSL Memory Model — Browser WebGPU implementations lower WGSL to Vulkan (and to Metal/Direct3D 12); the WGSL model is derived from Vulkan's.
- Incomparable with
- OpenCL 2.0 Memory Model — Both are scoped GPU API models, but differ in scope sets and synchronisation primitives — Vulkan adds explicit availability/visibility operations that OpenCL lacks; neither contains the other.
References
- Khronos Group. Vulkan Memory Model (Vulkan Specification — Memory Model chapter). Khronos Vulkan Registry, 2018. docs.vulkan.org/spec/latest/chapters/memorymodel.html
- Derek R. Hower, Blake A. Hechtman, Bradford M. Beckmann, Benedict R. Gaster, Mark D. Hill, Steven K. Reinhardt, David A. Wood. Heterogeneous-Race-Free Memory Models. ASPLOS 2014, 2014. doi:10.1145/2541940.2541981