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+fencembonceonces.litmus against the memory model: 39 40 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus 41 42Here is the corresponding output: 43 44 Test SB+fencembonceonces 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+fencembonceonces Never 0 3 54 Time SB+fencembonceonces 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+fencembonceonces.litmus against hardware: 71 72 $ mkdir mymodules 73 $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus 74 $ cd mymodules ; make 75 $ sudo sh run.sh 76 77The corresponding output includes: 78 79 Test SB+fencembonceonces 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+fencembonceonces Never 0 2000000 90 Time SB+fencembonceonces 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 174 Note that this limitation in turn limits LKMM's ability to 175 accurately model address, control, and data dependencies. 176 For example, if the compiler can deduce the value of some variable 177 carrying a dependency, then the compiler can break that dependency 178 by substituting a constant of that value. 179 1802. Multiple access sizes for a single variable are not supported, 181 and neither are misaligned or partially overlapping accesses. 182 1833. Exceptions and interrupts are not modeled. In some cases, 184 this limitation can be overcome by modeling the interrupt or 185 exception with an additional process. 186 1874. I/O such as MMIO or DMA is not supported. 188 1895. Self-modifying code (such as that found in the kernel's 190 alternatives mechanism, function tracer, Berkeley Packet Filter 191 JIT compiler, and module loader) is not supported. 192 1936. Complete modeling of all variants of atomic read-modify-write 194 operations, locking primitives, and RCU is not provided. 195 For example, call_rcu() and rcu_barrier() are not supported. 196 However, a substantial amount of support is provided for these 197 operations, as shown in the linux-kernel.def file. 198 199 a. When rcu_assign_pointer() is passed NULL, the Linux 200 kernel provides no ordering, but LKMM models this 201 case as a store release. 202 203 b. The "unless" RMW operations are not currently modeled: 204 atomic_long_add_unless(), atomic_add_unless(), 205 atomic_inc_unless_negative(), and 206 atomic_dec_unless_positive(). These can be emulated 207 in litmus tests, for example, by using atomic_cmpxchg(). 208 209 c. The call_rcu() function is not modeled. It can be 210 emulated in litmus tests by adding another process that 211 invokes synchronize_rcu() and the body of the callback 212 function, with (for example) a release-acquire from 213 the site of the emulated call_rcu() to the beginning 214 of the additional process. 215 216 d. The rcu_barrier() function is not modeled. It can be 217 emulated in litmus tests emulating call_rcu() via 218 (for example) a release-acquire from the end of each 219 additional call_rcu() process to the site of the 220 emulated rcu-barrier(). 221 222 e. Sleepable RCU (SRCU) is not modeled. It can be 223 emulated, but perhaps not simply. 224 225 f. Reader-writer locking is not modeled. It can be 226 emulated in litmus tests using atomic read-modify-write 227 operations. 228 229The "herd7" tool has some additional limitations of its own, apart from 230the memory model: 231 2321. Non-trivial data structures such as arrays or structures are 233 not supported. However, pointers are supported, allowing trivial 234 linked lists to be constructed. 235 2362. Dynamic memory allocation is not supported, although this can 237 be worked around in some cases by supplying multiple statically 238 allocated variables. 239 240Some of these limitations may be overcome in the future, but others are 241more likely to be addressed by incorporating the Linux-kernel memory model 242into other tools. 243 244Finally, please note that LKMM is subject to change as hardware, use cases, 245and compilers evolve. 246