224 lines · plain
1 =====================================2 LINUX KERNEL MEMORY CONSISTENCY MODEL3 =====================================4 5============6INTRODUCTION7============8 9This directory contains the memory consistency model (memory model, for10short) of the Linux kernel, written in the "cat" language and executable11by the externally provided "herd7" simulator, which exhaustively explores12the state space of small litmus tests.13 14In addition, the "klitmus7" tool (also externally provided) may be used15to convert a litmus test to a Linux kernel module, which in turn allows16that litmus test to be exercised within the Linux kernel.17 18 19============20REQUIREMENTS21============22 23Version 7.52 or higher of the "herd7" and "klitmus7" tools must be24downloaded separately:25 26 https://github.com/herd/herdtools727 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 model34in this release. A compatible model will likely be made available in35a 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 own41dependency on a target kernel release where converted code is built42and executed. Any change in kernel APIs essential to klitmus7 will43necessitate an upgrade of klitmus7.44 45If you find any compatibility issues in klitmus7, please inform the46memory model maintainers.47 48klitmus7 Compatibility Table49----------------------------50 51 ============ ==========52 target Linux herdtools753 ------------ ----------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==================63BASIC USAGE: HERD764==================65 66The memory model is used, in conjunction with "herd7", to exhaustively67explore the state space of small litmus tests. Documentation describing68the format, features, capabilities and limitations of these litmus69tests is available in tools/memory-model/Documentation/litmus-tests.txt.70 71Example litmus tests may be found in the Linux-kernel source tree:72 73 tools/memory-model/litmus-tests/74 Documentation/litmus-tests/75 76Several thousand more example litmus tests are available here:77 78 https://github.com/paulmckrcu/litmus79 https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd80 https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus81 82Documentation describing litmus tests and now to use them may be found83here:84 85 tools/memory-model/Documentation/litmus-tests.txt86 87The remainder of this section uses the SB+fencembonceonces.litmus test88located in the tools/memory-model directory.89 90To run SB+fencembonceonces.litmus against the memory model:91 92 $ cd $LINUX_SOURCE_TREE/tools/memory-model93 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus94 95Here is the corresponding output:96 97 Test SB+fencembonceonces Allowed98 States 399 0:r0=0; 1:r0=1;100 0:r0=1; 1:r0=0;101 0:r0=1; 1:r0=1;102 No103 Witnesses104 Positive: 0 Negative: 3105 Condition exists (0:r0=0 /\ 1:r0=0)106 Observation SB+fencembonceonces Never 0 3107 Time SB+fencembonceonces 0.01108 Hash=d66d99523e2cac6b06e66f4c995ebb48109 110The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that111this litmus test's "exists" clause can not be satisfied.112 113See "herd7 -help" or "herdtools7/doc/" for more information on running the114tool itself, but please be aware that this documentation is intended for115people who work on the memory model itself, that is, people making changes116to the tools/memory-model/linux-kernel.* files. It is not intended for117people focusing on writing, understanding, and running LKMM litmus tests.118 119 120=====================121BASIC USAGE: KLITMUS7122=====================123 124The "klitmus7" tool converts a litmus test into a Linux kernel module,125which may then be loaded and run.126 127For example, to run SB+fencembonceonces.litmus against hardware:128 129 $ mkdir mymodules130 $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus131 $ cd mymodules ; make132 $ sudo sh run.sh133 134The corresponding output includes:135 136 Test SB+fencembonceonces Allowed137 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 No142 Witnesses143 Positive: 0, Negative: 2000000144 Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated145 Hash=d66d99523e2cac6b06e66f4c995ebb48146 Observation SB+fencembonceonces Never 0 2000000147 Time SB+fencembonceonces 0.16148 149The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate150that during two million trials, the state specified in this litmus151test's "exists" clause was not reached.152 153And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"154for more information. And again, please be aware that this documentation155is intended for people who work on the memory model itself, that is,156people making changes to the tools/memory-model/linux-kernel.* files.157It is not intended for people focusing on writing, understanding, and158running LKMM litmus tests.159 160 161====================162DESCRIPTION OF FILES163====================164 165Documentation/README166 Guide to the other documents in the Documentation/ directory.167 168linux-kernel.bell169 Categorizes the relevant instructions, including memory170 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 various174 event types used by the memory model and (2) performs RCU175 read-side critical section nesting analysis.176 177linux-kernel.cat178 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 forbidden182 by the memory model. Allowed executions are those which183 satisfy the model's "coherence", "atomic", "happens-before",184 "propagation", and "rcu" axioms, which are defined in the file.185 186linux-kernel.cfg187 Convenience file that gathers the common-case herd7 command-line188 arguments.189 190linux-kernel.def191 Maps from C-like syntax to herd7's internal litmus-test192 instruction-set architecture.193 194litmus-tests195 Directory containing a few representative litmus tests, which196 are listed in litmus-tests/README. A great deal more litmus197 tests are available at https://github.com/paulmckrcu/litmus.198 199 By "representative", it means the one in the litmus-tests200 directory is:201 202 1) simple, the number of threads should be relatively203 small and each thread function should be relatively204 simple.205 2) orthogonal, there should be no two litmus tests206 describing the same aspect of the memory model.207 3) textbook, developers can easily copy-paste-modify208 the litmus tests to use the patterns on their own209 code.210 211lock.cat212 Provides a front-end analysis of lock acquisition and release,213 for example, associating a lock acquisition with the preceding214 and following releases and checking for self-deadlock.215 216 More formally, this file defines a performance-enhanced scheme217 for generation of the possible reads-from and coherence order218 relations on the locking primitives.219 220README221 This file.222 223scripts Various scripts, see scripts/README.224