Loading...
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.14 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/README
165 Guide to the other documents in the Documentation/ directory.
166
167linux-kernel.bell
168 Categorizes the relevant instructions, including memory
169 references, memory barriers, atomic read-modify-write operations,
170 lock acquisition/release, and RCU operations.
171
172 More formally, this file (1) lists the subtypes of the various
173 event types used by the memory model and (2) performs RCU
174 read-side critical section nesting analysis.
175
176linux-kernel.cat
177 Specifies what reorderings are forbidden by memory references,
178 memory barriers, atomic read-modify-write operations, and RCU.
179
180 More formally, this file specifies what executions are forbidden
181 by the memory model. Allowed executions are those which
182 satisfy the model's "coherence", "atomic", "happens-before",
183 "propagation", and "rcu" axioms, which are defined in the file.
184
185linux-kernel.cfg
186 Convenience file that gathers the common-case herd7 command-line
187 arguments.
188
189linux-kernel.def
190 Maps from C-like syntax to herd7's internal litmus-test
191 instruction-set architecture.
192
193litmus-tests
194 Directory containing a few representative litmus tests, which
195 are listed in litmus-tests/README. A great deal more litmus
196 tests are available at https://github.com/paulmckrcu/litmus.
197
198lock.cat
199 Provides a front-end analysis of lock acquisition and release,
200 for example, associating a lock acquisition with the preceding
201 and following releases and checking for self-deadlock.
202
203 More formally, this file defines a performance-enhanced scheme
204 for generation of the possible reads-from and coherence order
205 relations on the locking primitives.
206
207README
208 This file.
209
210scripts Various scripts, see scripts/README.
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. Therefore, if a later version does
32not work, please try using the exact version called out above.
33
34
35==================
36BASIC USAGE: HERD7
37==================
38
39The memory model is used, in conjunction with "herd7", to exhaustively
40explore the state space of small litmus tests.
41
42For example, to run SB+fencembonceonces.litmus against the memory model:
43
44 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
45
46Here is the corresponding output:
47
48 Test SB+fencembonceonces Allowed
49 States 3
50 0:r0=0; 1:r0=1;
51 0:r0=1; 1:r0=0;
52 0:r0=1; 1:r0=1;
53 No
54 Witnesses
55 Positive: 0 Negative: 3
56 Condition exists (0:r0=0 /\ 1:r0=0)
57 Observation SB+fencembonceonces Never 0 3
58 Time SB+fencembonceonces 0.01
59 Hash=d66d99523e2cac6b06e66f4c995ebb48
60
61The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
62this litmus test's "exists" clause can not be satisfied.
63
64See "herd7 -help" or "herdtools7/doc/" for more information.
65
66
67=====================
68BASIC USAGE: KLITMUS7
69=====================
70
71The "klitmus7" tool converts a litmus test into a Linux kernel module,
72which may then be loaded and run.
73
74For example, to run SB+fencembonceonces.litmus against hardware:
75
76 $ mkdir mymodules
77 $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
78 $ cd mymodules ; make
79 $ sudo sh run.sh
80
81The corresponding output includes:
82
83 Test SB+fencembonceonces Allowed
84 Histogram (3 states)
85 644580 :>0:r0=1; 1:r0=0;
86 644328 :>0:r0=0; 1:r0=1;
87 711092 :>0:r0=1; 1:r0=1;
88 No
89 Witnesses
90 Positive: 0, Negative: 2000000
91 Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
92 Hash=d66d99523e2cac6b06e66f4c995ebb48
93 Observation SB+fencembonceonces Never 0 2000000
94 Time SB+fencembonceonces 0.16
95
96The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
97that during two million trials, the state specified in this litmus
98test's "exists" clause was not reached.
99
100And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
101for more information.
102
103
104====================
105DESCRIPTION OF FILES
106====================
107
108Documentation/cheatsheet.txt
109 Quick-reference guide to the Linux-kernel memory model.
110
111Documentation/explanation.txt
112 Describes the memory model in detail.
113
114Documentation/recipes.txt
115 Lists common memory-ordering patterns.
116
117Documentation/references.txt
118 Provides background reading.
119
120linux-kernel.bell
121 Categorizes the relevant instructions, including memory
122 references, memory barriers, atomic read-modify-write operations,
123 lock acquisition/release, and RCU operations.
124
125 More formally, this file (1) lists the subtypes of the various
126 event types used by the memory model and (2) performs RCU
127 read-side critical section nesting analysis.
128
129linux-kernel.cat
130 Specifies what reorderings are forbidden by memory references,
131 memory barriers, atomic read-modify-write operations, and RCU.
132
133 More formally, this file specifies what executions are forbidden
134 by the memory model. Allowed executions are those which
135 satisfy the model's "coherence", "atomic", "happens-before",
136 "propagation", and "rcu" axioms, which are defined in the file.
137
138linux-kernel.cfg
139 Convenience file that gathers the common-case herd7 command-line
140 arguments.
141
142linux-kernel.def
143 Maps from C-like syntax to herd7's internal litmus-test
144 instruction-set architecture.
145
146litmus-tests
147 Directory containing a few representative litmus tests, which
148 are listed in litmus-tests/README. A great deal more litmus
149 tests are available at https://github.com/paulmckrcu/litmus.
150
151lock.cat
152 Provides a front-end analysis of lock acquisition and release,
153 for example, associating a lock acquisition with the preceding
154 and following releases and checking for self-deadlock.
155
156 More formally, this file defines a performance-enhanced scheme
157 for generation of the possible reads-from and coherence order
158 relations on the locking primitives.
159
160README
161 This file.
162
163scripts Various scripts, see scripts/README.
164
165
166===========
167LIMITATIONS
168===========
169
170The Linux-kernel memory model (LKMM) has the following limitations:
171
1721. Compiler optimizations are not accurately modeled. Of course,
173 the use of READ_ONCE() and WRITE_ONCE() limits the compiler's
174 ability to optimize, but under some circumstances it is possible
175 for the compiler to undermine the memory model. For more
176 information, see Documentation/explanation.txt (in particular,
177 the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING"
178 sections).
179
180 Note that this limitation in turn limits LKMM's ability to
181 accurately model address, control, and data dependencies.
182 For example, if the compiler can deduce the value of some variable
183 carrying a dependency, then the compiler can break that dependency
184 by substituting a constant of that value.
185
1862. Multiple access sizes for a single variable are not supported,
187 and neither are misaligned or partially overlapping accesses.
188
1893. Exceptions and interrupts are not modeled. In some cases,
190 this limitation can be overcome by modeling the interrupt or
191 exception with an additional process.
192
1934. I/O such as MMIO or DMA is not supported.
194
1955. Self-modifying code (such as that found in the kernel's
196 alternatives mechanism, function tracer, Berkeley Packet Filter
197 JIT compiler, and module loader) is not supported.
198
1996. Complete modeling of all variants of atomic read-modify-write
200 operations, locking primitives, and RCU is not provided.
201 For example, call_rcu() and rcu_barrier() are not supported.
202 However, a substantial amount of support is provided for these
203 operations, as shown in the linux-kernel.def file.
204
205 a. When rcu_assign_pointer() is passed NULL, the Linux
206 kernel provides no ordering, but LKMM models this
207 case as a store release.
208
209 b. The "unless" RMW operations are not currently modeled:
210 atomic_long_add_unless(), atomic_add_unless(),
211 atomic_inc_unless_negative(), and
212 atomic_dec_unless_positive(). These can be emulated
213 in litmus tests, for example, by using atomic_cmpxchg().
214
215 c. The call_rcu() function is not modeled. It can be
216 emulated in litmus tests by adding another process that
217 invokes synchronize_rcu() and the body of the callback
218 function, with (for example) a release-acquire from
219 the site of the emulated call_rcu() to the beginning
220 of the additional process.
221
222 d. The rcu_barrier() function is not modeled. It can be
223 emulated in litmus tests emulating call_rcu() via
224 (for example) a release-acquire from the end of each
225 additional call_rcu() process to the site of the
226 emulated rcu-barrier().
227
228 e. Although sleepable RCU (SRCU) is now modeled, there
229 are some subtle differences between its semantics and
230 those in the Linux kernel. For example, the kernel
231 might interpret the following sequence as two partially
232 overlapping SRCU read-side critical sections:
233
234 1 r1 = srcu_read_lock(&my_srcu);
235 2 do_something_1();
236 3 r2 = srcu_read_lock(&my_srcu);
237 4 do_something_2();
238 5 srcu_read_unlock(&my_srcu, r1);
239 6 do_something_3();
240 7 srcu_read_unlock(&my_srcu, r2);
241
242 In contrast, LKMM will interpret this as a nested pair of
243 SRCU read-side critical sections, with the outer critical
244 section spanning lines 1-7 and the inner critical section
245 spanning lines 3-5.
246
247 This difference would be more of a concern had anyone
248 identified a reasonable use case for partially overlapping
249 SRCU read-side critical sections. For more information,
250 please see: https://paulmck.livejournal.com/40593.html
251
252 f. Reader-writer locking is not modeled. It can be
253 emulated in litmus tests using atomic read-modify-write
254 operations.
255
256The "herd7" tool has some additional limitations of its own, apart from
257the memory model:
258
2591. Non-trivial data structures such as arrays or structures are
260 not supported. However, pointers are supported, allowing trivial
261 linked lists to be constructed.
262
2632. Dynamic memory allocation is not supported, although this can
264 be worked around in some cases by supplying multiple statically
265 allocated variables.
266
267Some of these limitations may be overcome in the future, but others are
268more likely to be addressed by incorporating the Linux-kernel memory model
269into other tools.
270
271Finally, please note that LKMM is subject to change as hardware, use cases,
272and compilers evolve.