| 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.58 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 how 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. |