Compound Memory Models
summary
Defines a compositional operational specification that composes distinct device models into a x86TSO/PTX compound model and proves C-to-architecture compiler mappings still hold for threads mapped to each device. Implements the model axiomatically, ships artifacts and tests on an AMD G5 simulator, and finds simulator behaviors match the model except when a cache protocol relaxes a single-writer multiple-reader invariant, which breaks a message-passing litmus test. Uses a thread-local operational model with lossy propagation by stalling to get compositionality.
AI-written summary · about
chapters (10)
- 0:00Compound memory models intro
- 0:20What memory models are
- 2:24Why they matter now
- 3:51Challenges in combining models
- 6:40Message passing example
- 8:26Compositionality problem
- 9:08Thread-local semantics loss
- 10:53Lost pop operational model
- 13:00Conclusion and future
- 13:22Q&A
related talks
13mThe Semantics of Shared Memory in Intel CPU/FPGA Systems
01h 02mThe Two Memory Models
21mWeak Memory Demands Model-based Compiler Testing
30mA Tale of Shared Memory Concurrency in Programming Languages
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
01h 11mProgramming language memory models: Problems, solutions, and directions
26mArmed cats: formal concurrency modelling at Arm