Scoped C11 / HRF-Relaxed

2015 · Gaster, Hower, Howes · theoretical, gpu, formal, scoped · axiomatic formalism

A generalisation of the C11 DRF framework with a scope hierarchy, relaxing HRF-direct/indirect's strict scope-matching to suit industrial heterogeneous models. It underpins the scoped-atomics designs adopted by OpenCL, HSA and the GPU vendor models.

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 No undefined behaviour
no In-order execution
no No out-of-thin-air

Ordering relationships

Strictly weaker than: Heterogeneous-Race-Free (HRF) — Gaster et al.'s HRF-Relaxed loosens HRF-direct/indirect's exact scope-matching, admitting more programs and behaviours than the original HRF models.

References

Benedict R. Gaster, Derek Hower, Lee Howes. HRF-Relaxed: Adapting HRF to the Complexities of Industrial Heterogeneous Memory Models. ACM TACO, 2015. doi:10.1145/2701618
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

Open Scoped C11 in the interactive map →