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.14 7.48 -- 55 4.15 -- 4.19 7.49 -- 56 4.20 -- 5.5 7.54 -- 57 5.6 -- 5.16 7.56 -- 58 5.17 -- 7.56.1 -- 59 ============ ========== 60 61 62 ================== 63 BASIC USAGE: HERD7 64 ================== 65 66 The memory model is used, in conjunction with "herd7", to exhaustively 67 explore the state space of small litmus tests. Documentation describing 68 the format, features, capabilities and limitations of these litmus 69 tests is available in tools/memory-model/Documentation/litmus-tests.txt. 70 71 Example litmus tests may be found in the Linux-kernel source tree: 72 73 tools/memory-model/litmus-tests/ 74 Documentation/litmus-tests/ 75 76 Several thousand more example litmus tests are available here: 77 78 https://github.com/paulmckrcu/litmus 79 https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd 80 https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus 81 82 Documentation describing litmus tests and now to use them may be found 83 here: 84 85 tools/memory-model/Documentation/litmus-tests.txt 86 87 The remainder of this section uses the SB+fencembonceonces.litmus test 88 located in the tools/memory-model directory. 89 90 To run SB+fencembonceonces.litmus against the memory model: 91 92 $ cd $LINUX_SOURCE_TREE/tools/memory-model 93 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus 94 95 Here is the corresponding output: 96 97 Test SB+fencembonceonces Allowed 98 States 3 99 0:r0=0; 1:r0=1; 100 0:r0=1; 1:r0=0; 101 0:r0=1; 1:r0=1; 102 No 103 Witnesses 104 Positive: 0 Negative: 3 105 Condition exists (0:r0=0 /\ 1:r0=0) 106 Observation SB+fencembonceonces Never 0 3 107 Time SB+fencembonceonces 0.01 108 Hash=d66d99523e2cac6b06e66f4c995ebb48 109 110 The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that 111 this litmus test's "exists" clause can not be satisfied. 112 113 See "herd7 -help" or "herdtools7/doc/" for more information on running the 114 tool itself, but please be aware that this documentation is intended for 115 people who work on the memory model itself, that is, people making changes 116 to the tools/memory-model/linux-kernel.* files. It is not intended for 117 people focusing on writing, understanding, and running LKMM litmus tests. 118 119 120 ===================== 121 BASIC USAGE: KLITMUS7 122 ===================== 123 124 The "klitmus7" tool converts a litmus test into a Linux kernel module, 125 which may then be loaded and run. 126 127 For example, to run SB+fencembonceonces.litmus against hardware: 128 129 $ mkdir mymodules 130 $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus 131 $ cd mymodules ; make 132 $ sudo sh run.sh 133 134 The corresponding output includes: 135 136 Test SB+fencembonceonces Allowed 137 Histogram (3 states) 138 644580 :>0:r0=1; 1:r0=0; 139 644328 :>0:r0=0; 1:r0=1; 140 711092 :>0:r0=1; 1:r0=1; 141 No 142 Witnesses 143 Positive: 0, Negative: 2000000 144 Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated 145 Hash=d66d99523e2cac6b06e66f4c995ebb48 146 Observation SB+fencembonceonces Never 0 2000000 147 Time SB+fencembonceonces 0.16 148 149 The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate 150 that during two million trials, the state specified in this litmus 151 test's "exists" clause was not reached. 152 153 And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/" 154 for more information. And again, please be aware that this documentation 155 is intended for people who work on the memory model itself, that is, 156 people making changes to the tools/memory-model/linux-kernel.* files. 157 It is not intended for people focusing on writing, understanding, and 158 running LKMM litmus tests. 159 160 161 ==================== 162 DESCRIPTION OF FILES 163 ==================== 164 165 Documentation/README 166 Guide to the other documents in the Documentation/ directory. 167 168 linux-kernel.bell 169 Categorizes the relevant instructions, including memory 170 references, memory barriers, atomic read-modify-write operations, 171 lock acquisition/release, and RCU operations. 172 173 More formally, this file (1) lists the subtypes of the various 174 event types used by the memory model and (2) performs RCU 175 read-side critical section nesting analysis. 176 177 linux-kernel.cat 178 Specifies what reorderings are forbidden by memory references, 179 memory barriers, atomic read-modify-write operations, and RCU. 180 181 More formally, this file specifies what executions are forbidden 182 by the memory model. Allowed executions are those which 183 satisfy the model's "coherence", "atomic", "happens-before", 184 "propagation", and "rcu" axioms, which are defined in the file. 185 186 linux-kernel.cfg 187 Convenience file that gathers the common-case herd7 command-line 188 arguments. 189 190 linux-kernel.def 191 Maps from C-like syntax to herd7's internal litmus-test 192 instruction-set architecture. 193 194 litmus-tests 195 Directory containing a few representative litmus tests, which 196 are listed in litmus-tests/README. A great deal more litmus 197 tests are available at https://github.com/paulmckrcu/litmus. 198 199 By "representative", it means the one in the litmus-tests 200 directory is: 201 202 1) simple, the number of threads should be relatively 203 small and each thread function should be relatively 204 simple. 205 2) orthogonal, there should be no two litmus tests 206 describing the same aspect of the memory model. 207 3) textbook, developers can easily copy-paste-modify 208 the litmus tests to use the patterns on their own 209 code. 210 211 lock.cat 212 Provides a front-end analysis of lock acquisition and release, 213 for example, associating a lock acquisition with the preceding 214 and following releases and checking for self-deadlock. 215 216 More formally, this file defines a performance-enhanced scheme 217 for generation of the possible reads-from and coherence order 218 relations on the locking primitives. 219 220 README 221 This file. 222 223 scripts Various scripts, see scripts/README.
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.