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.52 or higher of the "herd7" and "klitmus7" tools must be 24downloaded separately: 25 26 https://github.com/herd/herdtools7 27 28See "herdtools7/INSTALL.md" for installation instructions. 29 30Note that although these tools usually provide backwards compatibility, 31this is not absolutely guaranteed. Therefore, if a later version does 32not work, please try using the exact version called out above. 33 34 35================== 36BASIC USAGE: HERD7 37================== 38 39The memory model is used, in conjunction with "herd7", to exhaustively 40explore the state space of small litmus tests. 41 42For example, to run SB+fencembonceonces.litmus against the memory model: 43 44 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus 45 46Here is the corresponding output: 47 48 Test SB+fencembonceonces Allowed 49 States 3 50 0:r0=0; 1:r0=1; 51 0:r0=1; 1:r0=0; 52 0:r0=1; 1:r0=1; 53 No 54 Witnesses 55 Positive: 0 Negative: 3 56 Condition exists (0:r0=0 /\ 1:r0=0) 57 Observation SB+fencembonceonces Never 0 3 58 Time SB+fencembonceonces 0.01 59 Hash=d66d99523e2cac6b06e66f4c995ebb48 60 61The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that 62this litmus test's "exists" clause can not be satisfied. 63 64See "herd7 -help" or "herdtools7/doc/" for more information. 65 66 67===================== 68BASIC USAGE: KLITMUS7 69===================== 70 71The "klitmus7" tool converts a litmus test into a Linux kernel module, 72which may then be loaded and run. 73 74For example, to run SB+fencembonceonces.litmus against hardware: 75 76 $ mkdir mymodules 77 $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus 78 $ cd mymodules ; make 79 $ sudo sh run.sh 80 81The corresponding output includes: 82 83 Test SB+fencembonceonces Allowed 84 Histogram (3 states) 85 644580 :>0:r0=1; 1:r0=0; 86 644328 :>0:r0=0; 1:r0=1; 87 711092 :>0:r0=1; 1:r0=1; 88 No 89 Witnesses 90 Positive: 0, Negative: 2000000 91 Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated 92 Hash=d66d99523e2cac6b06e66f4c995ebb48 93 Observation SB+fencembonceonces Never 0 2000000 94 Time SB+fencembonceonces 0.16 95 96The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate 97that during two million trials, the state specified in this litmus 98test's "exists" clause was not reached. 99 100And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/" 101for more information. 102 103 104==================== 105DESCRIPTION OF FILES 106==================== 107 108Documentation/cheatsheet.txt 109 Quick-reference guide to the Linux-kernel memory model. 110 111Documentation/explanation.txt 112 Describes the memory model in detail. 113 114Documentation/recipes.txt 115 Lists common memory-ordering patterns. 116 117Documentation/references.txt 118 Provides background reading. 119 120linux-kernel.bell 121 Categorizes the relevant instructions, including memory 122 references, memory barriers, atomic read-modify-write operations, 123 lock acquisition/release, and RCU operations. 124 125 More formally, this file (1) lists the subtypes of the various 126 event types used by the memory model and (2) performs RCU 127 read-side critical section nesting analysis. 128 129linux-kernel.cat 130 Specifies what reorderings are forbidden by memory references, 131 memory barriers, atomic read-modify-write operations, and RCU. 132 133 More formally, this file specifies what executions are forbidden 134 by the memory model. Allowed executions are those which 135 satisfy the model's "coherence", "atomic", "happens-before", 136 "propagation", and "rcu" axioms, which are defined in the file. 137 138linux-kernel.cfg 139 Convenience file that gathers the common-case herd7 command-line 140 arguments. 141 142linux-kernel.def 143 Maps from C-like syntax to herd7's internal litmus-test 144 instruction-set architecture. 145 146litmus-tests 147 Directory containing a few representative litmus tests, which 148 are listed in litmus-tests/README. A great deal more litmus 149 tests are available at https://github.com/paulmckrcu/litmus. 150 151lock.cat 152 Provides a front-end analysis of lock acquisition and release, 153 for example, associating a lock acquisition with the preceding 154 and following releases and checking for self-deadlock. 155 156 More formally, this file defines a performance-enhanced scheme 157 for generation of the possible reads-from and coherence order 158 relations on the locking primitives. 159 160README 161 This file. 162 163scripts Various scripts, see scripts/README. 164 165 166=========== 167LIMITATIONS 168=========== 169 170The Linux-kernel memory model (LKMM) has the following limitations: 171 1721. Compiler optimizations are not accurately modeled. Of course, 173 the use of READ_ONCE() and WRITE_ONCE() limits the compiler's 174 ability to optimize, but under some circumstances it is possible 175 for the compiler to undermine the memory model. For more 176 information, see Documentation/explanation.txt (in particular, 177 the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING" 178 sections). 179 180 Note that this limitation in turn limits LKMM's ability to 181 accurately model address, control, and data dependencies. 182 For example, if the compiler can deduce the value of some variable 183 carrying a dependency, then the compiler can break that dependency 184 by substituting a constant of that value. 185 1862. Multiple access sizes for a single variable are not supported, 187 and neither are misaligned or partially overlapping accesses. 188 1893. Exceptions and interrupts are not modeled. In some cases, 190 this limitation can be overcome by modeling the interrupt or 191 exception with an additional process. 192 1934. I/O such as MMIO or DMA is not supported. 194 1955. Self-modifying code (such as that found in the kernel's 196 alternatives mechanism, function tracer, Berkeley Packet Filter 197 JIT compiler, and module loader) is not supported. 198 1996. Complete modeling of all variants of atomic read-modify-write 200 operations, locking primitives, and RCU is not provided. 201 For example, call_rcu() and rcu_barrier() are not supported. 202 However, a substantial amount of support is provided for these 203 operations, as shown in the linux-kernel.def file. 204 205 a. When rcu_assign_pointer() is passed NULL, the Linux 206 kernel provides no ordering, but LKMM models this 207 case as a store release. 208 209 b. The "unless" RMW operations are not currently modeled: 210 atomic_long_add_unless(), atomic_inc_unless_negative(), 211 and atomic_dec_unless_positive(). These can be emulated 212 in litmus tests, for example, by using atomic_cmpxchg(). 213 214 One exception of this limitation is atomic_add_unless(), 215 which is provided directly by herd7 (so no corresponding 216 definition in linux-kernel.def). atomic_add_unless() is 217 modeled by herd7 therefore it can be used in litmus tests. 218 219 c. The call_rcu() function is not modeled. It can be 220 emulated in litmus tests by adding another process that 221 invokes synchronize_rcu() and the body of the callback 222 function, with (for example) a release-acquire from 223 the site of the emulated call_rcu() to the beginning 224 of the additional process. 225 226 d. The rcu_barrier() function is not modeled. It can be 227 emulated in litmus tests emulating call_rcu() via 228 (for example) a release-acquire from the end of each 229 additional call_rcu() process to the site of the 230 emulated rcu-barrier(). 231 232 e. Although sleepable RCU (SRCU) is now modeled, there 233 are some subtle differences between its semantics and 234 those in the Linux kernel. For example, the kernel 235 might interpret the following sequence as two partially 236 overlapping SRCU read-side critical sections: 237 238 1 r1 = srcu_read_lock(&my_srcu); 239 2 do_something_1(); 240 3 r2 = srcu_read_lock(&my_srcu); 241 4 do_something_2(); 242 5 srcu_read_unlock(&my_srcu, r1); 243 6 do_something_3(); 244 7 srcu_read_unlock(&my_srcu, r2); 245 246 In contrast, LKMM will interpret this as a nested pair of 247 SRCU read-side critical sections, with the outer critical 248 section spanning lines 1-7 and the inner critical section 249 spanning lines 3-5. 250 251 This difference would be more of a concern had anyone 252 identified a reasonable use case for partially overlapping 253 SRCU read-side critical sections. For more information, 254 please see: https://paulmck.livejournal.com/40593.html 255 256 f. Reader-writer locking is not modeled. It can be 257 emulated in litmus tests using atomic read-modify-write 258 operations. 259 260The "herd7" tool has some additional limitations of its own, apart from 261the memory model: 262 2631. Non-trivial data structures such as arrays or structures are 264 not supported. However, pointers are supported, allowing trivial 265 linked lists to be constructed. 266 2672. Dynamic memory allocation is not supported, although this can 268 be worked around in some cases by supplying multiple statically 269 allocated variables. 270 271Some of these limitations may be overcome in the future, but others are 272more likely to be addressed by incorporating the Linux-kernel memory model 273into other tools. 274 275Finally, please note that LKMM is subject to change as hardware, use cases, 276and compilers evolve. 277