Open Source Summit Europe 2022

The Linux Kernel runs on a variety of architectures under an aggressively optimizing compiler. Both compiler and hardware reorder memory operations in various ways to improve performance, resulting in drastically different behaviors of mainly concurrent code on each platform. To allow concurrent components for the kernel to be developed in a mostly platform-independent way, developers and researchers tackled the daunting effort of providing a unified abstraction of these hardware and compiler optimizations in the form of 1) a library of concurrency primitives and 2) a high-level mathematical model of these optimizations which predicts their visible effects when using that library. This Linux Kernel Memory Model (LKMM) was published under the title "Frightening small children and disconcerting grown-ups: Concurrency in the Linux kernel", reminiscent of German fairy tales. We explain how to read and use such models for practitioners, and show on various examples that perhaps the LKMM is less like a fairy tale and more like science fiction, as it involves time travel, robots, and lots of moving parts. We discuss some areas where the LKMM might be improved further, e.g., where it makes incorrect predictions on Linux code or allows behaviors unintended by its original designers.