Relaxed Memory Model Zoo

Memory model
← Back to the map

Vulkan Memory Model

2018 · Khronos Group, Alglave · language, gpu, formal, scoped

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.

Ordering relationships

Compiles correctly to
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.
  • 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