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.
68 the format, features, capabilities and limitat <<
69 tests is available in tools/memory-model/Docum <<
70 67
71 Example litmus tests may be found in the Linux !! 68 For example, to run SB+fencembonceonces.litmus against the memory model:
72 69
73 tools/memory-model/litmus-tests/ <<
74 Documentation/litmus-tests/ <<
75 <<
76 Several thousand more example litmus tests are <<
77 <<
78 https://github.com/paulmckrcu/litmus <<
79 https://git.kernel.org/pub/scm/linux/k <<
80 https://git.kernel.org/pub/scm/linux/k <<
81 <<
82 Documentation describing litmus tests and now <<
83 here: <<
84 <<
85 tools/memory-model/Documentation/litmu <<
86 <<
87 The remainder of this section uses the SB+fenc <<
88 located in the tools/memory-model directory. <<
89 <<
90 To run SB+fencembonceonces.litmus against the <<
91 <<
92 $ cd $LINUX_SOURCE_TREE/tools/memory-model <<
93 $ herd7 -conf linux-kernel.cfg litmus-tests/ 70 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
94 71
95 Here is the corresponding output: 72 Here is the corresponding output:
96 73
97 Test SB+fencembonceonces Allowed 74 Test SB+fencembonceonces Allowed
98 States 3 75 States 3
99 0:r0=0; 1:r0=1; 76 0:r0=0; 1:r0=1;
100 0:r0=1; 1:r0=0; 77 0:r0=1; 1:r0=0;
101 0:r0=1; 1:r0=1; 78 0:r0=1; 1:r0=1;
102 No 79 No
103 Witnesses 80 Witnesses
104 Positive: 0 Negative: 3 81 Positive: 0 Negative: 3
105 Condition exists (0:r0=0 /\ 1:r0=0) 82 Condition exists (0:r0=0 /\ 1:r0=0)
106 Observation SB+fencembonceonces Never 0 3 83 Observation SB+fencembonceonces Never 0 3
107 Time SB+fencembonceonces 0.01 84 Time SB+fencembonceonces 0.01
108 Hash=d66d99523e2cac6b06e66f4c995ebb48 85 Hash=d66d99523e2cac6b06e66f4c995ebb48
109 86
110 The "Positive: 0 Negative: 3" and the "Never 0 87 The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
111 this litmus test's "exists" clause can not be 88 this litmus test's "exists" clause can not be satisfied.
112 89
113 See "herd7 -help" or "herdtools7/doc/" for mor !! 90 See "herd7 -help" or "herdtools7/doc/" for more information.
114 tool itself, but please be aware that this doc <<
115 people who work on the memory model itself, th <<
116 to the tools/memory-model/linux-kernel.* files <<
117 people focusing on writing, understanding, and <<
118 91
119 92
120 ===================== 93 =====================
121 BASIC USAGE: KLITMUS7 94 BASIC USAGE: KLITMUS7
122 ===================== 95 =====================
123 96
124 The "klitmus7" tool converts a litmus test int 97 The "klitmus7" tool converts a litmus test into a Linux kernel module,
125 which may then be loaded and run. 98 which may then be loaded and run.
126 99
127 For example, to run SB+fencembonceonces.litmus 100 For example, to run SB+fencembonceonces.litmus against hardware:
128 101
129 $ mkdir mymodules 102 $ mkdir mymodules
130 $ klitmus7 -o mymodules litmus-tests/SB+fenc 103 $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
131 $ cd mymodules ; make 104 $ cd mymodules ; make
132 $ sudo sh run.sh 105 $ sudo sh run.sh
133 106
134 The corresponding output includes: 107 The corresponding output includes:
135 108
136 Test SB+fencembonceonces Allowed 109 Test SB+fencembonceonces Allowed
137 Histogram (3 states) 110 Histogram (3 states)
138 644580 :>0:r0=1; 1:r0=0; 111 644580 :>0:r0=1; 1:r0=0;
139 644328 :>0:r0=0; 1:r0=1; 112 644328 :>0:r0=0; 1:r0=1;
140 711092 :>0:r0=1; 1:r0=1; 113 711092 :>0:r0=1; 1:r0=1;
141 No 114 No
142 Witnesses 115 Witnesses
143 Positive: 0, Negative: 2000000 116 Positive: 0, Negative: 2000000
144 Condition exists (0:r0=0 /\ 1:r0=0) is NOT v 117 Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
145 Hash=d66d99523e2cac6b06e66f4c995ebb48 118 Hash=d66d99523e2cac6b06e66f4c995ebb48
146 Observation SB+fencembonceonces Never 0 2000 119 Observation SB+fencembonceonces Never 0 2000000
147 Time SB+fencembonceonces 0.16 120 Time SB+fencembonceonces 0.16
148 121
149 The "Positive: 0 Negative: 2000000" and the "N 122 The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
150 that during two million trials, the state spec 123 that during two million trials, the state specified in this litmus
151 test's "exists" clause was not reached. 124 test's "exists" clause was not reached.
152 125
153 And, as with "herd7", please see "klitmus7 -he 126 And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
154 for more information. And again, please be aw !! 127 for more information.
155 is intended for people who work on the memory <<
156 people making changes to the tools/memory-mode <<
157 It is not intended for people focusing on writ <<
158 running LKMM litmus tests. <<
159 128
160 129
161 ==================== 130 ====================
162 DESCRIPTION OF FILES 131 DESCRIPTION OF FILES
163 ==================== 132 ====================
164 133
165 Documentation/README !! 134 Documentation/cheatsheet.txt
166 Guide to the other documents in the Do !! 135 Quick-reference guide to the Linux-kernel memory model.
>> 136
>> 137 Documentation/explanation.txt
>> 138 Describes the memory model in detail.
>> 139
>> 140 Documentation/recipes.txt
>> 141 Lists common memory-ordering patterns.
>> 142
>> 143 Documentation/references.txt
>> 144 Provides background reading.
167 145
168 linux-kernel.bell 146 linux-kernel.bell
169 Categorizes the relevant instructions, 147 Categorizes the relevant instructions, including memory
170 references, memory barriers, atomic re 148 references, memory barriers, atomic read-modify-write operations,
171 lock acquisition/release, and RCU oper 149 lock acquisition/release, and RCU operations.
172 150
173 More formally, this file (1) lists the 151 More formally, this file (1) lists the subtypes of the various
174 event types used by the memory model a 152 event types used by the memory model and (2) performs RCU
175 read-side critical section nesting ana 153 read-side critical section nesting analysis.
176 154
177 linux-kernel.cat 155 linux-kernel.cat
178 Specifies what reorderings are forbidd 156 Specifies what reorderings are forbidden by memory references,
179 memory barriers, atomic read-modify-wr 157 memory barriers, atomic read-modify-write operations, and RCU.
180 158
181 More formally, this file specifies wha 159 More formally, this file specifies what executions are forbidden
182 by the memory model. Allowed executio 160 by the memory model. Allowed executions are those which
183 satisfy the model's "coherence", "atom 161 satisfy the model's "coherence", "atomic", "happens-before",
184 "propagation", and "rcu" axioms, which 162 "propagation", and "rcu" axioms, which are defined in the file.
185 163
186 linux-kernel.cfg 164 linux-kernel.cfg
187 Convenience file that gathers the comm 165 Convenience file that gathers the common-case herd7 command-line
188 arguments. 166 arguments.
189 167
190 linux-kernel.def 168 linux-kernel.def
191 Maps from C-like syntax to herd7's int 169 Maps from C-like syntax to herd7's internal litmus-test
192 instruction-set architecture. 170 instruction-set architecture.
193 171
194 litmus-tests 172 litmus-tests
195 Directory containing a few representat 173 Directory containing a few representative litmus tests, which
196 are listed in litmus-tests/README. A 174 are listed in litmus-tests/README. A great deal more litmus
197 tests are available at https://github. 175 tests are available at https://github.com/paulmckrcu/litmus.
198 176
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 <<
211 lock.cat 177 lock.cat
212 Provides a front-end analysis of lock 178 Provides a front-end analysis of lock acquisition and release,
213 for example, associating a lock acquis 179 for example, associating a lock acquisition with the preceding
214 and following releases and checking fo 180 and following releases and checking for self-deadlock.
215 181
216 More formally, this file defines a per 182 More formally, this file defines a performance-enhanced scheme
217 for generation of the possible reads-f 183 for generation of the possible reads-from and coherence order
218 relations on the locking primitives. 184 relations on the locking primitives.
219 185
220 README 186 README
221 This file. 187 This file.
222 188
223 scripts Various scripts, see scripts/README. 189 scripts Various scripts, see scripts/README.
>> 190
>> 191
>> 192 ===========
>> 193 LIMITATIONS
>> 194 ===========
>> 195
>> 196 The Linux-kernel memory model (LKMM) has the following limitations:
>> 197
>> 198 1. Compiler optimizations are not accurately modeled. Of course,
>> 199 the use of READ_ONCE() and WRITE_ONCE() limits the compiler's
>> 200 ability to optimize, but under some circumstances it is possible
>> 201 for the compiler to undermine the memory model. For more
>> 202 information, see Documentation/explanation.txt (in particular,
>> 203 the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING"
>> 204 sections).
>> 205
>> 206 Note that this limitation in turn limits LKMM's ability to
>> 207 accurately model address, control, and data dependencies.
>> 208 For example, if the compiler can deduce the value of some variable
>> 209 carrying a dependency, then the compiler can break that dependency
>> 210 by substituting a constant of that value.
>> 211
>> 212 2. Multiple access sizes for a single variable are not supported,
>> 213 and neither are misaligned or partially overlapping accesses.
>> 214
>> 215 3. Exceptions and interrupts are not modeled. In some cases,
>> 216 this limitation can be overcome by modeling the interrupt or
>> 217 exception with an additional process.
>> 218
>> 219 4. I/O such as MMIO or DMA is not supported.
>> 220
>> 221 5. Self-modifying code (such as that found in the kernel's
>> 222 alternatives mechanism, function tracer, Berkeley Packet Filter
>> 223 JIT compiler, and module loader) is not supported.
>> 224
>> 225 6. Complete modeling of all variants of atomic read-modify-write
>> 226 operations, locking primitives, and RCU is not provided.
>> 227 For example, call_rcu() and rcu_barrier() are not supported.
>> 228 However, a substantial amount of support is provided for these
>> 229 operations, as shown in the linux-kernel.def file.
>> 230
>> 231 a. When rcu_assign_pointer() is passed NULL, the Linux
>> 232 kernel provides no ordering, but LKMM models this
>> 233 case as a store release.
>> 234
>> 235 b. The "unless" RMW operations are not currently modeled:
>> 236 atomic_long_add_unless(), atomic_inc_unless_negative(),
>> 237 and atomic_dec_unless_positive(). These can be emulated
>> 238 in litmus tests, for example, by using atomic_cmpxchg().
>> 239
>> 240 One exception of this limitation is atomic_add_unless(),
>> 241 which is provided directly by herd7 (so no corresponding
>> 242 definition in linux-kernel.def). atomic_add_unless() is
>> 243 modeled by herd7 therefore it can be used in litmus tests.
>> 244
>> 245 c. The call_rcu() function is not modeled. It can be
>> 246 emulated in litmus tests by adding another process that
>> 247 invokes synchronize_rcu() and the body of the callback
>> 248 function, with (for example) a release-acquire from
>> 249 the site of the emulated call_rcu() to the beginning
>> 250 of the additional process.
>> 251
>> 252 d. The rcu_barrier() function is not modeled. It can be
>> 253 emulated in litmus tests emulating call_rcu() via
>> 254 (for example) a release-acquire from the end of each
>> 255 additional call_rcu() process to the site of the
>> 256 emulated rcu-barrier().
>> 257
>> 258 e. Although sleepable RCU (SRCU) is now modeled, there
>> 259 are some subtle differences between its semantics and
>> 260 those in the Linux kernel. For example, the kernel
>> 261 might interpret the following sequence as two partially
>> 262 overlapping SRCU read-side critical sections:
>> 263
>> 264 1 r1 = srcu_read_lock(&my_srcu);
>> 265 2 do_something_1();
>> 266 3 r2 = srcu_read_lock(&my_srcu);
>> 267 4 do_something_2();
>> 268 5 srcu_read_unlock(&my_srcu, r1);
>> 269 6 do_something_3();
>> 270 7 srcu_read_unlock(&my_srcu, r2);
>> 271
>> 272 In contrast, LKMM will interpret this as a nested pair of
>> 273 SRCU read-side critical sections, with the outer critical
>> 274 section spanning lines 1-7 and the inner critical section
>> 275 spanning lines 3-5.
>> 276
>> 277 This difference would be more of a concern had anyone
>> 278 identified a reasonable use case for partially overlapping
>> 279 SRCU read-side critical sections. For more information,
>> 280 please see: https://paulmck.livejournal.com/40593.html
>> 281
>> 282 f. Reader-writer locking is not modeled. It can be
>> 283 emulated in litmus tests using atomic read-modify-write
>> 284 operations.
>> 285
>> 286 The "herd7" tool has some additional limitations of its own, apart from
>> 287 the memory model:
>> 288
>> 289 1. Non-trivial data structures such as arrays or structures are
>> 290 not supported. However, pointers are supported, allowing trivial
>> 291 linked lists to be constructed.
>> 292
>> 293 2. Dynamic memory allocation is not supported, although this can
>> 294 be worked around in some cases by supplying multiple statically
>> 295 allocated variables.
>> 296
>> 297 Some of these limitations may be overcome in the future, but others are
>> 298 more likely to be addressed by incorporating the Linux-kernel memory model
>> 299 into other tools.
>> 300
>> 301 Finally, please note that LKMM is subject to change as hardware, use cases,
>> 302 and compilers evolve.
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.