Sequential Reasoning for Optimizing Compilers Under Weak Memory Concurrency
summary
Claim: a new sequential semantics seq suffices to prove compiler optimizations sound even when linked into arbitrary weak‑memory contexts modeled by the promising semantics. Method: formal adequacy theorem plus a verified optimizer (certified against the weak model) that uses analyses and transformations like store‑load forwarding, dead‑store elimination and loop‑hoisting. Result: any optimization proven as a behavioral refinement in seq is valid under the full weak memory model; the verified optimizer and the theorem both succeed with the stated limitations.
AI-written summary · about
chapters (13)
- 0:00Validating compiler optimizations
- 1:53How compiler writers do in practice
- 2:25Our approach
- 3:23Forget weak memory models and concurrency
- 4:01Brief explanation of weak memory
- 5:31Semantics of non-atomics in SEQ
- 6:11Optimization on non-atomics in SEQ
- 7:37Semantics of atomics in SEQ
- 9:21Optimization across atomics in SEQ
- 10:42Adequacy of reasoning with SEQ
- 11:25Certified Optimizer
- 13:23Limitation
- 13:51Conclusion
related talks
19mWhat Compilers desire from Weak Memory Semantics
17mPutting Weak Memory in Order via a Promising Intermediate Representation
14mMaking Weak Memory Models Fair
19mSystem-level weak memory models: The need for formalisation, ISA semantics integ...
22mCompilers should get over themselves and respect semantic dependencies!
23mA Reachability Logic for a Weak Memory Model with Promises
20mThe Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Conc
22mIn-order execution nails every weak memory behavior