Installing and Using the Linux-Kernel Memory Model (LKMM)
summary
Step-by-step setup of the Linux‑Kernel Memory Model shows how to install herd7 and OCaml, satisfy opam/dune dependencies and build the tools, then run litmus tests from tools/memory_model in kernel tree or from the GitHub repo with about 8,000 litmus tests. The model exhaustively explores tiny concurrent C snippets (no loops or functions), reports outcomes like the IRW test that is never allowed, documents supported primitives (atomics, spinlocks, RCU), and does not address forward progress.
AI-written summary · about
chapters (8)
- 0:00Introduction to LKMM
- 2:24Tooling and installation
- 5:19Configuration troubleshooting
- 9:24Technical Q&A session
- 12:46Understanding atomic primitives
- 17:58Hardware progress guarantees
- 21:32Running litmus tests
- 27:24Litmus test code walk-through
related talks
26mLet's demystify memory
46mLinux Kernel Functional Testing, or How to Build and Test Millions of Linux Kernels
01h 36mLinux Memory Management and Containers
43mGetting to Know the Linux Kernel: A Beginner's Guide
43mLive in a world with multiple memory types
24mContinuously Integrating the Upstream Linux Kernel on Hardware
26mGetting Started With Kernel Programming: The Linux Kernel Mentorship Program
27mFaster Linux Kernel Testing with Linaro's Open-Source Tools and LKFT Automation