1 ============================== 1 ===================================== 2 LINUX KERNEL MEMORY CONSISTENC 2 LINUX KERNEL MEMORY CONSISTENCY MODEL 3 ============================== 3 ===================================== 4 4 5 ============ 5 ============ 6 INTRODUCTION 6 INTRODUCTION 7 ============ 7 ============ 8 8 9 This directory contains the memory consistency 9 This directory contains the memory consistency model (memory model, for 10 short) of the Linux kernel, written in the "ca 10 short) of the Linux kernel, written in the "cat" language and executable 11 by the externally provided "herd7" simulator, 11 by the externally provided "herd7" simulator, which exhaustively explores 12 the state space of small litmus tests. 12 the state space of small litmus tests. 13 13 14 In addition, the "klitmus7" tool (also externa 14 In addition, the "klitmus7" tool (also externally provided) may be used 15 to convert a litmus test to a Linux kernel mod 15 to convert a litmus test to a Linux kernel module, which in turn allows 16 that litmus test to be exercised within the Li 16 that litmus test to be exercised within the Linux kernel. 17 17 18 18 19 ============ 19 ============ 20 REQUIREMENTS 20 REQUIREMENTS 21 ============ 21 ============ 22 22 23 Version 7.52 or higher of the "herd7" and "kli 23 Version 7.52 or higher of the "herd7" and "klitmus7" tools must be 24 downloaded separately: 24 downloaded separately: 25 25 26 https://github.com/herd/herdtools7 26 https://github.com/herd/herdtools7 27 27 28 See "herdtools7/INSTALL.md" for installation i 28 See "herdtools7/INSTALL.md" for installation instructions. 29 29 30 Note that although these tools usually provide 30 Note that although these tools usually provide backwards compatibility, 31 this is not absolutely guaranteed. !! 31 this is not absolutely guaranteed. Therefore, if a later version does 32 !! 32 not work, please try using the exact version called out above. 33 For example, a future version of herd7 might n << 34 in this release. A compatible model will like << 35 a later release of Linux kernel. << 36 << 37 If you absolutely need to run the model in thi << 38 please try using the exact version called out << 39 << 40 klitmus7 is independent of the model provided << 41 dependency on a target kernel release where co << 42 and executed. Any change in kernel APIs essen << 43 necessitate an upgrade of klitmus7. << 44 << 45 If you find any compatibility issues in klitmu << 46 memory model maintainers. << 47 << 48 klitmus7 Compatibility Table << 49 ---------------------------- << 50 << 51 ============ ========== << 52 target Linux herdtools7 << 53 ------------ ---------- << 54 -- 4.14 7.48 -- << 55 4.15 -- 4.19 7.49 -- << 56 4.20 -- 5.5 7.54 -- << 57 5.6 -- 5.16 7.56 -- << 58 5.17 -- 7.56.1 -- << 59 ============ ========== << 60 33 61 34 62 ================== 35 ================== 63 BASIC USAGE: HERD7 36 BASIC USAGE: HERD7 64 ================== 37 ================== 65 38 66 The memory model is used, in conjunction with 39 The memory model is used, in conjunction with "herd7", to exhaustively 67 explore the state space of small litmus tests. !! 40 explore the state space of small litmus tests. 68 the format, features, capabilities and limitat << 69 tests is available in tools/memory-model/Docum << 70 << 71 Example litmus tests may be found in the Linux << 72 << 73 tools/memory-model/litmus-tests/ << 74 Documentation/litmus-tests/ << 75 << 76 Several thousand more example litmus tests are << 77 << 78 https://github.com/paulmckrcu/litmus << 79 https://git.kernel.org/pub/scm/linux/k << 80 https://git.kernel.org/pub/scm/linux/k << 81 << 82 Documentation describing litmus tests and now << 83 here: << 84 << 85 tools/memory-model/Documentation/litmu << 86 << 87 The remainder of this section uses the SB+fenc << 88 located in the tools/memory-model directory. << 89 41 90 To run SB+fencembonceonces.litmus against the !! 42 For example, to run SB+fencembonceonces.litmus against the memory model: 91 43 92 $ cd $LINUX_SOURCE_TREE/tools/memory-model << 93 $ herd7 -conf linux-kernel.cfg litmus-tests/ 44 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus 94 45 95 Here is the corresponding output: 46 Here is the corresponding output: 96 47 97 Test SB+fencembonceonces Allowed 48 Test SB+fencembonceonces Allowed 98 States 3 49 States 3 99 0:r0=0; 1:r0=1; 50 0:r0=0; 1:r0=1; 100 0:r0=1; 1:r0=0; 51 0:r0=1; 1:r0=0; 101 0:r0=1; 1:r0=1; 52 0:r0=1; 1:r0=1; 102 No 53 No 103 Witnesses 54 Witnesses 104 Positive: 0 Negative: 3 55 Positive: 0 Negative: 3 105 Condition exists (0:r0=0 /\ 1:r0=0) 56 Condition exists (0:r0=0 /\ 1:r0=0) 106 Observation SB+fencembonceonces Never 0 3 57 Observation SB+fencembonceonces Never 0 3 107 Time SB+fencembonceonces 0.01 58 Time SB+fencembonceonces 0.01 108 Hash=d66d99523e2cac6b06e66f4c995ebb48 59 Hash=d66d99523e2cac6b06e66f4c995ebb48 109 60 110 The "Positive: 0 Negative: 3" and the "Never 0 61 The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that 111 this litmus test's "exists" clause can not be 62 this litmus test's "exists" clause can not be satisfied. 112 63 113 See "herd7 -help" or "herdtools7/doc/" for mor !! 64 See "herd7 -help" or "herdtools7/doc/" for more information. 114 tool itself, but please be aware that this doc << 115 people who work on the memory model itself, th << 116 to the tools/memory-model/linux-kernel.* files << 117 people focusing on writing, understanding, and << 118 65 119 66 120 ===================== 67 ===================== 121 BASIC USAGE: KLITMUS7 68 BASIC USAGE: KLITMUS7 122 ===================== 69 ===================== 123 70 124 The "klitmus7" tool converts a litmus test int 71 The "klitmus7" tool converts a litmus test into a Linux kernel module, 125 which may then be loaded and run. 72 which may then be loaded and run. 126 73 127 For example, to run SB+fencembonceonces.litmus 74 For example, to run SB+fencembonceonces.litmus against hardware: 128 75 129 $ mkdir mymodules 76 $ mkdir mymodules 130 $ klitmus7 -o mymodules litmus-tests/SB+fenc 77 $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus 131 $ cd mymodules ; make 78 $ cd mymodules ; make 132 $ sudo sh run.sh 79 $ sudo sh run.sh 133 80 134 The corresponding output includes: 81 The corresponding output includes: 135 82 136 Test SB+fencembonceonces Allowed 83 Test SB+fencembonceonces Allowed 137 Histogram (3 states) 84 Histogram (3 states) 138 644580 :>0:r0=1; 1:r0=0; 85 644580 :>0:r0=1; 1:r0=0; 139 644328 :>0:r0=0; 1:r0=1; 86 644328 :>0:r0=0; 1:r0=1; 140 711092 :>0:r0=1; 1:r0=1; 87 711092 :>0:r0=1; 1:r0=1; 141 No 88 No 142 Witnesses 89 Witnesses 143 Positive: 0, Negative: 2000000 90 Positive: 0, Negative: 2000000 144 Condition exists (0:r0=0 /\ 1:r0=0) is NOT v 91 Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated 145 Hash=d66d99523e2cac6b06e66f4c995ebb48 92 Hash=d66d99523e2cac6b06e66f4c995ebb48 146 Observation SB+fencembonceonces Never 0 2000 93 Observation SB+fencembonceonces Never 0 2000000 147 Time SB+fencembonceonces 0.16 94 Time SB+fencembonceonces 0.16 148 95 149 The "Positive: 0 Negative: 2000000" and the "N 96 The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate 150 that during two million trials, the state spec 97 that during two million trials, the state specified in this litmus 151 test's "exists" clause was not reached. 98 test's "exists" clause was not reached. 152 99 153 And, as with "herd7", please see "klitmus7 -he 100 And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/" 154 for more information. And again, please be aw !! 101 for more information. 155 is intended for people who work on the memory << 156 people making changes to the tools/memory-mode << 157 It is not intended for people focusing on writ << 158 running LKMM litmus tests. << 159 102 160 103 161 ==================== 104 ==================== 162 DESCRIPTION OF FILES 105 DESCRIPTION OF FILES 163 ==================== 106 ==================== 164 107 165 Documentation/README !! 108 Documentation/cheatsheet.txt 166 Guide to the other documents in the Do !! 109 Quick-reference guide to the Linux-kernel memory model. >> 110 >> 111 Documentation/explanation.txt >> 112 Describes the memory model in detail. >> 113 >> 114 Documentation/recipes.txt >> 115 Lists common memory-ordering patterns. >> 116 >> 117 Documentation/references.txt >> 118 Provides background reading. 167 119 168 linux-kernel.bell 120 linux-kernel.bell 169 Categorizes the relevant instructions, 121 Categorizes the relevant instructions, including memory 170 references, memory barriers, atomic re 122 references, memory barriers, atomic read-modify-write operations, 171 lock acquisition/release, and RCU oper 123 lock acquisition/release, and RCU operations. 172 124 173 More formally, this file (1) lists the 125 More formally, this file (1) lists the subtypes of the various 174 event types used by the memory model a 126 event types used by the memory model and (2) performs RCU 175 read-side critical section nesting ana 127 read-side critical section nesting analysis. 176 128 177 linux-kernel.cat 129 linux-kernel.cat 178 Specifies what reorderings are forbidd 130 Specifies what reorderings are forbidden by memory references, 179 memory barriers, atomic read-modify-wr 131 memory barriers, atomic read-modify-write operations, and RCU. 180 132 181 More formally, this file specifies wha 133 More formally, this file specifies what executions are forbidden 182 by the memory model. Allowed executio 134 by the memory model. Allowed executions are those which 183 satisfy the model's "coherence", "atom 135 satisfy the model's "coherence", "atomic", "happens-before", 184 "propagation", and "rcu" axioms, which 136 "propagation", and "rcu" axioms, which are defined in the file. 185 137 186 linux-kernel.cfg 138 linux-kernel.cfg 187 Convenience file that gathers the comm 139 Convenience file that gathers the common-case herd7 command-line 188 arguments. 140 arguments. 189 141 190 linux-kernel.def 142 linux-kernel.def 191 Maps from C-like syntax to herd7's int 143 Maps from C-like syntax to herd7's internal litmus-test 192 instruction-set architecture. 144 instruction-set architecture. 193 145 194 litmus-tests 146 litmus-tests 195 Directory containing a few representat 147 Directory containing a few representative litmus tests, which 196 are listed in litmus-tests/README. A 148 are listed in litmus-tests/README. A great deal more litmus 197 tests are available at https://github. 149 tests are available at https://github.com/paulmckrcu/litmus. 198 150 199 By "representative", it means the one << 200 directory is: << 201 << 202 1) simple, the number of threa << 203 small and each thread funct << 204 simple. << 205 2) orthogonal, there should be << 206 describing the same aspect << 207 3) textbook, developers can ea << 208 the litmus tests to use the << 209 code. << 210 << 211 lock.cat 151 lock.cat 212 Provides a front-end analysis of lock 152 Provides a front-end analysis of lock acquisition and release, 213 for example, associating a lock acquis 153 for example, associating a lock acquisition with the preceding 214 and following releases and checking fo 154 and following releases and checking for self-deadlock. 215 155 216 More formally, this file defines a per 156 More formally, this file defines a performance-enhanced scheme 217 for generation of the possible reads-f 157 for generation of the possible reads-from and coherence order 218 relations on the locking primitives. 158 relations on the locking primitives. 219 159 220 README 160 README 221 This file. 161 This file. 222 162 223 scripts Various scripts, see scripts/README. 163 scripts Various scripts, see scripts/README. >> 164 >> 165 >> 166 =========== >> 167 LIMITATIONS >> 168 =========== >> 169 >> 170 The Linux-kernel memory model (LKMM) has the following limitations: >> 171 >> 172 1. 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 >> 186 2. Multiple access sizes for a single variable are not supported, >> 187 and neither are misaligned or partially overlapping accesses. >> 188 >> 189 3. 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 >> 193 4. I/O such as MMIO or DMA is not supported. >> 194 >> 195 5. 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 >> 199 6. 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_add_unless(), >> 211 atomic_inc_unless_negative(), and >> 212 atomic_dec_unless_positive(). These can be emulated >> 213 in litmus tests, for example, by using atomic_cmpxchg(). >> 214 >> 215 c. The call_rcu() function is not modeled. It can be >> 216 emulated in litmus tests by adding another process that >> 217 invokes synchronize_rcu() and the body of the callback >> 218 function, with (for example) a release-acquire from >> 219 the site of the emulated call_rcu() to the beginning >> 220 of the additional process. >> 221 >> 222 d. The rcu_barrier() function is not modeled. It can be >> 223 emulated in litmus tests emulating call_rcu() via >> 224 (for example) a release-acquire from the end of each >> 225 additional call_rcu() process to the site of the >> 226 emulated rcu-barrier(). >> 227 >> 228 e. Although sleepable RCU (SRCU) is now modeled, there >> 229 are some subtle differences between its semantics and >> 230 those in the Linux kernel. For example, the kernel >> 231 might interpret the following sequence as two partially >> 232 overlapping SRCU read-side critical sections: >> 233 >> 234 1 r1 = srcu_read_lock(&my_srcu); >> 235 2 do_something_1(); >> 236 3 r2 = srcu_read_lock(&my_srcu); >> 237 4 do_something_2(); >> 238 5 srcu_read_unlock(&my_srcu, r1); >> 239 6 do_something_3(); >> 240 7 srcu_read_unlock(&my_srcu, r2); >> 241 >> 242 In contrast, LKMM will interpret this as a nested pair of >> 243 SRCU read-side critical sections, with the outer critical >> 244 section spanning lines 1-7 and the inner critical section >> 245 spanning lines 3-5. >> 246 >> 247 This difference would be more of a concern had anyone >> 248 identified a reasonable use case for partially overlapping >> 249 SRCU read-side critical sections. For more information, >> 250 please see: https://paulmck.livejournal.com/40593.html >> 251 >> 252 f. Reader-writer locking is not modeled. It can be >> 253 emulated in litmus tests using atomic read-modify-write >> 254 operations. >> 255 >> 256 The "herd7" tool has some additional limitations of its own, apart from >> 257 the memory model: >> 258 >> 259 1. Non-trivial data structures such as arrays or structures are >> 260 not supported. However, pointers are supported, allowing trivial >> 261 linked lists to be constructed. >> 262 >> 263 2. Dynamic memory allocation is not supported, although this can >> 264 be worked around in some cases by supplying multiple statically >> 265 allocated variables. >> 266 >> 267 Some of these limitations may be overcome in the future, but others are >> 268 more likely to be addressed by incorporating the Linux-kernel memory model >> 269 into other tools. >> 270 >> 271 Finally, please note that LKMM is subject to change as hardware, use cases, >> 272 and compilers evolve.
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.