0001 =====================================
0002 LINUX KERNEL MEMORY CONSISTENCY MODEL
0003 =====================================
0004
0005 ============
0006 INTRODUCTION
0007 ============
0008
0009 This directory contains the memory consistency model (memory model, for
0010 short) of the Linux kernel, written in the "cat" language and executable
0011 by the externally provided "herd7" simulator, which exhaustively explores
0012 the state space of small litmus tests.
0013
0014 In addition, the "klitmus7" tool (also externally provided) may be used
0015 to convert a litmus test to a Linux kernel module, which in turn allows
0016 that litmus test to be exercised within the Linux kernel.
0017
0018
0019 ============
0020 REQUIREMENTS
0021 ============
0022
0023 Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
0024 downloaded separately:
0025
0026 https://github.com/herd/herdtools7
0027
0028 See "herdtools7/INSTALL.md" for installation instructions.
0029
0030 Note that although these tools usually provide backwards compatibility,
0031 this is not absolutely guaranteed.
0032
0033 For example, a future version of herd7 might not work with the model
0034 in this release. A compatible model will likely be made available in
0035 a later release of Linux kernel.
0036
0037 If you absolutely need to run the model in this particular release,
0038 please try using the exact version called out above.
0039
0040 klitmus7 is independent of the model provided here. It has its own
0041 dependency on a target kernel release where converted code is built
0042 and executed. Any change in kernel APIs essential to klitmus7 will
0043 necessitate an upgrade of klitmus7.
0044
0045 If you find any compatibility issues in klitmus7, please inform the
0046 memory model maintainers.
0047
0048 klitmus7 Compatibility Table
0049 ----------------------------
0050
0051 ============ ==========
0052 target Linux herdtools7
0053 ------------ ----------
0054 -- 4.14 7.48 --
0055 4.15 -- 4.19 7.49 --
0056 4.20 -- 5.5 7.54 --
0057 5.6 -- 5.16 7.56 --
0058 5.17 -- 7.56.1 --
0059 ============ ==========
0060
0061
0062 ==================
0063 BASIC USAGE: HERD7
0064 ==================
0065
0066 The memory model is used, in conjunction with "herd7", to exhaustively
0067 explore the state space of small litmus tests. Documentation describing
0068 the format, features, capabilities and limitations of these litmus
0069 tests is available in tools/memory-model/Documentation/litmus-tests.txt.
0070
0071 Example litmus tests may be found in the Linux-kernel source tree:
0072
0073 tools/memory-model/litmus-tests/
0074 Documentation/litmus-tests/
0075
0076 Several thousand more example litmus tests are available here:
0077
0078 https://github.com/paulmckrcu/litmus
0079 https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd
0080 https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus
0081
0082 Documentation describing litmus tests and now to use them may be found
0083 here:
0084
0085 tools/memory-model/Documentation/litmus-tests.txt
0086
0087 The remainder of this section uses the SB+fencembonceonces.litmus test
0088 located in the tools/memory-model directory.
0089
0090 To run SB+fencembonceonces.litmus against the memory model:
0091
0092 $ cd $LINUX_SOURCE_TREE/tools/memory-model
0093 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
0094
0095 Here is the corresponding output:
0096
0097 Test SB+fencembonceonces Allowed
0098 States 3
0099 0:r0=0; 1:r0=1;
0100 0:r0=1; 1:r0=0;
0101 0:r0=1; 1:r0=1;
0102 No
0103 Witnesses
0104 Positive: 0 Negative: 3
0105 Condition exists (0:r0=0 /\ 1:r0=0)
0106 Observation SB+fencembonceonces Never 0 3
0107 Time SB+fencembonceonces 0.01
0108 Hash=d66d99523e2cac6b06e66f4c995ebb48
0109
0110 The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
0111 this litmus test's "exists" clause can not be satisfied.
0112
0113 See "herd7 -help" or "herdtools7/doc/" for more information on running the
0114 tool itself, but please be aware that this documentation is intended for
0115 people who work on the memory model itself, that is, people making changes
0116 to the tools/memory-model/linux-kernel.* files. It is not intended for
0117 people focusing on writing, understanding, and running LKMM litmus tests.
0118
0119
0120 =====================
0121 BASIC USAGE: KLITMUS7
0122 =====================
0123
0124 The "klitmus7" tool converts a litmus test into a Linux kernel module,
0125 which may then be loaded and run.
0126
0127 For example, to run SB+fencembonceonces.litmus against hardware:
0128
0129 $ mkdir mymodules
0130 $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
0131 $ cd mymodules ; make
0132 $ sudo sh run.sh
0133
0134 The corresponding output includes:
0135
0136 Test SB+fencembonceonces Allowed
0137 Histogram (3 states)
0138 644580 :>0:r0=1; 1:r0=0;
0139 644328 :>0:r0=0; 1:r0=1;
0140 711092 :>0:r0=1; 1:r0=1;
0141 No
0142 Witnesses
0143 Positive: 0, Negative: 2000000
0144 Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
0145 Hash=d66d99523e2cac6b06e66f4c995ebb48
0146 Observation SB+fencembonceonces Never 0 2000000
0147 Time SB+fencembonceonces 0.16
0148
0149 The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
0150 that during two million trials, the state specified in this litmus
0151 test's "exists" clause was not reached.
0152
0153 And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
0154 for more information. And again, please be aware that this documentation
0155 is intended for people who work on the memory model itself, that is,
0156 people making changes to the tools/memory-model/linux-kernel.* files.
0157 It is not intended for people focusing on writing, understanding, and
0158 running LKMM litmus tests.
0159
0160
0161 ====================
0162 DESCRIPTION OF FILES
0163 ====================
0164
0165 Documentation/README
0166 Guide to the other documents in the Documentation/ directory.
0167
0168 linux-kernel.bell
0169 Categorizes the relevant instructions, including memory
0170 references, memory barriers, atomic read-modify-write operations,
0171 lock acquisition/release, and RCU operations.
0172
0173 More formally, this file (1) lists the subtypes of the various
0174 event types used by the memory model and (2) performs RCU
0175 read-side critical section nesting analysis.
0176
0177 linux-kernel.cat
0178 Specifies what reorderings are forbidden by memory references,
0179 memory barriers, atomic read-modify-write operations, and RCU.
0180
0181 More formally, this file specifies what executions are forbidden
0182 by the memory model. Allowed executions are those which
0183 satisfy the model's "coherence", "atomic", "happens-before",
0184 "propagation", and "rcu" axioms, which are defined in the file.
0185
0186 linux-kernel.cfg
0187 Convenience file that gathers the common-case herd7 command-line
0188 arguments.
0189
0190 linux-kernel.def
0191 Maps from C-like syntax to herd7's internal litmus-test
0192 instruction-set architecture.
0193
0194 litmus-tests
0195 Directory containing a few representative litmus tests, which
0196 are listed in litmus-tests/README. A great deal more litmus
0197 tests are available at https://github.com/paulmckrcu/litmus.
0198
0199 By "representative", it means the one in the litmus-tests
0200 directory is:
0201
0202 1) simple, the number of threads should be relatively
0203 small and each thread function should be relatively
0204 simple.
0205 2) orthogonal, there should be no two litmus tests
0206 describing the same aspect of the memory model.
0207 3) textbook, developers can easily copy-paste-modify
0208 the litmus tests to use the patterns on their own
0209 code.
0210
0211 lock.cat
0212 Provides a front-end analysis of lock acquisition and release,
0213 for example, associating a lock acquisition with the preceding
0214 and following releases and checking for self-deadlock.
0215
0216 More formally, this file defines a performance-enhanced scheme
0217 for generation of the possible reads-from and coherence order
0218 relations on the locking primitives.
0219
0220 README
0221 This file.
0222
0223 scripts Various scripts, see scripts/README.
