More Science Fiction than Fairy Tale: A Discussion of the Linux Kernel Memory Mo...
summary
Linux kernel concurrency uses a graph-based LKMM that encodes axioms, 5,000+ lit tests, and predicts real hardware/compiler reorderings; analysis of a Q spinlock reveals a hang that stays in upstream code for three years until tooling finds it. Automated tools genemc and datanya generate execution graphs, the 34th graph flags a safety violation on current qspinlock within seconds, and adding a store-release fixes the ARM-server failure while the model sometimes errs on conservatism.
AI-written summary · about
chapters (7)
- 0:00Intro
- 0:52WHY WEAK MEMORY?
- 5:26WHY WEAK MEMORY MODELS?
- 11:23HISTORY OF LINUX KERNEL MEMORY MODEL
- 22:29HOW TO USE LKMM - MANUALLY?
- 28:13FINAL EXAMPLES
- 33:58CONCLUSION
related talks
40mKernel Locking Engineering
30mA Tale of Shared Memory Concurrency in Programming Languages
26mArmed cats: formal concurrency modelling at Arm
13mThe Semantics of Shared Memory in Intel CPU/FPGA Systems
01h 01mThe Future of Concurrency and Parallelism
01h 11mProgramming language memory models: Problems, solutions, and directions
01h 02mMaking Games Start Fast: A Story About Concurrency
21mWeak Memory Demands Model-based Compiler Testing