Programming language memory models: Problems, solutions, and directions
summary
Shows why sequential consistency fails for real hardware with the Dekker's lock example (both critical sections observed on x86 unless fences are inserted) and why C11 permits out-of-thin-air values. Compares models (SC, C11/Java, RC11, Promising 1.0/2.0, Weakestmo) by three concrete metrics: which compiler reorderings must be banned, which fences compilers/VMs insert for ARM/x86, and measured cost (LLVM disablement → ~34% slowdown, patched → ~5.5%; volatile-everywhere JVM → x86 ~28–79% avg, ARM up to 557%). Recommends tradeoffs: RC11-like fixes give near-zero cost on x86 but need extra fences on ARM; Promising-style semantics avoid thin-air with different complexity.
AI-written summary · about
chapters (22)
- 0:00Start
- 0:27Research Interests
- 1:11Memory Models
- 7:22Weak Behaviors
- 10:16Programming Language Memory Models Requirements
- 10:32Soundness of Compile Optimizations
- 11:47Criteria Is Efficient Compilation to Hardware
- 15:07Well-Known Memory Models
- 15:23Sequential Consistency
- 18:13Java Memory Models
- 20:01Efficient Efficiency of Compilation to Hardware
- 20:21Exploding Java Memory Model Drf Guarantee
- 24:38Memory Models in Terms of Drf Guarantee
- 28:03Execution Graphs
- 30:13Rf Edge
- 31:23Axiomatic Memory Model
- 35:53Rc11 Memory Model
- 39:58Example Program
- 53:17Modular Relaxed Dependencies
- 54:22Data Race Freedom Guarantee
- 59:23Mainstream Memory Models
- 1:08:59Problems with Promising Semantics
related talks
01h 02mThe Two Memory Models
30mA Tale of Shared Memory Concurrency in Programming Languages
21mWeak Memory Demands Model-based Compiler Testing
01h 28mC++ Memory Model: from C++11 to C++23
40mA practical approach to Java Memory Model
19mSystem-level weak memory models: The need for formalisation, ISA semantics integ...
19mWhat Compilers desire from Weak Memory Semantics
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++