Explanation of the Linux-Kernel Memory Consistency Model

Summary

Explanation of the Linux-Kernel Memory Consistency Model ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ :Author: Alan Stern :Created: October 2017 .. Contents 1. INTRODUCTION 2. BACKGROUND 3. A SIMPLE EXAMPLE 4. A SELECTION OF MEMORY MODELS 5. ORDERING AND CYCLES 6. EVENTS 7. THE PROGRAM ORDER RELATION: po AND po-loc 8. A WARNING 9. DEPENDENCY RELATIONS: data, addr, and ctrl 10. THE READS-FROM RELATION: rf, rfi, and rfe 11. CACHE COHERENCE AND THE COHERENCE ORDER RELATION: co, coi, and coe 12. THE FROM-READS RELATION: fr, fri, and fre 13. AN OPERATIONAL MODEL 14. PROPAGATION ORDER RELATION: cumul-fence 15. DERIVATION OF THE LKMM FROM THE OPERATIONAL MODEL 16. SEQUENTIAL CONSISTENCY PER VARIABLE 17. ATOMIC UPDATES: rmw 18. THE PRESERVED PROGRAM ORDER RELATION: ppo 19. AND THEN THERE WAS ALPHA 20. THE HAPPENS-BEFORE RELATION: hb 21. THE PROPAGATES-BEFORE RELATION: pb 22. RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb 23. SRCU READ-SIDE CRITICAL SECTIONS 24. LOCKING 25. PLAIN ACCESSES AND DATA RACES 26. ODDS AND ENDS INTRODUCTION ------------ The Linux-kernel memory consistency model (LKMM) is rather complex and obscure. This is particularly evident if you read through the linux-kernel.bell and linux-kernel.cat files that make up the formal version of the model; they are extremely terse and their meanings are far from clear. This document describes the ideas underlying the LKMM. It is meant for people who want to understand how the model was designed. It does not go into the details of the code in the .bell and .cat files; rather, it explains in English what the code expresses symbolically. Sections 2 (BACKGROUND) through 5 (ORDERING AND CYCLES) are aimed toward beginners; they explain what memory consistency models are and the basic notions shared by all such models. People already familiar with these concepts can skim or skip over them. Sections 6 (EVENTS) through 12 (THE FROM_READS RELATION) describe the fundamental relations used...