What Compilers desire from Weak Memory Semantics
summary
Claims a method to derive weaker memory models that preserve SC-safe optimizations so compilers need not be reproved for every model. Demonstrates concrete counterexamples where inlining and eliminating writes (via PO immediate edge removal) enable a forbidden message passing outcome or introduce out-of-thin-air–style behaviors, showing simple weakening breaks specific optimizations. Proposes formal criteria and relationships between models so an optimization proven under SC remains valid under the derived weaker semantics.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:11Who I am and my research focus
- 2:06Problem statement
- 4:24Weak memory behaviors
- 9:23Optimizations under weak memory
- 14:22Safety for compiler optimizations
- 17:18Future memory model guarantees
- 18:47Conclusion and Q&A
related talks
01h 11mProgramming language memory models: Problems, solutions, and directions
28mMemory simulations, security and optimization in a verified compiler
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
15mSymbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
25mExorcising Spectres with Secure Compilers
22mReconciling High-level Optimizations and Low-level Code in LLVM
16mCompositional Symbolic Execution for the Next 700 Memory Models
30mA Tale of Shared Memory Concurrency in Programming Languages