Installing and Using the Linux-Kernel Memory Model (LKMM)
summary
Explains how to install LKMM from the kernel tree (use tools/memory-model and the distro package for a faster path), run lit tests and the verifier’s eval step, and interpret outputs like the reported “no” that proves a bad outcome cannot occur; demonstrates a small message-passing example that exercises atomics, barriers, RCU and locks; notes limits (no allocator/free, limited structs, unrolled loops) and kernel compatibility (around 6.x); five attendees install live.
AI-written summary · about
chapters (6)
- 0:00Introduction to LKMM
- 3:45What the memory model does
- 10:11Installing the tool
- 12:29Running a test example
- 21:36Verifying synchronization correctness
- 24:14Limitations and use cases
related talks
46mLinux Kernel Functional Testing, or How to Build and Test Millions of Linux Kernels
15mMLEE: Effective Detection of Memory Leaks on Early-Exit Paths in OS Kernels
41mKeeping up with LTS: Linux Kernel Functional Testing (LKFT) on Devices
27mFaster Linux Kernel Testing with Linaro's Open-Source Tools and LKFT Automation
44mKUnit - Unit Testing for the Linux Kernel
01h 01mAdvanced Unit Testing in C & C++
19mChecking your work: Linux kernel testing and CI
18mEnhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach