| Name | Size | Last modified (GMT) | Description | |
|
| Parent directory | 2020-12-29 06:16:13 | ||
|
| Documentation/ | 2020-12-29 06:16:11 | ||
|
| litmus-tests/ | 2020-12-29 06:16:11 | ||
|
| scripts/ | 2020-12-29 06:16:11 | ||
|
| README | 10203 bytes | 2020-12-29 06:16:11 | |
|
| linux-kernel.bell | 3159 bytes | 2020-12-29 06:16:11 | |
|
| linux-kernel.cat | 7232 bytes | 2020-12-29 06:16:11 | |
|
| linux-kernel.cfg | 391 bytes | 2020-12-29 06:16:11 | |
|
| linux-kernel.def | 4705 bytes | 2020-12-29 06:16:11 | |
|
| lock.cat | 4634 bytes | 2020-12-29 06:16:11 |
1 ===================================== 2 LINUX KERNEL MEMORY CONSISTENCY MODEL 3 ===================================== 4 5 ============ 6 INTRODUCTION 7 ============ 8 9 This directory contains the memory consistency model (memory model, for 10 short) of the Linux kernel, written in the "cat" language and executable 11 by the externally provided "herd7" simulator, which exhaustively explores 12 the state space of small litmus tests. 13 14 In addition, the "klitmus7" tool (also externally provided) may be used 15 to convert a litmus test to a Linux kernel module, which in turn allows 16 that litmus test to be exercised within the Linux kernel. 17 18 19 ============ 20 REQUIREMENTS 21 ============ 22 23 Version 7.52 or higher of the "herd7" and "klitmus7" tools must be 24 downloaded separately: 25 26 https://github.com/herd/herdtools7 27 28 See "herdtools7/INSTALL.md" for installation instructions. 29 30 Note that although these tools usually provide backwards compatibility, 31 this is not absolutely guaranteed. 32 33 For example, a future version of herd7 might not work with the model 34 in this release. A compatible model will likely be made available in 35 a later release of Linux kernel. 36 37 If you absolutely need to run the model in this particular release, 38 please try using the exact version called out above. 39 40 klitmus7 is independent of the model provided here. It has its own 41 dependency on a target kernel release where converted code is built 42 and executed. Any change in kernel APIs essential to klitmus7 will 43 necessitate an upgrade of klitmus7. 44 45 If you find any compatibility issues in klitmus7, please inform the 46 memory model maintainers. 47 48 klitmus7 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 ================== 62 BASIC USAGE: HERD7 63 ================== 64 65 The memory model is used, in conjunction with "herd7", to exhaustively 66 explore the state space of small litmus tests. 67 68 For example, to run SB+fencembonceonces.litmus against the memory model: 69 70 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus 71 72 Here 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 87 The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that 88 this litmus test's "exists" clause can not be satisfied. 89 90 See "herd7 -help" or "herdtools7/doc/" for more information. 91 92 93 ===================== 94 BASIC USAGE: KLITMUS7 95 ===================== 96 97 The "klitmus7" tool converts a litmus test into a Linux kernel module, 98 which may then be loaded and run. 99 100 For 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 107 The 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 122 The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate 123 that during two million trials, the state specified in this litmus 124 test's "exists" clause was not reached. 125 126 And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/" 127 for more information. 128 129 130 ==================== 131 DESCRIPTION OF FILES 132 ==================== 133 134 Documentation/cheatsheet.txt 135 Quick-reference guide to the Linux-kernel memory model. 136 137 Documentation/explanation.txt 138 Describes the memory model in detail. 139 140 Documentation/recipes.txt 141 Lists common memory-ordering patterns. 142 143 Documentation/references.txt 144 Provides background reading. 145 146 linux-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 155 linux-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 164 linux-kernel.cfg 165 Convenience file that gathers the common-case herd7 command-line 166 arguments. 167 168 linux-kernel.def 169 Maps from C-like syntax to herd7's internal litmus-test 170 instruction-set architecture. 171 172 litmus-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 177 lock.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 186 README 187 This file. 188 189 scripts Various scripts, see scripts/README. 190 191 192 =========== 193 LIMITATIONS 194 =========== 195 196 The Linux-kernel memory model (LKMM) has the following limitations: 197 198 1. 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 212 2. Multiple access sizes for a single variable are not supported, 213 and neither are misaligned or partially overlapping accesses. 214 215 3. 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 219 4. I/O such as MMIO or DMA is not supported. 220 221 5. 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 225 6. 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 286 The "herd7" tool has some additional limitations of its own, apart from 287 the memory model: 288 289 1. 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 293 2. Dynamic memory allocation is not supported, although this can 294 be worked around in some cases by supplying multiple statically 295 allocated variables. 296 297 Some of these limitations may be overcome in the future, but others are 298 more likely to be addressed by incorporating the Linux-kernel memory model 299 into other tools. 300 301 Finally, please note that LKMM is subject to change as hardware, use cases, 302 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.
