On the need for available, functional, and reusable memory models
summary
Paper data vanishes after a PhD student leaves, so reproducibility fails; experiments and examples claim conformance but links are dead, so demand is permanent accessibility. Verification debates over whether an API needs a fence collapse because multiple model versions exist and tools are missing, so projects need executable models and parametric tool support. One model ships only ~100 litmus tests and misses a message‑passing case, revealing lack of regression suites. Successes (RISC‑V task force, ARM team, Linux kernel model) share open source, tool-backed validation and industry–academia collaboration.
AI-written summary · about
chapters (15)
- 0:00Memory model challenges
- 1:05Formal model availability gaps
- 3:10Tool support lack
- 4:55Executable model problems
- 7:43Empirical validation need
- 8:46Proof reusability
- 10:37Formalization success stories
- 13:04ARM’s formal model
- 14:49Linux kernel model
- 17:18Successful model principles
- 19:25Open sourcing challenges
- 20:48Shared tool repositories
- 21:50Academia-industry progress
- 22:11Q&A on comparison tools
- 23:38Proof reusability discussion
related talks
01h 11mProgramming language memory models: Problems, solutions, and directions
30mA Tale of Shared Memory Concurrency in Programming Languages
23mMemory Consistency Model Status Update
01h 02mThe Two Memory Models
32mMemory Model
28mCAAT: Consistency as a Theory
26mArmed cats: formal concurrency modelling at Arm
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++