NVIDIA PTX Memory Model
A scoped, relaxed model for NVIDIA's PTX virtual ISA, with relaxed/acquire/release atomics and explicit thread scopes (CTA, GPU, system). Synchronisation only takes effect between threads that share the named scope, so narrower scopes admit weak behaviours a flat model forbids. Formalised and machine-checked by Lustig et al. (ASPLOS 2019) and the foundation for CUDA's cuda::atomic semantics.
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
- yes No undefined behaviour
- no In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- no Multicopy atomic
Ordering relationships
- Strictly stronger than
- NVIDIA Tile IR Memory Model — NVIDIA Tile IR docs §7: 'The axioms and relations of the Tile IR memory model are intended to be a strict weakening of the PTX memory model.' Vendor-asserted (note the hedged 'intended to be' language); not independently proven or machine-checked.
- Compilation target of
- CUDA C++ Memory Model — CUDA C++ atomics lower to PTX; the CUDA model is layered directly on the PTX memory model.
- OpenCL 2.0 Memory Model — OpenCL kernels compile to PTX on NVIDIA GPUs. Verified sound by memalloy: no execution where the compiled PTX behaviour violates the source OpenCL semantics, up to 4 OpenCL / 6 PTX events (opencl_scoped -> ptx_orig via the opencl_ptx mapping); the known-buggy mapping variant yields a counterexample at 5 events, confirming the check discriminates. Reproduced via litmus/memalloy/ (Docker).
- Vulkan Memory Model — Vulkan/SPIR-V compute shaders compile to PTX on NVIDIA GPUs.
- Incomparable with
- AMD GPU Memory Model — Both are scoped release-consistency ISA models, but expose different scope sets (CTA/GPU/system vs HSA work-group/agent/system) and cache-control qualifiers; neither subsumes the other.
References
- Daniel Lustig, Sameer Sahasrabuddhe, Olivier Giroux. A Formal Analysis of the NVIDIA PTX Memory Consistency Model. ASPLOS 2019, 2019. doi:10.1145/3297858.3304043
- Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen, John Wickerson. GPU Concurrency: Weak Behaviours and Programming Assumptions. ASPLOS 2015, 2015. doi:10.1145/2694344.2694391