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