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