Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
summary
Claims a thin-air free memory model that justifies every write with a symbolic justification structure (control/data dependencies plus elaborations) so compiler rewrites that assume freedom from undefined behavior and alias-analysis facts are sound. The executable tool handles dynamic allocation, exports a semantic dependency relation to C/C++, permits standard atomic mappings, matches the ISO desiderata tests, and runs the litmus battery orders of magnitude faster than prior executable thin-air semantics.
AI-written summary · about
chapters (9)
- 0:00Thin air problem intro
- 1:27Sequential consistency background
- 2:31Weak memory implications
- 3:58Thin air problem crux
- 5:03Undefined behavior and optimizations
- 6:52SMRD model with justifications
- 8:46Weakening dependencies in SMRD
- 9:07Tool demo and performance
- 10:11Q&A
related talks
19mWhat Compilers desire from Weak Memory Semantics
01h 11mProgramming language memory models: Problems, solutions, and directions
21mWeak Memory Demands Model-based Compiler Testing
19mSystem-level weak memory models: The need for formalisation, ISA semantics integ...
30mA Tale of Shared Memory Concurrency in Programming Languages
22mRelaxed Memory Concurrency Re-executed
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
22mCompilers should get over themselves and respect semantic dependencies!