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 159scripts Various scripts, see scripts/README. 160 161 162=========== 163LIMITATIONS 164=========== 165 166The Linux-kernel memory model has the following limitations: 167 1681. Compiler optimizations are not modeled. Of course, the use 169 of READ_ONCE() and WRITE_ONCE() limits the compiler's ability 170 to optimize, but there is Linux-kernel code that uses bare C 171 memory accesses. Handling this code is on the to-do list. 172 For more information, see Documentation/explanation.txt (in 173 particular, the "THE PROGRAM ORDER RELATION: po AND po-loc" 174 and "A WARNING" sections). 175 176 Note that this limitation in turn limits LKMM's ability to 177 accurately model address, control, and data dependencies. 178 For example, if the compiler can deduce the value of some variable 179 carrying a dependency, then the compiler can break that dependency 180 by substituting a constant of that value. 181 1822. Multiple access sizes for a single variable are not supported, 183 and neither are misaligned or partially overlapping accesses. 184 1853. Exceptions and interrupts are not modeled. In some cases, 186 this limitation can be overcome by modeling the interrupt or 187 exception with an additional process. 188 1894. I/O such as MMIO or DMA is not supported. 190 1915. Self-modifying code (such as that found in the kernel's 192 alternatives mechanism, function tracer, Berkeley Packet Filter 193 JIT compiler, and module loader) is not supported. 194 1956. Complete modeling of all variants of atomic read-modify-write 196 operations, locking primitives, and RCU is not provided. 197 For example, call_rcu() and rcu_barrier() are not supported. 198 However, a substantial amount of support is provided for these 199 operations, as shown in the linux-kernel.def file. 200 201 a. When rcu_assign_pointer() is passed NULL, the Linux 202 kernel provides no ordering, but LKMM models this 203 case as a store release. 204 205 b. The "unless" RMW operations are not currently modeled: 206 atomic_long_add_unless(), atomic_add_unless(), 207 atomic_inc_unless_negative(), and 208 atomic_dec_unless_positive(). These can be emulated 209 in litmus tests, for example, by using atomic_cmpxchg(). 210 211 c. The call_rcu() function is not modeled. It can be 212 emulated in litmus tests by adding another process that 213 invokes synchronize_rcu() and the body of the callback 214 function, with (for example) a release-acquire from 215 the site of the emulated call_rcu() to the beginning 216 of the additional process. 217 218 d. The rcu_barrier() function is not modeled. It can be 219 emulated in litmus tests emulating call_rcu() via 220 (for example) a release-acquire from the end of each 221 additional call_rcu() process to the site of the 222 emulated rcu-barrier(). 223 224 e. Sleepable RCU (SRCU) is not modeled. It can be 225 emulated, but perhaps not simply. 226 227 f. Reader-writer locking is not modeled. It can be 228 emulated in litmus tests using atomic read-modify-write 229 operations. 230 231The "herd7" tool has some additional limitations of its own, apart from 232the memory model: 233 2341. Non-trivial data structures such as arrays or structures are 235 not supported. However, pointers are supported, allowing trivial 236 linked lists to be constructed. 237 2382. Dynamic memory allocation is not supported, although this can 239 be worked around in some cases by supplying multiple statically 240 allocated variables. 241 242Some of these limitations may be overcome in the future, but others are 243more likely to be addressed by incorporating the Linux-kernel memory model 244into other tools. 245 246Finally, please note that LKMM is subject to change as hardware, use cases, 247and compilers evolve. 248