Putting Weak Memory in Order via a Promising Intermediate Representation
summary
Claims an in-order source semantics for C/C++ that preserves all common compiler optimizations for non-atomics by compiling to an out-of-order IR with undefined values for racy reads, and formally proves soundness of source→IR→Armv8 mappings. Uses the promising-style semantics split into a catch-fire source model and an out-of-order IR, mechanizing proofs in Coq. Shows relaxed atomics require forbidding load→store reordering and proposes a new strong store instruction to avoid measurable overhead.
AI-written summary · about
chapters (13)
- 0:00Weak memory ordering
- 0:22Relaxed memory model challenges
- 1:05Out-of-order execution issues
- 2:53Introducing Inod memory model
- 3:57Nonatomic access challenges
- 6:43Source and IR models for nonatomics
- 8:51Atomic accesses and hardware optimizations
- 10:17Load-store reordering impact
- 12:49Compiling relaxed atomics
- 13:11Summary and implications
- 14:14Q&A: Compiler optimizations
- 14:35Q&A: Hardware atomics
- 15:18Q&A: Low-overhead atomics
related talks
23mA Reachability Logic for a Weak Memory Model with Promises
59mA Relaxed Guide to memory_order_relaxed
01h 11mProgramming language memory models: Problems, solutions, and directions
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
01h 28mAtomic’s memory orders, what for?
14mMaking Weak Memory Models Fair
43mC++ Atomics...
01h 02mThe Two Memory Models