ClightTSO
The source-level memory model of CompCertTSO, a Coq-verified compiler from a concurrent C-like language (a threaded extension of CompCert's Clight) to x86 assembly. By design it mirrors the x86-TSO model at the language level, exposing per-thread FIFO store buffers, loads, stores, compare-and-swap, and memory barriers with TSO behaviour; a single TSO abstract machine is shared across all of the compiler's intermediate languages. The store→load relaxation is thus exactly that of TSO/x86-TSO, making it a verified-compiler vehicle for the same model rather than a behaviourally distinct one.
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.
- Compilation optimal mapping to
- yes x86
- no POWER
- no Armv7
- no Armv8
- Reordering sound
- yes Store→Load
- no Store→Store
- no Load→Load
- no Load→Store
- Reasoning guarantees
- yes Coherence
- yes In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- yes Multicopy atomic
Ordering relationships
- Equivalent to
- x86-TSO — Ševčík et al. 2013 §1.2, §4.4: ClightTSO is defined to mirror the x86-TSO model at the language level (loads, stores, compare-and-swap, barriers with TSO behaviour), with a single TSO abstract machine shared across all compiler levels — the same store→load relaxation by construction, not a restricted fragment.
References
- Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell. CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. Journal of the ACM 60(3), Article 22, 2013. doi:10.1145/2487241.2487248
- Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell. Relaxed-Memory Concurrency and Verified Compilation. POPL 2011, 2011. doi:10.1145/1926385.1926393