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