Loading...
Note: File does not exist in v3.5.6.
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.
67
68For example, to run SB+fencembonceonces.litmus against the memory model:
69
70 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
71
72Here is the corresponding output:
73
74 Test SB+fencembonceonces Allowed
75 States 3
76 0:r0=0; 1:r0=1;
77 0:r0=1; 1:r0=0;
78 0:r0=1; 1:r0=1;
79 No
80 Witnesses
81 Positive: 0 Negative: 3
82 Condition exists (0:r0=0 /\ 1:r0=0)
83 Observation SB+fencembonceonces Never 0 3
84 Time SB+fencembonceonces 0.01
85 Hash=d66d99523e2cac6b06e66f4c995ebb48
86
87The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
88this litmus test's "exists" clause can not be satisfied.
89
90See "herd7 -help" or "herdtools7/doc/" for more information.
91
92
93=====================
94BASIC USAGE: KLITMUS7
95=====================
96
97The "klitmus7" tool converts a litmus test into a Linux kernel module,
98which may then be loaded and run.
99
100For example, to run SB+fencembonceonces.litmus against hardware:
101
102 $ mkdir mymodules
103 $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
104 $ cd mymodules ; make
105 $ sudo sh run.sh
106
107The corresponding output includes:
108
109 Test SB+fencembonceonces Allowed
110 Histogram (3 states)
111 644580 :>0:r0=1; 1:r0=0;
112 644328 :>0:r0=0; 1:r0=1;
113 711092 :>0:r0=1; 1:r0=1;
114 No
115 Witnesses
116 Positive: 0, Negative: 2000000
117 Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
118 Hash=d66d99523e2cac6b06e66f4c995ebb48
119 Observation SB+fencembonceonces Never 0 2000000
120 Time SB+fencembonceonces 0.16
121
122The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
123that during two million trials, the state specified in this litmus
124test's "exists" clause was not reached.
125
126And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
127for more information.
128
129
130====================
131DESCRIPTION OF FILES
132====================
133
134Documentation/cheatsheet.txt
135 Quick-reference guide to the Linux-kernel memory model.
136
137Documentation/explanation.txt
138 Describes the memory model in detail.
139
140Documentation/recipes.txt
141 Lists common memory-ordering patterns.
142
143Documentation/references.txt
144 Provides background reading.
145
146linux-kernel.bell
147 Categorizes the relevant instructions, including memory
148 references, memory barriers, atomic read-modify-write operations,
149 lock acquisition/release, and RCU operations.
150
151 More formally, this file (1) lists the subtypes of the various
152 event types used by the memory model and (2) performs RCU
153 read-side critical section nesting analysis.
154
155linux-kernel.cat
156 Specifies what reorderings are forbidden by memory references,
157 memory barriers, atomic read-modify-write operations, and RCU.
158
159 More formally, this file specifies what executions are forbidden
160 by the memory model. Allowed executions are those which
161 satisfy the model's "coherence", "atomic", "happens-before",
162 "propagation", and "rcu" axioms, which are defined in the file.
163
164linux-kernel.cfg
165 Convenience file that gathers the common-case herd7 command-line
166 arguments.
167
168linux-kernel.def
169 Maps from C-like syntax to herd7's internal litmus-test
170 instruction-set architecture.
171
172litmus-tests
173 Directory containing a few representative litmus tests, which
174 are listed in litmus-tests/README. A great deal more litmus
175 tests are available at https://github.com/paulmckrcu/litmus.
176
177lock.cat
178 Provides a front-end analysis of lock acquisition and release,
179 for example, associating a lock acquisition with the preceding
180 and following releases and checking for self-deadlock.
181
182 More formally, this file defines a performance-enhanced scheme
183 for generation of the possible reads-from and coherence order
184 relations on the locking primitives.
185
186README
187 This file.
188
189scripts Various scripts, see scripts/README.
190
191
192===========
193LIMITATIONS
194===========
195
196The Linux-kernel memory model (LKMM) has the following limitations:
197
1981. 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
2122. Multiple access sizes for a single variable are not supported,
213 and neither are misaligned or partially overlapping accesses.
214
2153. 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
2194. I/O such as MMIO or DMA is not supported.
220
2215. 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
2256. 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
286The "herd7" tool has some additional limitations of its own, apart from
287the memory model:
288
2891. 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
2932. Dynamic memory allocation is not supported, although this can
294 be worked around in some cases by supplying multiple statically
295 allocated variables.
296
297Some of these limitations may be overcome in the future, but others are
298more likely to be addressed by incorporating the Linux-kernel memory model
299into other tools.
300
301Finally, please note that LKMM is subject to change as hardware, use cases,
302and compilers evolve.