1 ===================================== 2 LINUX KERNEL MEMORY CONSISTENCY MODEL 3 ===================================== 4 5============ 6INTRODUCTION 7============ 8 9This directory contains the memory consistency model (memory model, for 10short) of the Linux kernel, written in the "cat" language and executable 11by the externally provided "herd7" simulator, which exhaustively explores 12the state space of small litmus tests. 13 14In addition, the "klitmus7" tool (also externally provided) may be used 15to convert a litmus test to a Linux kernel module, which in turn allows 16that litmus test to be exercised within the Linux kernel. 17 18 19============ 20REQUIREMENTS 21============ 22 23Version 7.49 of the "herd7" and "klitmus7" tools must be downloaded 24separately: 25 26 https://github.com/herd/herdtools7 27 28See "herdtools7/INSTALL.md" for installation instructions. 29 30 31================== 32BASIC USAGE: HERD7 33================== 34 35The memory model is used, in conjunction with "herd7", to exhaustively 36explore the state space of small litmus tests. 37 38For example, to run SB+mbonceonces.litmus against the memory model: 39 40 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+mbonceonces.litmus 41 42Here is the corresponding output: 43 44 Test SB+mbonceonces Allowed 45 States 3 46 0:r0=0; 1:r0=1; 47 0:r0=1; 1:r0=0; 48 0:r0=1; 1:r0=1; 49 No 50 Witnesses 51 Positive: 0 Negative: 3 52 Condition exists (0:r0=0 /\ 1:r0=0) 53 Observation SB+mbonceonces Never 0 3 54 Time SB+mbonceonces 0.01 55 Hash=d66d99523e2cac6b06e66f4c995ebb48 56 57The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that 58this litmus test's "exists" clause can not be satisfied. 59 60See "herd7 -help" or "herdtools7/doc/" for more information. 61 62 63===================== 64BASIC USAGE: KLITMUS7 65===================== 66 67The "klitmus7" tool converts a litmus test into a Linux kernel module, 68which may then be loaded and run. 69 70For example, to run SB+mbonceonces.litmus against hardware: 71 72 $ mkdir mymodules 73 $ klitmus7 -o mymodules litmus-tests/SB+mbonceonces.litmus 74 $ cd mymodules ; make 75 $ sudo sh run.sh 76 77The corresponding output includes: 78 79 Test SB+mbonceonces Allowed 80 Histogram (3 states) 81 644580 :>0:r0=1; 1:r0=0; 82 644328 :>0:r0=0; 1:r0=1; 83 711092 :>0:r0=1; 1:r0=1; 84 No 85 Witnesses 86 Positive: 0, Negative: 2000000 87 Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated 88 Hash=d66d99523e2cac6b06e66f4c995ebb48 89 Observation SB+mbonceonces Never 0 2000000 90 Time SB+mbonceonces 0.16 91 92The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate 93that during two million trials, the state specified in this litmus 94test's "exists" clause was not reached. 95 96And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/" 97for more information. 98 99 100==================== 101DESCRIPTION OF FILES 102==================== 103 104Documentation/cheatsheet.txt 105 Quick-reference guide to the Linux-kernel memory model. 106 107Documentation/explanation.txt 108 Describes the memory model in detail. 109 110Documentation/recipes.txt 111 Lists common memory-ordering patterns. 112 113Documentation/references.txt 114 Provides background reading. 115 116linux-kernel.bell 117 Categorizes the relevant instructions, including memory 118 references, memory barriers, atomic read-modify-write operations, 119 lock acquisition/release, and RCU operations. 120 121 More formally, this file (1) lists the subtypes of the various 122 event types used by the memory model and (2) performs RCU 123 read-side critical section nesting analysis. 124 125linux-kernel.cat 126 Specifies what reorderings are forbidden by memory references, 127 memory barriers, atomic read-modify-write operations, and RCU. 128 129 More formally, this file specifies what executions are forbidden 130 by the memory model. Allowed executions are those which 131 satisfy the model's "coherence", "atomic", "happens-before", 132 "propagation", and "rcu" axioms, which are defined in the file. 133 134linux-kernel.cfg 135 Convenience file that gathers the common-case herd7 command-line 136 arguments. 137 138linux-kernel.def 139 Maps from C-like syntax to herd7's internal litmus-test 140 instruction-set architecture. 141 142litmus-tests 143 Directory containing a few representative litmus tests, which 144 are listed in litmus-tests/README. A great deal more litmus 145 tests are available at https://github.com/paulmckrcu/litmus. 146 147lock.cat 148 Provides a front-end analysis of lock acquisition and release, 149 for example, associating a lock acquisition with the preceding 150 and following releases and checking for self-deadlock. 151 152 More formally, this file defines a performance-enhanced scheme 153 for generation of the possible reads-from and coherence order 154 relations on the locking primitives. 155 156README 157 This file. 158 159 160=========== 161LIMITATIONS 162=========== 163 164The Linux-kernel memory model has the following limitations: 165 1661. Compiler optimizations are not modeled. Of course, the use 167 of READ_ONCE() and WRITE_ONCE() limits the compiler's ability 168 to optimize, but there is Linux-kernel code that uses bare C 169 memory accesses. Handling this code is on the to-do list. 170 For more information, see Documentation/explanation.txt (in 171 particular, the "THE PROGRAM ORDER RELATION: po AND po-loc" 172 and "A WARNING" sections). 173 1742. Multiple access sizes for a single variable are not supported, 175 and neither are misaligned or partially overlapping accesses. 176 1773. Exceptions and interrupts are not modeled. In some cases, 178 this limitation can be overcome by modeling the interrupt or 179 exception with an additional process. 180 1814. I/O such as MMIO or DMA is not supported. 182 1835. Self-modifying code (such as that found in the kernel's 184 alternatives mechanism, function tracer, Berkeley Packet Filter 185 JIT compiler, and module loader) is not supported. 186 1876. Complete modeling of all variants of atomic read-modify-write 188 operations, locking primitives, and RCU is not provided. 189 For example, call_rcu() and rcu_barrier() are not supported. 190 However, a substantial amount of support is provided for these 191 operations, as shown in the linux-kernel.def file. 192 193The "herd7" tool has some additional limitations of its own, apart from 194the memory model: 195 1961. Non-trivial data structures such as arrays or structures are 197 not supported. However, pointers are supported, allowing trivial 198 linked lists to be constructed. 199 2002. Dynamic memory allocation is not supported, although this can 201 be worked around in some cases by supplying multiple statically 202 allocated variables. 203 204Some of these limitations may be overcome in the future, but others are 205more likely to be addressed by incorporating the Linux-kernel memory model 206into other tools. 207