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.18 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/cheatsheet.txt
165 Quick-reference guide to the Linux-kernel memory model.
166
167Documentation/explanation.txt
168 Describes the memory model in detail.
169
170Documentation/litmus-tests.txt
171 Describes the format, features, capabilities, and limitations
172 of the litmus tests that LKMM can evaluate.
173
174Documentation/recipes.txt
175 Lists common memory-ordering patterns.
176
177Documentation/references.txt
178 Provides background reading.
179
180Documentation/simple.txt
181 Starting point for someone new to Linux-kernel concurrency.
182 And also for those needing a reminder of the simpler approaches
183 to concurrency!
184
185linux-kernel.bell
186 Categorizes the relevant instructions, including memory
187 references, memory barriers, atomic read-modify-write operations,
188 lock acquisition/release, and RCU operations.
189
190 More formally, this file (1) lists the subtypes of the various
191 event types used by the memory model and (2) performs RCU
192 read-side critical section nesting analysis.
193
194linux-kernel.cat
195 Specifies what reorderings are forbidden by memory references,
196 memory barriers, atomic read-modify-write operations, and RCU.
197
198 More formally, this file specifies what executions are forbidden
199 by the memory model. Allowed executions are those which
200 satisfy the model's "coherence", "atomic", "happens-before",
201 "propagation", and "rcu" axioms, which are defined in the file.
202
203linux-kernel.cfg
204 Convenience file that gathers the common-case herd7 command-line
205 arguments.
206
207linux-kernel.def
208 Maps from C-like syntax to herd7's internal litmus-test
209 instruction-set architecture.
210
211litmus-tests
212 Directory containing a few representative litmus tests, which
213 are listed in litmus-tests/README. A great deal more litmus
214 tests are available at https://github.com/paulmckrcu/litmus.
215
216lock.cat
217 Provides a front-end analysis of lock acquisition and release,
218 for example, associating a lock acquisition with the preceding
219 and following releases and checking for self-deadlock.
220
221 More formally, this file defines a performance-enhanced scheme
222 for generation of the possible reads-from and coherence order
223 relations on the locking primitives.
224
225README
226 This file.
227
228scripts Various scripts, see scripts/README.
229
