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