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.48 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 30Alternatively, Abhishek Bhardwaj has kindly provided a Docker image 31of these tools at "abhishek40/memory-model". Abhishek suggests the 32following commands to install and use this image: 33 34 - Users should install Docker for their distribution. 35 - docker run -itd abhishek40/memory-model 36 - docker attach <id-emitted-from-the-previous-command> 37 38Gentoo users might wish to make use of Patrick McLean's package: 39 40 https://gitweb.gentoo.org/repo/gentoo.git/tree/dev-util/herdtools7 41 42These packages may not be up-to-date with respect to the GitHub 43repository. 44 45 46================== 47BASIC USAGE: HERD7 48================== 49 50The memory model is used, in conjunction with "herd7", to exhaustively 51explore the state space of small litmus tests. 52 53For example, to run SB+mbonceonces.litmus against the memory model: 54 55 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+mbonceonces.litmus 56 57Here is the corresponding output: 58 59 Test SB+mbonceonces Allowed 60 States 3 61 0:r0=0; 1:r0=1; 62 0:r0=1; 1:r0=0; 63 0:r0=1; 1:r0=1; 64 No 65 Witnesses 66 Positive: 0 Negative: 3 67 Condition exists (0:r0=0 /\ 1:r0=0) 68 Observation SB+mbonceonces Never 0 3 69 Time SB+mbonceonces 0.01 70 Hash=d66d99523e2cac6b06e66f4c995ebb48 71 72The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that 73this litmus test's "exists" clause can not be satisfied. 74 75See "herd7 -help" or "herdtools7/doc/" for more information. 76 77 78===================== 79BASIC USAGE: KLITMUS7 80===================== 81 82The "klitmus7" tool converts a litmus test into a Linux kernel module, 83which may then be loaded and run. 84 85For example, to run SB+mbonceonces.litmus against hardware: 86 87 $ mkdir mymodules 88 $ klitmus7 -o mymodules litmus-tests/SB+mbonceonces.litmus 89 $ cd mymodules ; make 90 $ sudo sh run.sh 91 92The corresponding output includes: 93 94 Test SB+mbonceonces Allowed 95 Histogram (3 states) 96 644580 :>0:r0=1; 1:r0=0; 97 644328 :>0:r0=0; 1:r0=1; 98 711092 :>0:r0=1; 1:r0=1; 99 No 100 Witnesses 101 Positive: 0, Negative: 2000000 102 Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated 103 Hash=d66d99523e2cac6b06e66f4c995ebb48 104 Observation SB+mbonceonces Never 0 2000000 105 Time SB+mbonceonces 0.16 106 107The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate 108that during two million trials, the state specified in this litmus 109test's "exists" clause was not reached. 110 111And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/" 112for more information. 113 114 115==================== 116DESCRIPTION OF FILES 117==================== 118 119Documentation/cheatsheet.txt 120 Quick-reference guide to the Linux-kernel memory model. 121 122Documentation/explanation.txt 123 Describes the memory model in detail. 124 125Documentation/recipes.txt 126 Lists common memory-ordering patterns. 127 128Documentation/references.txt 129 Provides background reading. 130 131linux-kernel.bell 132 Categorizes the relevant instructions, including memory 133 references, memory barriers, atomic read-modify-write operations, 134 lock acquisition/release, and RCU operations. 135 136 More formally, this file (1) lists the subtypes of the various 137 event types used by the memory model and (2) performs RCU 138 read-side critical section nesting analysis. 139 140linux-kernel.cat 141 Specifies what reorderings are forbidden by memory references, 142 memory barriers, atomic read-modify-write operations, and RCU. 143 144 More formally, this file specifies what executions are forbidden 145 by the memory model. Allowed executions are those which 146 satisfy the model's "coherence", "atomic", "happens-before", 147 "propagation", and "rcu" axioms, which are defined in the file. 148 149linux-kernel.cfg 150 Convenience file that gathers the common-case herd7 command-line 151 arguments. 152 153linux-kernel.def 154 Maps from C-like syntax to herd7's internal litmus-test 155 instruction-set architecture. 156 157litmus-tests 158 Directory containing a few representative litmus tests, which 159 are listed in litmus-tests/README. A great deal more litmus 160 tests are available at https://github.com/paulmckrcu/litmus. 161 162lock.cat 163 Provides a front-end analysis of lock acquisition and release, 164 for example, associating a lock acquisition with the preceding 165 and following releases and checking for self-deadlock. 166 167 More formally, this file defines a performance-enhanced scheme 168 for generation of the possible reads-from and coherence order 169 relations on the locking primitives. 170 171README 172 This file. 173 174 175=========== 176LIMITATIONS 177=========== 178 179The Linux-kernel memory model has the following limitations: 180 1811. Compiler optimizations are not modeled. Of course, the use 182 of READ_ONCE() and WRITE_ONCE() limits the compiler's ability 183 to optimize, but there is Linux-kernel code that uses bare C 184 memory accesses. Handling this code is on the to-do list. 185 For more information, see Documentation/explanation.txt (in 186 particular, the "THE PROGRAM ORDER RELATION: po AND po-loc" 187 and "A WARNING" sections). 188 1892. Multiple access sizes for a single variable are not supported, 190 and neither are misaligned or partially overlapping accesses. 191 1923. Exceptions and interrupts are not modeled. In some cases, 193 this limitation can be overcome by modeling the interrupt or 194 exception with an additional process. 195 1964. I/O such as MMIO or DMA is not supported. 197 1985. Self-modifying code (such as that found in the kernel's 199 alternatives mechanism, function tracer, Berkeley Packet Filter 200 JIT compiler, and module loader) is not supported. 201 2026. Complete modeling of all variants of atomic read-modify-write 203 operations, locking primitives, and RCU is not provided. 204 For example, call_rcu() and rcu_barrier() are not supported. 205 However, a substantial amount of support is provided for these 206 operations, as shown in the linux-kernel.def file. 207 208The "herd7" tool has some additional limitations of its own, apart from 209the memory model: 210 2111. Non-trivial data structures such as arrays or structures are 212 not supported. However, pointers are supported, allowing trivial 213 linked lists to be constructed. 214 2152. Dynamic memory allocation is not supported, although this can 216 be worked around in some cases by supplying multiple statically 217 allocated variables. 218 219Some of these limitations may be overcome in the future, but others are 220more likely to be addressed by incorporating the Linux-kernel memory model 221into other tools. 222