1 ============================== 1 =====================================
2 LINUX KERNEL MEMORY CONSISTENC 2 LINUX KERNEL MEMORY CONSISTENCY MODEL
3 ============================== 3 =====================================
4 4
5 ============ 5 ============
6 INTRODUCTION 6 INTRODUCTION
7 ============ 7 ============
8 8
9 This directory contains the memory consistency 9 This directory contains the memory consistency model (memory model, for
10 short) of the Linux kernel, written in the "ca 10 short) of the Linux kernel, written in the "cat" language and executable
11 by the externally provided "herd7" simulator, 11 by the externally provided "herd7" simulator, which exhaustively explores
12 the state space of small litmus tests. 12 the state space of small litmus tests.
13 13
14 In addition, the "klitmus7" tool (also externa 14 In addition, the "klitmus7" tool (also externally provided) may be used
15 to convert a litmus test to a Linux kernel mod 15 to convert a litmus test to a Linux kernel module, which in turn allows
16 that litmus test to be exercised within the Li 16 that litmus test to be exercised within the Linux kernel.
17 17
18 18
19 ============ 19 ============
20 REQUIREMENTS 20 REQUIREMENTS
21 ============ 21 ============
22 22
23 Version 7.52 or higher of the "herd7" and "kli 23 Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
24 downloaded separately: 24 downloaded separately:
25 25
26 https://github.com/herd/herdtools7 26 https://github.com/herd/herdtools7
27 27
28 See "herdtools7/INSTALL.md" for installation i 28 See "herdtools7/INSTALL.md" for installation instructions.
29 29
30 Note that although these tools usually provide 30 Note that although these tools usually provide backwards compatibility,
31 this is not absolutely guaranteed. 31 this is not absolutely guaranteed.
32 32
33 For example, a future version of herd7 might n 33 For example, a future version of herd7 might not work with the model
34 in this release. A compatible model will like 34 in this release. A compatible model will likely be made available in
35 a later release of Linux kernel. 35 a later release of Linux kernel.
36 36
37 If you absolutely need to run the model in thi 37 If you absolutely need to run the model in this particular release,
38 please try using the exact version called out 38 please try using the exact version called out above.
39 39
40 klitmus7 is independent of the model provided 40 klitmus7 is independent of the model provided here. It has its own
41 dependency on a target kernel release where co 41 dependency on a target kernel release where converted code is built
42 and executed. Any change in kernel APIs essen 42 and executed. Any change in kernel APIs essential to klitmus7 will
43 necessitate an upgrade of klitmus7. 43 necessitate an upgrade of klitmus7.
44 44
45 If you find any compatibility issues in klitmu 45 If you find any compatibility issues in klitmus7, please inform the
46 memory model maintainers. 46 memory model maintainers.
47 47
48 klitmus7 Compatibility Table 48 klitmus7 Compatibility Table
49 ---------------------------- 49 ----------------------------
50 50
51 ============ ========== 51 ============ ==========
52 target Linux herdtools7 52 target Linux herdtools7
53 ------------ ---------- 53 ------------ ----------
54 -- 4.14 7.48 -- !! 54 -- 4.18 7.48 --
55 4.15 -- 4.19 7.49 -- 55 4.15 -- 4.19 7.49 --
56 4.20 -- 5.5 7.54 -- 56 4.20 -- 5.5 7.54 --
57 5.6 -- 5.16 7.56 -- !! 57 5.6 -- 7.56 --
58 5.17 -- 7.56.1 -- <<
59 ============ ========== 58 ============ ==========
60 59
61 60
62 ================== 61 ==================
63 BASIC USAGE: HERD7 62 BASIC USAGE: HERD7
64 ================== 63 ==================
65 64
66 The memory model is used, in conjunction with 65 The memory model is used, in conjunction with "herd7", to exhaustively
67 explore the state space of small litmus tests. 66 explore the state space of small litmus tests. Documentation describing
68 the format, features, capabilities and limitat 67 the format, features, capabilities and limitations of these litmus
69 tests is available in tools/memory-model/Docum 68 tests is available in tools/memory-model/Documentation/litmus-tests.txt.
70 69
71 Example litmus tests may be found in the Linux 70 Example litmus tests may be found in the Linux-kernel source tree:
72 71
73 tools/memory-model/litmus-tests/ 72 tools/memory-model/litmus-tests/
74 Documentation/litmus-tests/ 73 Documentation/litmus-tests/
75 74
76 Several thousand more example litmus tests are 75 Several thousand more example litmus tests are available here:
77 76
78 https://github.com/paulmckrcu/litmus 77 https://github.com/paulmckrcu/litmus
79 https://git.kernel.org/pub/scm/linux/k 78 https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd
80 https://git.kernel.org/pub/scm/linux/k 79 https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus
81 80
82 Documentation describing litmus tests and now 81 Documentation describing litmus tests and now to use them may be found
83 here: 82 here:
84 83
85 tools/memory-model/Documentation/litmu 84 tools/memory-model/Documentation/litmus-tests.txt
86 85
87 The remainder of this section uses the SB+fenc 86 The remainder of this section uses the SB+fencembonceonces.litmus test
88 located in the tools/memory-model directory. 87 located in the tools/memory-model directory.
89 88
90 To run SB+fencembonceonces.litmus against the 89 To run SB+fencembonceonces.litmus against the memory model:
91 90
92 $ cd $LINUX_SOURCE_TREE/tools/memory-model 91 $ cd $LINUX_SOURCE_TREE/tools/memory-model
93 $ herd7 -conf linux-kernel.cfg litmus-tests/ 92 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
94 93
95 Here is the corresponding output: 94 Here is the corresponding output:
96 95
97 Test SB+fencembonceonces Allowed 96 Test SB+fencembonceonces Allowed
98 States 3 97 States 3
99 0:r0=0; 1:r0=1; 98 0:r0=0; 1:r0=1;
100 0:r0=1; 1:r0=0; 99 0:r0=1; 1:r0=0;
101 0:r0=1; 1:r0=1; 100 0:r0=1; 1:r0=1;
102 No 101 No
103 Witnesses 102 Witnesses
104 Positive: 0 Negative: 3 103 Positive: 0 Negative: 3
105 Condition exists (0:r0=0 /\ 1:r0=0) 104 Condition exists (0:r0=0 /\ 1:r0=0)
106 Observation SB+fencembonceonces Never 0 3 105 Observation SB+fencembonceonces Never 0 3
107 Time SB+fencembonceonces 0.01 106 Time SB+fencembonceonces 0.01
108 Hash=d66d99523e2cac6b06e66f4c995ebb48 107 Hash=d66d99523e2cac6b06e66f4c995ebb48
109 108
110 The "Positive: 0 Negative: 3" and the "Never 0 109 The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
111 this litmus test's "exists" clause can not be 110 this litmus test's "exists" clause can not be satisfied.
112 111
113 See "herd7 -help" or "herdtools7/doc/" for mor 112 See "herd7 -help" or "herdtools7/doc/" for more information on running the
114 tool itself, but please be aware that this doc 113 tool itself, but please be aware that this documentation is intended for
115 people who work on the memory model itself, th 114 people who work on the memory model itself, that is, people making changes
116 to the tools/memory-model/linux-kernel.* files 115 to the tools/memory-model/linux-kernel.* files. It is not intended for
117 people focusing on writing, understanding, and 116 people focusing on writing, understanding, and running LKMM litmus tests.
118 117
119 118
120 ===================== 119 =====================
121 BASIC USAGE: KLITMUS7 120 BASIC USAGE: KLITMUS7
122 ===================== 121 =====================
123 122
124 The "klitmus7" tool converts a litmus test int 123 The "klitmus7" tool converts a litmus test into a Linux kernel module,
125 which may then be loaded and run. 124 which may then be loaded and run.
126 125
127 For example, to run SB+fencembonceonces.litmus 126 For example, to run SB+fencembonceonces.litmus against hardware:
128 127
129 $ mkdir mymodules 128 $ mkdir mymodules
130 $ klitmus7 -o mymodules litmus-tests/SB+fenc 129 $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
131 $ cd mymodules ; make 130 $ cd mymodules ; make
132 $ sudo sh run.sh 131 $ sudo sh run.sh
133 132
134 The corresponding output includes: 133 The corresponding output includes:
135 134
136 Test SB+fencembonceonces Allowed 135 Test SB+fencembonceonces Allowed
137 Histogram (3 states) 136 Histogram (3 states)
138 644580 :>0:r0=1; 1:r0=0; 137 644580 :>0:r0=1; 1:r0=0;
139 644328 :>0:r0=0; 1:r0=1; 138 644328 :>0:r0=0; 1:r0=1;
140 711092 :>0:r0=1; 1:r0=1; 139 711092 :>0:r0=1; 1:r0=1;
141 No 140 No
142 Witnesses 141 Witnesses
143 Positive: 0, Negative: 2000000 142 Positive: 0, Negative: 2000000
144 Condition exists (0:r0=0 /\ 1:r0=0) is NOT v 143 Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
145 Hash=d66d99523e2cac6b06e66f4c995ebb48 144 Hash=d66d99523e2cac6b06e66f4c995ebb48
146 Observation SB+fencembonceonces Never 0 2000 145 Observation SB+fencembonceonces Never 0 2000000
147 Time SB+fencembonceonces 0.16 146 Time SB+fencembonceonces 0.16
148 147
149 The "Positive: 0 Negative: 2000000" and the "N 148 The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
150 that during two million trials, the state spec 149 that during two million trials, the state specified in this litmus
151 test's "exists" clause was not reached. 150 test's "exists" clause was not reached.
152 151
153 And, as with "herd7", please see "klitmus7 -he 152 And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
154 for more information. And again, please be aw 153 for more information. And again, please be aware that this documentation
155 is intended for people who work on the memory 154 is intended for people who work on the memory model itself, that is,
156 people making changes to the tools/memory-mode 155 people making changes to the tools/memory-model/linux-kernel.* files.
157 It is not intended for people focusing on writ 156 It is not intended for people focusing on writing, understanding, and
158 running LKMM litmus tests. 157 running LKMM litmus tests.
159 158
160 159
161 ==================== 160 ====================
162 DESCRIPTION OF FILES 161 DESCRIPTION OF FILES
163 ==================== 162 ====================
164 163
165 Documentation/README !! 164 Documentation/cheatsheet.txt
166 Guide to the other documents in the Do !! 165 Quick-reference guide to the Linux-kernel memory model.
>> 166
>> 167 Documentation/explanation.txt
>> 168 Describes the memory model in detail.
>> 169
>> 170 Documentation/litmus-tests.txt
>> 171 Describes the format, features, capabilities, and limitations
>> 172 of the litmus tests that LKMM can evaluate.
>> 173
>> 174 Documentation/recipes.txt
>> 175 Lists common memory-ordering patterns.
>> 176
>> 177 Documentation/references.txt
>> 178 Provides background reading.
>> 179
>> 180 Documentation/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!
167 184
168 linux-kernel.bell 185 linux-kernel.bell
169 Categorizes the relevant instructions, 186 Categorizes the relevant instructions, including memory
170 references, memory barriers, atomic re 187 references, memory barriers, atomic read-modify-write operations,
171 lock acquisition/release, and RCU oper 188 lock acquisition/release, and RCU operations.
172 189
173 More formally, this file (1) lists the 190 More formally, this file (1) lists the subtypes of the various
174 event types used by the memory model a 191 event types used by the memory model and (2) performs RCU
175 read-side critical section nesting ana 192 read-side critical section nesting analysis.
176 193
177 linux-kernel.cat 194 linux-kernel.cat
178 Specifies what reorderings are forbidd 195 Specifies what reorderings are forbidden by memory references,
179 memory barriers, atomic read-modify-wr 196 memory barriers, atomic read-modify-write operations, and RCU.
180 197
181 More formally, this file specifies wha 198 More formally, this file specifies what executions are forbidden
182 by the memory model. Allowed executio 199 by the memory model. Allowed executions are those which
183 satisfy the model's "coherence", "atom 200 satisfy the model's "coherence", "atomic", "happens-before",
184 "propagation", and "rcu" axioms, which 201 "propagation", and "rcu" axioms, which are defined in the file.
185 202
186 linux-kernel.cfg 203 linux-kernel.cfg
187 Convenience file that gathers the comm 204 Convenience file that gathers the common-case herd7 command-line
188 arguments. 205 arguments.
189 206
190 linux-kernel.def 207 linux-kernel.def
191 Maps from C-like syntax to herd7's int 208 Maps from C-like syntax to herd7's internal litmus-test
192 instruction-set architecture. 209 instruction-set architecture.
193 210
194 litmus-tests 211 litmus-tests
195 Directory containing a few representat 212 Directory containing a few representative litmus tests, which
196 are listed in litmus-tests/README. A 213 are listed in litmus-tests/README. A great deal more litmus
197 tests are available at https://github. 214 tests are available at https://github.com/paulmckrcu/litmus.
198 <<
199 By "representative", it means the one <<
200 directory is: <<
201 <<
202 1) simple, the number of threa <<
203 small and each thread funct <<
204 simple. <<
205 2) orthogonal, there should be <<
206 describing the same aspect <<
207 3) textbook, developers can ea <<
208 the litmus tests to use the <<
209 code. <<
210 215
211 lock.cat 216 lock.cat
212 Provides a front-end analysis of lock 217 Provides a front-end analysis of lock acquisition and release,
213 for example, associating a lock acquis 218 for example, associating a lock acquisition with the preceding
214 and following releases and checking fo 219 and following releases and checking for self-deadlock.
215 220
216 More formally, this file defines a per 221 More formally, this file defines a performance-enhanced scheme
217 for generation of the possible reads-f 222 for generation of the possible reads-from and coherence order
218 relations on the locking primitives. 223 relations on the locking primitives.
219 224
220 README 225 README
221 This file. 226 This file.
222 227
223 scripts Various scripts, see scripts/README. 228 scripts Various scripts, see scripts/README.
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.