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.
Cat model
Expressible in cat cited
Khronos specifies the model executably in Alloy rather than cat. Its availability/visibility rules are per-execution constraints, expressible with cat's scope support. Group 2018
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