1 Linux-Kernel Memory Model Litmus Tests 1 Linux-Kernel Memory Model Litmus Tests
2 ====================================== 2 ======================================
3 3
4 This file describes the LKMM litmus-test forma 4 This file describes the LKMM litmus-test format by example, describes
5 some tricks and traps, and finally outlines LK 5 some tricks and traps, and finally outlines LKMM's limitations. Earlier
6 versions of this material appeared in a number 6 versions of this material appeared in a number of LWN articles, including:
7 7
8 https://lwn.net/Articles/720550/ 8 https://lwn.net/Articles/720550/
9 A formal kernel memory-ordering model 9 A formal kernel memory-ordering model (part 2)
10 https://lwn.net/Articles/608550/ 10 https://lwn.net/Articles/608550/
11 Axiomatic validation of memory barrier 11 Axiomatic validation of memory barriers and atomic instructions
12 https://lwn.net/Articles/470681/ 12 https://lwn.net/Articles/470681/
13 Validating Memory Barriers and Atomic 13 Validating Memory Barriers and Atomic Instructions
14 14
15 This document presents information in decreasi 15 This document presents information in decreasing order of applicability,
16 so that, where possible, the information that 16 so that, where possible, the information that has proven more commonly
17 useful is shown near the beginning. 17 useful is shown near the beginning.
18 18
19 For information on installing LKMM, including 19 For information on installing LKMM, including the underlying "herd7"
20 tool, please see tools/memory-model/README. 20 tool, please see tools/memory-model/README.
21 21
22 22
23 Copy-Pasta 23 Copy-Pasta
24 ========== 24 ==========
25 25
26 As with other software, it is often better (if 26 As with other software, it is often better (if less macho) to adapt an
27 existing litmus test than it is to create one 27 existing litmus test than it is to create one from scratch. A number
28 of litmus tests may be found in the kernel sou 28 of litmus tests may be found in the kernel source tree:
29 29
30 tools/memory-model/litmus-tests/ 30 tools/memory-model/litmus-tests/
31 Documentation/litmus-tests/ 31 Documentation/litmus-tests/
32 32
33 Several thousand more example litmus tests are 33 Several thousand more example litmus tests are available on github
34 and kernel.org: 34 and kernel.org:
35 35
36 https://github.com/paulmckrcu/litmus 36 https://github.com/paulmckrcu/litmus
37 https://git.kernel.org/pub/scm/linux/k 37 https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd
38 https://git.kernel.org/pub/scm/linux/k 38 https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus
39 39
40 The -l and -L arguments to "git grep" can be q 40 The -l and -L arguments to "git grep" can be quite helpful in identifying
41 existing litmus tests that are similar to the 41 existing litmus tests that are similar to the one you need. But even if
42 you start with an existing litmus test, it is 42 you start with an existing litmus test, it is still helpful to have a
43 good understanding of the litmus-test format. 43 good understanding of the litmus-test format.
44 44
45 45
46 Examples and Format 46 Examples and Format
47 =================== 47 ===================
48 48
49 This section describes the overall format of l 49 This section describes the overall format of litmus tests, starting
50 with a small example of the message-passing pa 50 with a small example of the message-passing pattern and moving on to
51 more complex examples that illustrate explicit 51 more complex examples that illustrate explicit initialization and LKMM's
52 minimalistic set of flow-control statements. 52 minimalistic set of flow-control statements.
53 53
54 54
55 Message-Passing Example 55 Message-Passing Example
56 ----------------------- 56 -----------------------
57 57
58 This section gives an overview of the format o 58 This section gives an overview of the format of a litmus test using an
59 example based on the common message-passing us 59 example based on the common message-passing use case. This use case
60 appears often in the Linux kernel. For exampl 60 appears often in the Linux kernel. For example, a flag (modeled by "y"
61 below) indicates that a buffer (modeled by "x" 61 below) indicates that a buffer (modeled by "x" below) is now completely
62 filled in and ready for use. It would be very 62 filled in and ready for use. It would be very bad if the consumer saw the
63 flag set, but, due to memory misordering, saw 63 flag set, but, due to memory misordering, saw old values in the buffer.
64 64
65 This example asks whether smp_store_release() 65 This example asks whether smp_store_release() and smp_load_acquire()
66 suffices to avoid this bad outcome: 66 suffices to avoid this bad outcome:
67 67
68 1 C MP+pooncerelease+poacquireonce 68 1 C MP+pooncerelease+poacquireonce
69 2 69 2
70 3 {} 70 3 {}
71 4 71 4
72 5 P0(int *x, int *y) 72 5 P0(int *x, int *y)
73 6 { 73 6 {
74 7 WRITE_ONCE(*x, 1); 74 7 WRITE_ONCE(*x, 1);
75 8 smp_store_release(y, 1); 75 8 smp_store_release(y, 1);
76 9 } 76 9 }
77 10 77 10
78 11 P1(int *x, int *y) 78 11 P1(int *x, int *y)
79 12 { 79 12 {
80 13 int r0; 80 13 int r0;
81 14 int r1; 81 14 int r1;
82 15 82 15
83 16 r0 = smp_load_acquire(y); 83 16 r0 = smp_load_acquire(y);
84 17 r1 = READ_ONCE(*x); 84 17 r1 = READ_ONCE(*x);
85 18 } 85 18 }
86 19 86 19
87 20 exists (1:r0=1 /\ 1:r1=0) 87 20 exists (1:r0=1 /\ 1:r1=0)
88 88
89 Line 1 starts with "C", which identifies this 89 Line 1 starts with "C", which identifies this file as being in the
90 LKMM C-language format (which, as we will see, 90 LKMM C-language format (which, as we will see, is a small fragment
91 of the full C language). The remainder of lin 91 of the full C language). The remainder of line 1 is the name of
92 the test, which by convention is the filename 92 the test, which by convention is the filename with the ".litmus"
93 suffix stripped. In this case, the actual tes 93 suffix stripped. In this case, the actual test may be found in
94 tools/memory-model/litmus-tests/MP+pooncerelea 94 tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
95 in the Linux-kernel source tree. 95 in the Linux-kernel source tree.
96 96
97 Mechanically generated litmus tests will often 97 Mechanically generated litmus tests will often have an optional
98 double-quoted comment string on the second lin 98 double-quoted comment string on the second line. Such strings are ignored
99 when running the test. Yes, you can add your 99 when running the test. Yes, you can add your own comments to litmus
100 tests, but this is a bit involved due to the u 100 tests, but this is a bit involved due to the use of multiple parsers.
101 For now, you can use C-language comments in th 101 For now, you can use C-language comments in the C code, and these comments
102 may be in either the "/* */" or the "//" style 102 may be in either the "/* */" or the "//" style. A later section will
103 cover the full litmus-test commenting story. 103 cover the full litmus-test commenting story.
104 104
105 Line 3 is the initialization section. Because 105 Line 3 is the initialization section. Because the default initialization
106 to zero suffices for this test, the "{}" synta 106 to zero suffices for this test, the "{}" syntax is used, which mean the
107 initialization section is empty. Litmus tests 107 initialization section is empty. Litmus tests requiring non-default
108 initialization must have non-empty initializat 108 initialization must have non-empty initialization sections, as in the
109 example that will be presented later in this d 109 example that will be presented later in this document.
110 110
111 Lines 5-9 show the first process and lines 11- 111 Lines 5-9 show the first process and lines 11-18 the second process. Each
112 process corresponds to a Linux-kernel task (or 112 process corresponds to a Linux-kernel task (or kthread, workqueue, thread,
113 and so on; LKMM discussions often use these te 113 and so on; LKMM discussions often use these terms interchangeably).
114 The name of the first process is "P0" and that 114 The name of the first process is "P0" and that of the second "P1".
115 You can name your processes anything you like 115 You can name your processes anything you like as long as the names consist
116 of a single "P" followed by a number, and as l 116 of a single "P" followed by a number, and as long as the numbers are
117 consecutive starting with zero. This can actu 117 consecutive starting with zero. This can actually be quite helpful,
118 for example, a .litmus file matching "^P1(" bu 118 for example, a .litmus file matching "^P1(" but not matching "^P2("
119 must contain a two-process litmus test. 119 must contain a two-process litmus test.
120 120
121 The argument list for each function are pointe 121 The argument list for each function are pointers to the global variables
122 used by that function. Unlike normal C-langua 122 used by that function. Unlike normal C-language function parameters, the
123 names are significant. The fact that both P0( 123 names are significant. The fact that both P0() and P1() have a formal
124 parameter named "x" means that these two proce 124 parameter named "x" means that these two processes are working with the
125 same global variable, also named "x". So the 125 same global variable, also named "x". So the "int *x, int *y" on P0()
126 and P1() mean that both processes are working 126 and P1() mean that both processes are working with two shared global
127 variables, "x" and "y". Global variables are 127 variables, "x" and "y". Global variables are always passed to processes
128 by reference, hence "P0(int *x, int *y)", but 128 by reference, hence "P0(int *x, int *y)", but *never* "P0(int x, int y)".
129 129
130 P0() has no local variables, but P1() has two 130 P0() has no local variables, but P1() has two of them named "r0" and "r1".
131 These names may be freely chosen, but for hist 131 These names may be freely chosen, but for historical reasons stemming from
132 other litmus-test formats, it is conventional 132 other litmus-test formats, it is conventional to use names consisting of
133 "r" followed by a number as shown here. A com 133 "r" followed by a number as shown here. A common bug in litmus tests
134 is forgetting to add a global variable to a pr 134 is forgetting to add a global variable to a process's parameter list.
135 This will sometimes result in an error message 135 This will sometimes result in an error message, but can also cause the
136 intended global to instead be silently treated 136 intended global to instead be silently treated as an undeclared local
137 variable. 137 variable.
138 138
139 Each process's code is similar to Linux-kernel 139 Each process's code is similar to Linux-kernel C, as can be seen on lines
140 7-8 and 13-17. This code may use many of the 140 7-8 and 13-17. This code may use many of the Linux kernel's atomic
141 operations, some of its exclusive-lock functio 141 operations, some of its exclusive-lock functions, and some of its RCU
142 and SRCU functions. An approximate list of th 142 and SRCU functions. An approximate list of the currently supported
143 functions may be found in the linux-kernel.def 143 functions may be found in the linux-kernel.def file.
144 144
145 The P0() process does "WRITE_ONCE(*x, 1)" on l 145 The P0() process does "WRITE_ONCE(*x, 1)" on line 7. Because "x" is a
146 pointer in P0()'s parameter list, this does an 146 pointer in P0()'s parameter list, this does an unordered store to global
147 variable "x". Line 8 does "smp_store_release( 147 variable "x". Line 8 does "smp_store_release(y, 1)", and because "y"
148 is also in P0()'s parameter list, this does a 148 is also in P0()'s parameter list, this does a release store to global
149 variable "y". 149 variable "y".
150 150
151 The P1() process declares two local variables 151 The P1() process declares two local variables on lines 13 and 14.
152 Line 16 does "r0 = smp_load_acquire(y)" which 152 Line 16 does "r0 = smp_load_acquire(y)" which does an acquire load
153 from global variable "y" into local variable " 153 from global variable "y" into local variable "r0". Line 17 does a
154 "r1 = READ_ONCE(*x)", which does an unordered 154 "r1 = READ_ONCE(*x)", which does an unordered load from "*x" into local
155 variable "r1". Both "x" and "y" are in P1()'s 155 variable "r1". Both "x" and "y" are in P1()'s parameter list, so both
156 reference the same global variables that are u 156 reference the same global variables that are used by P0().
157 157
158 Line 20 is the "exists" assertion expression t 158 Line 20 is the "exists" assertion expression to evaluate the final state.
159 This final state is evaluated after the dust h 159 This final state is evaluated after the dust has settled: both processes
160 have completed and all of their memory referen 160 have completed and all of their memory references and memory barriers
161 have propagated to all parts of the system. T 161 have propagated to all parts of the system. The references to the local
162 variables "r0" and "r1" in line 24 must be pre 162 variables "r0" and "r1" in line 24 must be prefixed with "1:" to specify
163 which process they are local to. 163 which process they are local to.
164 164
165 Note that the assertion expression is written 165 Note that the assertion expression is written in the litmus-test
166 language rather than in C. For example, singl 166 language rather than in C. For example, single "=" is an equality
167 operator rather than an assignment. The "/\" 167 operator rather than an assignment. The "/\" character combination means
168 "and". Similarly, "\/" stands for "or". Both 168 "and". Similarly, "\/" stands for "or". Both of these are ASCII-art
169 representations of the corresponding mathemati 169 representations of the corresponding mathematical symbols. Finally,
170 "~" stands for "logical not", which is "!" in 170 "~" stands for "logical not", which is "!" in C, and not to be confused
171 with the C-language "~" operator which instead 171 with the C-language "~" operator which instead stands for "bitwise not".
172 Parentheses may be used to override precedence 172 Parentheses may be used to override precedence.
173 173
174 The "exists" assertion on line 20 is satisfied 174 The "exists" assertion on line 20 is satisfied if the consumer sees the
175 flag ("y") set but the buffer ("x") as not yet 175 flag ("y") set but the buffer ("x") as not yet filled in, that is, if P1()
176 loaded a value from "x" that was equal to 1 bu 176 loaded a value from "x" that was equal to 1 but loaded a value from "y"
177 that was still equal to zero. 177 that was still equal to zero.
178 178
179 This example can be checked by running the fol 179 This example can be checked by running the following command, which
180 absolutely must be run from the tools/memory-m 180 absolutely must be run from the tools/memory-model directory and from
181 this directory only: 181 this directory only:
182 182
183 herd7 -conf linux-kernel.cfg litmus-tests/MP+p 183 herd7 -conf linux-kernel.cfg litmus-tests/MP+pooncerelease+poacquireonce.litmus
184 184
185 The output is the result of something similar 185 The output is the result of something similar to a full state-space
186 search, and is as follows: 186 search, and is as follows:
187 187
188 1 Test MP+pooncerelease+poacquireonce Allowed 188 1 Test MP+pooncerelease+poacquireonce Allowed
189 2 States 3 189 2 States 3
190 3 1:r0=0; 1:r1=0; 190 3 1:r0=0; 1:r1=0;
191 4 1:r0=0; 1:r1=1; 191 4 1:r0=0; 1:r1=1;
192 5 1:r0=1; 1:r1=1; 192 5 1:r0=1; 1:r1=1;
193 6 No 193 6 No
194 7 Witnesses 194 7 Witnesses
195 8 Positive: 0 Negative: 3 195 8 Positive: 0 Negative: 3
196 9 Condition exists (1:r0=1 /\ 1:r1=0) 196 9 Condition exists (1:r0=1 /\ 1:r1=0)
197 10 Observation MP+pooncerelease+poacquireonce 197 10 Observation MP+pooncerelease+poacquireonce Never 0 3
198 11 Time MP+pooncerelease+poacquireonce 0.00 198 11 Time MP+pooncerelease+poacquireonce 0.00
199 12 Hash=579aaa14d8c35a39429b02e698241d09 199 12 Hash=579aaa14d8c35a39429b02e698241d09
200 200
201 The most pertinent line is line 10, which cont 201 The most pertinent line is line 10, which contains "Never 0 3", which
202 indicates that the bad result flagged by the " 202 indicates that the bad result flagged by the "exists" clause never
203 happens. This line might instead say "Sometim 203 happens. This line might instead say "Sometimes" to indicate that the
204 bad result happened in some but not all execut 204 bad result happened in some but not all executions, or it might say
205 "Always" to indicate that the bad result happe 205 "Always" to indicate that the bad result happened in all executions.
206 (The herd7 tool doesn't judge, so it is only a 206 (The herd7 tool doesn't judge, so it is only an LKMM convention that the
207 "exists" clause indicates a bad result. To se 207 "exists" clause indicates a bad result. To see this, invert the "exists"
208 clause's condition and run the test.) The num 208 clause's condition and run the test.) The numbers ("0 3") at the end
209 of this line indicate the number of end states 209 of this line indicate the number of end states satisfying the "exists"
210 clause (0) and the number not not satisfying t 210 clause (0) and the number not not satisfying that clause (3).
211 211
212 Another important part of this output is shown 212 Another important part of this output is shown in lines 2-5, repeated here:
213 213
214 2 States 3 214 2 States 3
215 3 1:r0=0; 1:r1=0; 215 3 1:r0=0; 1:r1=0;
216 4 1:r0=0; 1:r1=1; 216 4 1:r0=0; 1:r1=1;
217 5 1:r0=1; 1:r1=1; 217 5 1:r0=1; 1:r1=1;
218 218
219 Line 2 gives the total number of end states, a 219 Line 2 gives the total number of end states, and each of lines 3-5 list
220 one of these states, with the first ("1:r0=0; 220 one of these states, with the first ("1:r0=0; 1:r1=0;") indicating that
221 both of P1()'s loads returned the value "0". 221 both of P1()'s loads returned the value "0". As expected, given the
222 "Never" on line 10, the state flagged by the " 222 "Never" on line 10, the state flagged by the "exists" clause is not
223 listed. This full list of states can be helpf 223 listed. This full list of states can be helpful when debugging a new
224 litmus test. 224 litmus test.
225 225
226 The rest of the output is not normally needed, 226 The rest of the output is not normally needed, either due to irrelevance
227 or due to being redundant with the lines discu 227 or due to being redundant with the lines discussed above. However, the
228 following paragraph lists them for the benefit 228 following paragraph lists them for the benefit of readers possessed of
229 an insatiable curiosity. Other readers should 229 an insatiable curiosity. Other readers should feel free to skip ahead.
230 230
231 Line 1 echos the test name, along with the "Te 231 Line 1 echos the test name, along with the "Test" and "Allowed". Line 6's
232 "No" says that the "exists" clause was not sat 232 "No" says that the "exists" clause was not satisfied by any execution,
233 and as such it has the same meaning as line 10 233 and as such it has the same meaning as line 10's "Never". Line 7 is a
234 lead-in to line 8's "Positive: 0 Negative: 3", 234 lead-in to line 8's "Positive: 0 Negative: 3", which lists the number
235 of end states satisfying and not satisfying th 235 of end states satisfying and not satisfying the "exists" clause, just
236 like the two numbers at the end of line 10. L 236 like the two numbers at the end of line 10. Line 9 repeats the "exists"
237 clause so that you don't have to look it up in 237 clause so that you don't have to look it up in the litmus-test file.
238 The number at the end of line 11 (which begins 238 The number at the end of line 11 (which begins with "Time") gives the
239 time in seconds required to analyze the litmus 239 time in seconds required to analyze the litmus test. Small tests such
240 as this one complete in a few milliseconds, so 240 as this one complete in a few milliseconds, so "0.00" is quite common.
241 Line 12 gives a hash of the contents for the l 241 Line 12 gives a hash of the contents for the litmus-test file, and is used
242 by tooling that manages litmus tests and their 242 by tooling that manages litmus tests and their output. This tooling is
243 used by people modifying LKMM itself, and amon 243 used by people modifying LKMM itself, and among other things lets such
244 people know which of the several thousand rele 244 people know which of the several thousand relevant litmus tests were
245 affected by a given change to LKMM. 245 affected by a given change to LKMM.
246 246
247 247
248 Initialization 248 Initialization
249 -------------- 249 --------------
250 250
251 The previous example relied on the default zer 251 The previous example relied on the default zero initialization for
252 "x" and "y", but a similar litmus test could i 252 "x" and "y", but a similar litmus test could instead initialize them
253 to some other value: 253 to some other value:
254 254
255 1 C MP+pooncerelease+poacquireonce 255 1 C MP+pooncerelease+poacquireonce
256 2 256 2
257 3 { 257 3 {
258 4 x=42; 258 4 x=42;
259 5 y=42; 259 5 y=42;
260 6 } 260 6 }
261 7 261 7
262 8 P0(int *x, int *y) 262 8 P0(int *x, int *y)
263 9 { 263 9 {
264 10 WRITE_ONCE(*x, 1); 264 10 WRITE_ONCE(*x, 1);
265 11 smp_store_release(y, 1); 265 11 smp_store_release(y, 1);
266 12 } 266 12 }
267 13 267 13
268 14 P1(int *x, int *y) 268 14 P1(int *x, int *y)
269 15 { 269 15 {
270 16 int r0; 270 16 int r0;
271 17 int r1; 271 17 int r1;
272 18 272 18
273 19 r0 = smp_load_acquire(y); 273 19 r0 = smp_load_acquire(y);
274 20 r1 = READ_ONCE(*x); 274 20 r1 = READ_ONCE(*x);
275 21 } 275 21 }
276 22 276 22
277 23 exists (1:r0=1 /\ 1:r1=42) 277 23 exists (1:r0=1 /\ 1:r1=42)
278 278
279 Lines 3-6 now initialize both "x" and "y" to t 279 Lines 3-6 now initialize both "x" and "y" to the value 42. This also
280 means that the "exists" clause on line 23 must 280 means that the "exists" clause on line 23 must change "1:r1=0" to
281 "1:r1=42". 281 "1:r1=42".
282 282
283 Running the test gives the same overall result 283 Running the test gives the same overall result as before, but with the
284 value 42 appearing in place of the value zero: 284 value 42 appearing in place of the value zero:
285 285
286 1 Test MP+pooncerelease+poacquireonce Allowed 286 1 Test MP+pooncerelease+poacquireonce Allowed
287 2 States 3 287 2 States 3
288 3 1:r0=1; 1:r1=1; 288 3 1:r0=1; 1:r1=1;
289 4 1:r0=42; 1:r1=1; 289 4 1:r0=42; 1:r1=1;
290 5 1:r0=42; 1:r1=42; 290 5 1:r0=42; 1:r1=42;
291 6 No 291 6 No
292 7 Witnesses 292 7 Witnesses
293 8 Positive: 0 Negative: 3 293 8 Positive: 0 Negative: 3
294 9 Condition exists (1:r0=1 /\ 1:r1=42) 294 9 Condition exists (1:r0=1 /\ 1:r1=42)
295 10 Observation MP+pooncerelease+poacquireonce 295 10 Observation MP+pooncerelease+poacquireonce Never 0 3
296 11 Time MP+pooncerelease+poacquireonce 0.02 296 11 Time MP+pooncerelease+poacquireonce 0.02
297 12 Hash=ab9a9b7940a75a792266be279a980156 297 12 Hash=ab9a9b7940a75a792266be279a980156
298 298
299 It is tempting to avoid the open-coded repetit 299 It is tempting to avoid the open-coded repetitions of the value "42"
300 by defining another global variable "initval=4 300 by defining another global variable "initval=42" and replacing all
301 occurrences of "42" with "initval". This will 301 occurrences of "42" with "initval". This will not, repeat *not*,
302 initialize "x" and "y" to 42, but instead to t 302 initialize "x" and "y" to 42, but instead to the address of "initval"
303 (try it!). See the section below on linked li 303 (try it!). See the section below on linked lists to learn more about
304 why this approach to initialization can be use 304 why this approach to initialization can be useful.
305 305
306 306
307 Control Structures 307 Control Structures
308 ------------------ 308 ------------------
309 309
310 LKMM supports the C-language "if" statement, w 310 LKMM supports the C-language "if" statement, which allows modeling of
311 conditional branches. In LKMM, conditional br 311 conditional branches. In LKMM, conditional branches can affect ordering,
312 but only if you are *very* careful (compilers 312 but only if you are *very* careful (compilers are surprisingly able
313 to optimize away conditional branches). The f 313 to optimize away conditional branches). The following example shows
314 the "load buffering" (LB) use case that is use 314 the "load buffering" (LB) use case that is used in the Linux kernel to
315 synchronize between ring-buffer producers and 315 synchronize between ring-buffer producers and consumers. In the example
316 below, P0() is one side checking to see if an 316 below, P0() is one side checking to see if an operation may proceed and
317 P1() is the other side completing its update. 317 P1() is the other side completing its update.
318 318
319 1 C LB+fencembonceonce+ctrlonceonce 319 1 C LB+fencembonceonce+ctrlonceonce
320 2 320 2
321 3 {} 321 3 {}
322 4 322 4
323 5 P0(int *x, int *y) 323 5 P0(int *x, int *y)
324 6 { 324 6 {
325 7 int r0; 325 7 int r0;
326 8 326 8
327 9 r0 = READ_ONCE(*x); 327 9 r0 = READ_ONCE(*x);
328 10 if (r0) 328 10 if (r0)
329 11 WRITE_ONCE(*y, 1); 329 11 WRITE_ONCE(*y, 1);
330 12 } 330 12 }
331 13 331 13
332 14 P1(int *x, int *y) 332 14 P1(int *x, int *y)
333 15 { 333 15 {
334 16 int r0; 334 16 int r0;
335 17 335 17
336 18 r0 = READ_ONCE(*y); 336 18 r0 = READ_ONCE(*y);
337 19 smp_mb(); 337 19 smp_mb();
338 20 WRITE_ONCE(*x, 1); 338 20 WRITE_ONCE(*x, 1);
339 21 } 339 21 }
340 22 340 22
341 23 exists (0:r0=1 /\ 1:r0=1) 341 23 exists (0:r0=1 /\ 1:r0=1)
342 342
343 P1()'s "if" statement on line 10 works as expe 343 P1()'s "if" statement on line 10 works as expected, so that line 11 is
344 executed only if line 9 loads a non-zero value 344 executed only if line 9 loads a non-zero value from "x". Because P1()'s
345 write of "1" to "x" happens only after P1()'s 345 write of "1" to "x" happens only after P1()'s read from "y", one would
346 hope that the "exists" clause cannot be satisf 346 hope that the "exists" clause cannot be satisfied. LKMM agrees:
347 347
348 1 Test LB+fencembonceonce+ctrlonceonce Allowe 348 1 Test LB+fencembonceonce+ctrlonceonce Allowed
349 2 States 2 349 2 States 2
350 3 0:r0=0; 1:r0=0; 350 3 0:r0=0; 1:r0=0;
351 4 0:r0=1; 1:r0=0; 351 4 0:r0=1; 1:r0=0;
352 5 No 352 5 No
353 6 Witnesses 353 6 Witnesses
354 7 Positive: 0 Negative: 2 354 7 Positive: 0 Negative: 2
355 8 Condition exists (0:r0=1 /\ 1:r0=1) 355 8 Condition exists (0:r0=1 /\ 1:r0=1)
356 9 Observation LB+fencembonceonce+ctrlonceonce 356 9 Observation LB+fencembonceonce+ctrlonceonce Never 0 2
357 10 Time LB+fencembonceonce+ctrlonceonce 0.00 357 10 Time LB+fencembonceonce+ctrlonceonce 0.00
358 11 Hash=e5260556f6de495fd39b556d1b831c3b 358 11 Hash=e5260556f6de495fd39b556d1b831c3b
359 359
360 However, there is no "while" statement due to 360 However, there is no "while" statement due to the fact that full
361 state-space search has some difficulty with it 361 state-space search has some difficulty with iteration. However, there
362 are tricks that may be used to handle some spe 362 are tricks that may be used to handle some special cases, which are
363 discussed below. In addition, loop-unrolling 363 discussed below. In addition, loop-unrolling tricks may be applied,
364 albeit sparingly. 364 albeit sparingly.
365 365
366 366
367 Tricks and Traps 367 Tricks and Traps
368 ================ 368 ================
369 369
370 This section covers extracting debug output fr 370 This section covers extracting debug output from herd7, emulating
371 spin loops, handling trivial linked lists, add 371 spin loops, handling trivial linked lists, adding comments to litmus tests,
372 emulating call_rcu(), and finally tricks to im 372 emulating call_rcu(), and finally tricks to improve herd7 performance
373 in order to better handle large litmus tests. 373 in order to better handle large litmus tests.
374 374
375 375
376 Debug Output 376 Debug Output
377 ------------ 377 ------------
378 378
379 By default, the herd7 state output includes al 379 By default, the herd7 state output includes all variables mentioned
380 in the "exists" clause. But sometimes debuggi 380 in the "exists" clause. But sometimes debugging efforts are greatly
381 aided by the values of other variables. Consi 381 aided by the values of other variables. Consider this litmus test
382 (tools/memory-order/litmus-tests/SB+rfionceonc 382 (tools/memory-order/litmus-tests/SB+rfionceonce-poonceonces.litmus but
383 slightly modified), which probes an obscure co 383 slightly modified), which probes an obscure corner of hardware memory
384 ordering: 384 ordering:
385 385
386 1 C SB+rfionceonce-poonceonces 386 1 C SB+rfionceonce-poonceonces
387 2 387 2
388 3 {} 388 3 {}
389 4 389 4
390 5 P0(int *x, int *y) 390 5 P0(int *x, int *y)
391 6 { 391 6 {
392 7 int r1; 392 7 int r1;
393 8 int r2; 393 8 int r2;
394 9 394 9
395 10 WRITE_ONCE(*x, 1); 395 10 WRITE_ONCE(*x, 1);
396 11 r1 = READ_ONCE(*x); 396 11 r1 = READ_ONCE(*x);
397 12 r2 = READ_ONCE(*y); 397 12 r2 = READ_ONCE(*y);
398 13 } 398 13 }
399 14 399 14
400 15 P1(int *x, int *y) 400 15 P1(int *x, int *y)
401 16 { 401 16 {
402 17 int r3; 402 17 int r3;
403 18 int r4; 403 18 int r4;
404 19 404 19
405 20 WRITE_ONCE(*y, 1); 405 20 WRITE_ONCE(*y, 1);
406 21 r3 = READ_ONCE(*y); 406 21 r3 = READ_ONCE(*y);
407 22 r4 = READ_ONCE(*x); 407 22 r4 = READ_ONCE(*x);
408 23 } 408 23 }
409 24 409 24
410 25 exists (0:r2=0 /\ 1:r4=0) 410 25 exists (0:r2=0 /\ 1:r4=0)
411 411
412 The herd7 output is as follows: 412 The herd7 output is as follows:
413 413
414 1 Test SB+rfionceonce-poonceonces Allowed 414 1 Test SB+rfionceonce-poonceonces Allowed
415 2 States 4 415 2 States 4
416 3 0:r2=0; 1:r4=0; 416 3 0:r2=0; 1:r4=0;
417 4 0:r2=0; 1:r4=1; 417 4 0:r2=0; 1:r4=1;
418 5 0:r2=1; 1:r4=0; 418 5 0:r2=1; 1:r4=0;
419 6 0:r2=1; 1:r4=1; 419 6 0:r2=1; 1:r4=1;
420 7 Ok 420 7 Ok
421 8 Witnesses 421 8 Witnesses
422 9 Positive: 1 Negative: 3 422 9 Positive: 1 Negative: 3
423 10 Condition exists (0:r2=0 /\ 1:r4=0) 423 10 Condition exists (0:r2=0 /\ 1:r4=0)
424 11 Observation SB+rfionceonce-poonceonces Some 424 11 Observation SB+rfionceonce-poonceonces Sometimes 1 3
425 12 Time SB+rfionceonce-poonceonces 0.01 425 12 Time SB+rfionceonce-poonceonces 0.01
426 13 Hash=c7f30fe0faebb7d565405d55b7318ada 426 13 Hash=c7f30fe0faebb7d565405d55b7318ada
427 427
428 (This output indicates that CPUs are permitted 428 (This output indicates that CPUs are permitted to "snoop their own
429 store buffers", which all of Linux's CPU famil 429 store buffers", which all of Linux's CPU families other than s390 will
430 happily do. Such snooping results in disagree 430 happily do. Such snooping results in disagreement among CPUs on the
431 order of stores from different CPUs, which is 431 order of stores from different CPUs, which is rarely an issue.)
432 432
433 But the herd7 output shows only the two variab 433 But the herd7 output shows only the two variables mentioned in the
434 "exists" clause. Someone modifying this test 434 "exists" clause. Someone modifying this test might wish to know the
435 values of "x", "y", "0:r1", and "0:r3" as well 435 values of "x", "y", "0:r1", and "0:r3" as well. The "locations"
436 statement on line 25 shows how to cause herd7 436 statement on line 25 shows how to cause herd7 to display additional
437 variables: 437 variables:
438 438
439 1 C SB+rfionceonce-poonceonces 439 1 C SB+rfionceonce-poonceonces
440 2 440 2
441 3 {} 441 3 {}
442 4 442 4
443 5 P0(int *x, int *y) 443 5 P0(int *x, int *y)
444 6 { 444 6 {
445 7 int r1; 445 7 int r1;
446 8 int r2; 446 8 int r2;
447 9 447 9
448 10 WRITE_ONCE(*x, 1); 448 10 WRITE_ONCE(*x, 1);
449 11 r1 = READ_ONCE(*x); 449 11 r1 = READ_ONCE(*x);
450 12 r2 = READ_ONCE(*y); 450 12 r2 = READ_ONCE(*y);
451 13 } 451 13 }
452 14 452 14
453 15 P1(int *x, int *y) 453 15 P1(int *x, int *y)
454 16 { 454 16 {
455 17 int r3; 455 17 int r3;
456 18 int r4; 456 18 int r4;
457 19 457 19
458 20 WRITE_ONCE(*y, 1); 458 20 WRITE_ONCE(*y, 1);
459 21 r3 = READ_ONCE(*y); 459 21 r3 = READ_ONCE(*y);
460 22 r4 = READ_ONCE(*x); 460 22 r4 = READ_ONCE(*x);
461 23 } 461 23 }
462 24 462 24
463 25 locations [0:r1; 1:r3; x; y] 463 25 locations [0:r1; 1:r3; x; y]
464 26 exists (0:r2=0 /\ 1:r4=0) 464 26 exists (0:r2=0 /\ 1:r4=0)
465 465
466 The herd7 output then displays the values of a 466 The herd7 output then displays the values of all the variables:
467 467
468 1 Test SB+rfionceonce-poonceonces Allowed 468 1 Test SB+rfionceonce-poonceonces Allowed
469 2 States 4 469 2 States 4
470 3 0:r1=1; 0:r2=0; 1:r3=1; 1:r4=0; x=1; y=1; 470 3 0:r1=1; 0:r2=0; 1:r3=1; 1:r4=0; x=1; y=1;
471 4 0:r1=1; 0:r2=0; 1:r3=1; 1:r4=1; x=1; y=1; 471 4 0:r1=1; 0:r2=0; 1:r3=1; 1:r4=1; x=1; y=1;
472 5 0:r1=1; 0:r2=1; 1:r3=1; 1:r4=0; x=1; y=1; 472 5 0:r1=1; 0:r2=1; 1:r3=1; 1:r4=0; x=1; y=1;
473 6 0:r1=1; 0:r2=1; 1:r3=1; 1:r4=1; x=1; y=1; 473 6 0:r1=1; 0:r2=1; 1:r3=1; 1:r4=1; x=1; y=1;
474 7 Ok 474 7 Ok
475 8 Witnesses 475 8 Witnesses
476 9 Positive: 1 Negative: 3 476 9 Positive: 1 Negative: 3
477 10 Condition exists (0:r2=0 /\ 1:r4=0) 477 10 Condition exists (0:r2=0 /\ 1:r4=0)
478 11 Observation SB+rfionceonce-poonceonces Some 478 11 Observation SB+rfionceonce-poonceonces Sometimes 1 3
479 12 Time SB+rfionceonce-poonceonces 0.01 479 12 Time SB+rfionceonce-poonceonces 0.01
480 13 Hash=40de8418c4b395388f6501cafd1ed38d 480 13 Hash=40de8418c4b395388f6501cafd1ed38d
481 481
482 What if you would like to know the value of a 482 What if you would like to know the value of a particular global variable
483 at some particular point in a given process's 483 at some particular point in a given process's execution? One approach
484 is to use a READ_ONCE() to load that global va 484 is to use a READ_ONCE() to load that global variable into a new local
485 variable, then add that local variable to the 485 variable, then add that local variable to the "locations" clause.
486 But be careful: In some litmus tests, adding 486 But be careful: In some litmus tests, adding a READ_ONCE() will change
487 the outcome! For one example, please see the 487 the outcome! For one example, please see the C-READ_ONCE.litmus and
488 C-READ_ONCE-omitted.litmus tests located here: 488 C-READ_ONCE-omitted.litmus tests located here:
489 489
490 https://github.com/paulmckrcu/litmus/b 490 https://github.com/paulmckrcu/litmus/blob/master/manual/kernel/
491 491
492 492
493 Spin Loops 493 Spin Loops
494 ---------- 494 ----------
495 495
496 The analysis carried out by herd7 explores ful 496 The analysis carried out by herd7 explores full state space, which is
497 at best of exponential time complexity. Addin 497 at best of exponential time complexity. Adding processes and increasing
498 the amount of code in a give process can great 498 the amount of code in a give process can greatly increase execution time.
499 Potentially infinite loops, such as those used 499 Potentially infinite loops, such as those used to wait for locks to
500 become available, are clearly problematic. 500 become available, are clearly problematic.
501 501
502 Fortunately, it is possible to avoid state-spa 502 Fortunately, it is possible to avoid state-space explosion by specially
503 modeling such loops. For example, the followi 503 modeling such loops. For example, the following litmus tests emulates
504 locking using xchg_acquire(), but instead of e 504 locking using xchg_acquire(), but instead of enclosing xchg_acquire()
505 in a spin loop, it instead excludes executions 505 in a spin loop, it instead excludes executions that fail to acquire the
506 lock using a herd7 "filter" clause. Note that 506 lock using a herd7 "filter" clause. Note that for exclusive locking, you
507 are better off using the spin_lock() and spin_ 507 are better off using the spin_lock() and spin_unlock() that LKMM directly
508 models, if for no other reason that these are 508 models, if for no other reason that these are much faster. However, the
509 techniques illustrated in this section can be 509 techniques illustrated in this section can be used for other purposes,
510 such as emulating reader-writer locking, which 510 such as emulating reader-writer locking, which LKMM does not yet model.
511 511
512 1 C C-SB+l-o-o-u+l-o-o-u-X 512 1 C C-SB+l-o-o-u+l-o-o-u-X
513 2 513 2
514 3 { 514 3 {
515 4 } 515 4 }
516 5 516 5
517 6 P0(int *sl, int *x0, int *x1) 517 6 P0(int *sl, int *x0, int *x1)
518 7 { 518 7 {
519 8 int r2; 519 8 int r2;
520 9 int r1; 520 9 int r1;
521 10 521 10
522 11 r2 = xchg_acquire(sl, 1); 522 11 r2 = xchg_acquire(sl, 1);
523 12 WRITE_ONCE(*x0, 1); 523 12 WRITE_ONCE(*x0, 1);
524 13 r1 = READ_ONCE(*x1); 524 13 r1 = READ_ONCE(*x1);
525 14 smp_store_release(sl, 0); 525 14 smp_store_release(sl, 0);
526 15 } 526 15 }
527 16 527 16
528 17 P1(int *sl, int *x0, int *x1) 528 17 P1(int *sl, int *x0, int *x1)
529 18 { 529 18 {
530 19 int r2; 530 19 int r2;
531 20 int r1; 531 20 int r1;
532 21 532 21
533 22 r2 = xchg_acquire(sl, 1); 533 22 r2 = xchg_acquire(sl, 1);
534 23 WRITE_ONCE(*x1, 1); 534 23 WRITE_ONCE(*x1, 1);
535 24 r1 = READ_ONCE(*x0); 535 24 r1 = READ_ONCE(*x0);
536 25 smp_store_release(sl, 0); 536 25 smp_store_release(sl, 0);
537 26 } 537 26 }
538 27 538 27
539 28 filter (0:r2=0 /\ 1:r2=0) 539 28 filter (0:r2=0 /\ 1:r2=0)
540 29 exists (0:r1=0 /\ 1:r1=0) 540 29 exists (0:r1=0 /\ 1:r1=0)
541 541
542 This litmus test may be found here: 542 This litmus test may be found here:
543 543
544 https://git.kernel.org/pub/scm/linux/kernel/gi 544 https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus
545 545
546 This test uses two global variables, "x1" and 546 This test uses two global variables, "x1" and "x2", and also emulates a
547 single global spinlock named "sl". This spinl 547 single global spinlock named "sl". This spinlock is held by whichever
548 process changes the value of "sl" from "0" to 548 process changes the value of "sl" from "0" to "1", and is released when
549 that process sets "sl" back to "0". P0()'s lo 549 that process sets "sl" back to "0". P0()'s lock acquisition is emulated
550 on line 11 using xchg_acquire(), which uncondi 550 on line 11 using xchg_acquire(), which unconditionally stores the value
551 "1" to "sl" and stores either "0" or "1" to "r 551 "1" to "sl" and stores either "0" or "1" to "r2", depending on whether
552 the lock acquisition was successful or unsucce 552 the lock acquisition was successful or unsuccessful (due to "sl" already
553 having the value "1"), respectively. P1() ope 553 having the value "1"), respectively. P1() operates in a similar manner.
554 554
555 Rather unconventionally, execution appears to 555 Rather unconventionally, execution appears to proceed to the critical
556 section on lines 12 and 13 in either case. Li 556 section on lines 12 and 13 in either case. Line 14 then uses an
557 smp_store_release() to store zero to "sl", thu 557 smp_store_release() to store zero to "sl", thus emulating lock release.
558 558
559 The case where xchg_acquire() fails to acquire 559 The case where xchg_acquire() fails to acquire the lock is handled by
560 the "filter" clause on line 28, which tells he 560 the "filter" clause on line 28, which tells herd7 to keep only those
561 executions in which both "0:r2" and "1:r2" are 561 executions in which both "0:r2" and "1:r2" are zero, that is to pay
562 attention only to those executions in which bo 562 attention only to those executions in which both locks are actually
563 acquired. Thus, the bogus executions that wou 563 acquired. Thus, the bogus executions that would execute the critical
564 sections are discarded and any effects that th 564 sections are discarded and any effects that they might have had are
565 ignored. Note well that the "filter" clause k 565 ignored. Note well that the "filter" clause keeps those executions
566 for which its expression is satisfied, that is 566 for which its expression is satisfied, that is, for which the expression
567 evaluates to true. In other words, the "filte 567 evaluates to true. In other words, the "filter" clause says what to
568 keep, not what to discard. 568 keep, not what to discard.
569 569
570 The result of running this test is as follows: 570 The result of running this test is as follows:
571 571
572 1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed 572 1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed
573 2 States 2 573 2 States 2
574 3 0:r1=0; 1:r1=1; 574 3 0:r1=0; 1:r1=1;
575 4 0:r1=1; 1:r1=0; 575 4 0:r1=1; 1:r1=0;
576 5 No 576 5 No
577 6 Witnesses 577 6 Witnesses
578 7 Positive: 0 Negative: 2 578 7 Positive: 0 Negative: 2
579 8 Condition exists (0:r1=0 /\ 1:r1=0) 579 8 Condition exists (0:r1=0 /\ 1:r1=0)
580 9 Observation C-SB+l-o-o-u+l-o-o-u-X Never 0 580 9 Observation C-SB+l-o-o-u+l-o-o-u-X Never 0 2
581 10 Time C-SB+l-o-o-u+l-o-o-u-X 0.03 581 10 Time C-SB+l-o-o-u+l-o-o-u-X 0.03
582 582
583 The "Never" on line 9 indicates that this use 583 The "Never" on line 9 indicates that this use of xchg_acquire() and
584 smp_store_release() really does correctly emul 584 smp_store_release() really does correctly emulate locking.
585 585
586 Why doesn't the litmus test take the simpler a 586 Why doesn't the litmus test take the simpler approach of using a spin loop
587 to handle failed spinlock acquisitions, like t 587 to handle failed spinlock acquisitions, like the kernel does? The key
588 insight behind this litmus test is that spin l 588 insight behind this litmus test is that spin loops have no effect on the
589 possible "exists"-clause outcomes of program e 589 possible "exists"-clause outcomes of program execution in the absence
590 of deadlock. In other words, given a high-qua 590 of deadlock. In other words, given a high-quality lock-acquisition
591 primitive in a deadlock-free program running o 591 primitive in a deadlock-free program running on high-quality hardware,
592 each lock acquisition will eventually succeed. 592 each lock acquisition will eventually succeed. Because herd7 already
593 explores the full state space, the length of t 593 explores the full state space, the length of time required to actually
594 acquire the lock does not matter. After all, 594 acquire the lock does not matter. After all, herd7 already models all
595 possible durations of the xchg_acquire() state 595 possible durations of the xchg_acquire() statements.
596 596
597 Why not just add the "filter" clause to the "e 597 Why not just add the "filter" clause to the "exists" clause, thus
598 avoiding the "filter" clause entirely? This d 598 avoiding the "filter" clause entirely? This does work, but is slower.
599 The reason that the "filter" clause is faster 599 The reason that the "filter" clause is faster is that (in the common case)
600 herd7 knows to abandon an execution as soon as 600 herd7 knows to abandon an execution as soon as the "filter" expression
601 fails to be satisfied. In contrast, the "exis 601 fails to be satisfied. In contrast, the "exists" clause is evaluated
602 only at the end of time, thus requiring herd7 602 only at the end of time, thus requiring herd7 to waste time on bogus
603 executions in which both critical sections pro 603 executions in which both critical sections proceed concurrently. In
604 addition, some LKMM users like the separation 604 addition, some LKMM users like the separation of concerns provided by
605 using the both the "filter" and "exists" claus 605 using the both the "filter" and "exists" clauses.
606 606
607 Readers lacking a pathological interest in odd 607 Readers lacking a pathological interest in odd corner cases should feel
608 free to skip the remainder of this section. 608 free to skip the remainder of this section.
609 609
610 But what if the litmus test were to temporaril 610 But what if the litmus test were to temporarily set "0:r2" to a non-zero
611 value? Wouldn't that cause herd7 to abandon t 611 value? Wouldn't that cause herd7 to abandon the execution prematurely
612 due to an early mismatch of the "filter" claus 612 due to an early mismatch of the "filter" clause?
613 613
614 Why not just try it? Line 4 of the following 614 Why not just try it? Line 4 of the following modified litmus test
615 introduces a new global variable "x2" that is 615 introduces a new global variable "x2" that is initialized to "1". Line 23
616 of P1() reads that variable into "1:r2" to for 616 of P1() reads that variable into "1:r2" to force an early mismatch with
617 the "filter" clause. Line 24 does a known-tru 617 the "filter" clause. Line 24 does a known-true "if" condition to avoid
618 and static analysis that herd7 might do. Fina 618 and static analysis that herd7 might do. Finally the "exists" clause
619 on line 32 is updated to a condition that is a 619 on line 32 is updated to a condition that is alway satisfied at the end
620 of the test. 620 of the test.
621 621
622 1 C C-SB+l-o-o-u+l-o-o-u-X 622 1 C C-SB+l-o-o-u+l-o-o-u-X
623 2 623 2
624 3 { 624 3 {
625 4 x2=1; 625 4 x2=1;
626 5 } 626 5 }
627 6 627 6
628 7 P0(int *sl, int *x0, int *x1) 628 7 P0(int *sl, int *x0, int *x1)
629 8 { 629 8 {
630 9 int r2; 630 9 int r2;
631 10 int r1; 631 10 int r1;
632 11 632 11
633 12 r2 = xchg_acquire(sl, 1); 633 12 r2 = xchg_acquire(sl, 1);
634 13 WRITE_ONCE(*x0, 1); 634 13 WRITE_ONCE(*x0, 1);
635 14 r1 = READ_ONCE(*x1); 635 14 r1 = READ_ONCE(*x1);
636 15 smp_store_release(sl, 0); 636 15 smp_store_release(sl, 0);
637 16 } 637 16 }
638 17 638 17
639 18 P1(int *sl, int *x0, int *x1, int *x2) 639 18 P1(int *sl, int *x0, int *x1, int *x2)
640 19 { 640 19 {
641 20 int r2; 641 20 int r2;
642 21 int r1; 642 21 int r1;
643 22 643 22
644 23 r2 = READ_ONCE(*x2); 644 23 r2 = READ_ONCE(*x2);
645 24 if (r2) 645 24 if (r2)
646 25 r2 = xchg_acquire(sl, 1); 646 25 r2 = xchg_acquire(sl, 1);
647 26 WRITE_ONCE(*x1, 1); 647 26 WRITE_ONCE(*x1, 1);
648 27 r1 = READ_ONCE(*x0); 648 27 r1 = READ_ONCE(*x0);
649 28 smp_store_release(sl, 0); 649 28 smp_store_release(sl, 0);
650 29 } 650 29 }
651 30 651 30
652 31 filter (0:r2=0 /\ 1:r2=0) 652 31 filter (0:r2=0 /\ 1:r2=0)
653 32 exists (x1=1) 653 32 exists (x1=1)
654 654
655 If the "filter" clause were to check each vari 655 If the "filter" clause were to check each variable at each point in the
656 execution, running this litmus test would disp 656 execution, running this litmus test would display no executions because
657 all executions would be filtered out at line 2 657 all executions would be filtered out at line 23. However, the output
658 is instead as follows: 658 is instead as follows:
659 659
660 1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed 660 1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed
661 2 States 1 661 2 States 1
662 3 x1=1; 662 3 x1=1;
663 4 Ok 663 4 Ok
664 5 Witnesses 664 5 Witnesses
665 6 Positive: 2 Negative: 0 665 6 Positive: 2 Negative: 0
666 7 Condition exists (x1=1) 666 7 Condition exists (x1=1)
667 8 Observation C-SB+l-o-o-u+l-o-o-u-X Always 2 667 8 Observation C-SB+l-o-o-u+l-o-o-u-X Always 2 0
668 9 Time C-SB+l-o-o-u+l-o-o-u-X 0.04 668 9 Time C-SB+l-o-o-u+l-o-o-u-X 0.04
669 10 Hash=080bc508da7f291e122c6de76c0088e3 669 10 Hash=080bc508da7f291e122c6de76c0088e3
670 670
671 Line 3 shows that there is one execution that 671 Line 3 shows that there is one execution that did not get filtered out,
672 so the "filter" clause is evaluated only on th 672 so the "filter" clause is evaluated only on the last assignment to
673 the variables that it checks. In this case, t 673 the variables that it checks. In this case, the "filter" clause is a
674 disjunction, so it might be evaluated twice, o 674 disjunction, so it might be evaluated twice, once at the final (and only)
675 assignment to "0:r2" and once at the final ass 675 assignment to "0:r2" and once at the final assignment to "1:r2".
676 676
677 677
678 Linked Lists 678 Linked Lists
679 ------------ 679 ------------
680 680
681 LKMM can handle linked lists, but only linked 681 LKMM can handle linked lists, but only linked lists in which each node
682 contains nothing except a pointer to the next 682 contains nothing except a pointer to the next node in the list. This is
683 of course quite restrictive, but there is neve 683 of course quite restrictive, but there is nevertheless quite a bit that
684 can be done within these confines, as can be s 684 can be done within these confines, as can be seen in the litmus test
685 at tools/memory-model/litmus-tests/MP+onceassi 685 at tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus:
686 686
687 1 C MP+onceassign+derefonce 687 1 C MP+onceassign+derefonce
688 2 688 2
689 3 { 689 3 {
690 4 y=z; 690 4 y=z;
691 5 z=0; 691 5 z=0;
692 6 } 692 6 }
693 7 693 7
694 8 P0(int *x, int **y) 694 8 P0(int *x, int **y)
695 9 { 695 9 {
696 10 WRITE_ONCE(*x, 1); 696 10 WRITE_ONCE(*x, 1);
697 11 rcu_assign_pointer(*y, x); 697 11 rcu_assign_pointer(*y, x);
698 12 } 698 12 }
699 13 699 13
700 14 P1(int *x, int **y) 700 14 P1(int *x, int **y)
701 15 { 701 15 {
702 16 int *r0; 702 16 int *r0;
703 17 int r1; 703 17 int r1;
704 18 704 18
705 19 rcu_read_lock(); 705 19 rcu_read_lock();
706 20 r0 = rcu_dereference(*y); 706 20 r0 = rcu_dereference(*y);
707 21 r1 = READ_ONCE(*r0); 707 21 r1 = READ_ONCE(*r0);
708 22 rcu_read_unlock(); 708 22 rcu_read_unlock();
709 23 } 709 23 }
710 24 710 24
711 25 exists (1:r0=x /\ 1:r1=0) 711 25 exists (1:r0=x /\ 1:r1=0)
712 712
713 Line 4's "y=z" may seem odd, given that "z" ha 713 Line 4's "y=z" may seem odd, given that "z" has not yet been initialized.
714 But "y=z" does not set the value of "y" to tha 714 But "y=z" does not set the value of "y" to that of "z", but instead
715 sets the value of "y" to the *address* of "z". 715 sets the value of "y" to the *address* of "z". Lines 4 and 5 therefore
716 create a simple linked list, with "y" pointing 716 create a simple linked list, with "y" pointing to "z" and "z" having a
717 NULL pointer. A much longer linked list could 717 NULL pointer. A much longer linked list could be created if desired,
718 and circular singly linked lists can also be c 718 and circular singly linked lists can also be created and manipulated.
719 719
720 The "exists" clause works the same way, with t 720 The "exists" clause works the same way, with the "1:r0=x" comparing P1()'s
721 "r0" not to the value of "x", but again to its 721 "r0" not to the value of "x", but again to its address. This term of the
722 "exists" clause therefore tests whether line 2 722 "exists" clause therefore tests whether line 20's load from "y" saw the
723 value stored by line 11, which is in fact what 723 value stored by line 11, which is in fact what is required in this case.
724 724
725 P0()'s line 10 initializes "x" to the value 1 725 P0()'s line 10 initializes "x" to the value 1 then line 11 links to "x"
726 from "y", replacing "z". 726 from "y", replacing "z".
727 727
728 P1()'s line 20 loads a pointer from "y", and l 728 P1()'s line 20 loads a pointer from "y", and line 21 dereferences that
729 pointer. The RCU read-side critical section s 729 pointer. The RCU read-side critical section spanning lines 19-22 is just
730 for show in this example. Note that the addre 730 for show in this example. Note that the address used for line 21's load
731 depends on (in this case, "is exactly the same 731 depends on (in this case, "is exactly the same as") the value loaded by
732 line 20. This is an example of what is called 732 line 20. This is an example of what is called an "address dependency".
733 This particular address dependency extends fro 733 This particular address dependency extends from the load on line 20 to the
734 load on line 21. Address dependencies provide 734 load on line 21. Address dependencies provide a weak form of ordering.
735 735
736 Running this test results in the following: 736 Running this test results in the following:
737 737
738 1 Test MP+onceassign+derefonce Allowed 738 1 Test MP+onceassign+derefonce Allowed
739 2 States 2 739 2 States 2
740 3 1:r0=x; 1:r1=1; 740 3 1:r0=x; 1:r1=1;
741 4 1:r0=z; 1:r1=0; 741 4 1:r0=z; 1:r1=0;
742 5 No 742 5 No
743 6 Witnesses 743 6 Witnesses
744 7 Positive: 0 Negative: 2 744 7 Positive: 0 Negative: 2
745 8 Condition exists (1:r0=x /\ 1:r1=0) 745 8 Condition exists (1:r0=x /\ 1:r1=0)
746 9 Observation MP+onceassign+derefonce Never 0 746 9 Observation MP+onceassign+derefonce Never 0 2
747 10 Time MP+onceassign+derefonce 0.00 747 10 Time MP+onceassign+derefonce 0.00
748 11 Hash=49ef7a741563570102448a256a0c8568 748 11 Hash=49ef7a741563570102448a256a0c8568
749 749
750 The only possible outcomes feature P1() loadin 750 The only possible outcomes feature P1() loading a pointer to "z"
751 (which contains zero) on the one hand and P1() 751 (which contains zero) on the one hand and P1() loading a pointer to "x"
752 (which contains the value one) on the other. 752 (which contains the value one) on the other. This should be reassuring
753 because it says that RCU readers cannot see th 753 because it says that RCU readers cannot see the old preinitialization
754 values when accessing a newly inserted list no 754 values when accessing a newly inserted list node. This undesirable
755 scenario is flagged by the "exists" clause, an 755 scenario is flagged by the "exists" clause, and would occur if P1()
756 loaded a pointer to "x", but obtained the pre- 756 loaded a pointer to "x", but obtained the pre-initialization value of
757 zero after dereferencing that pointer. 757 zero after dereferencing that pointer.
758 758
759 759
760 Comments 760 Comments
761 -------- 761 --------
762 762
763 Different portions of a litmus test are proces 763 Different portions of a litmus test are processed by different parsers,
764 which has the charming effect of requiring dif 764 which has the charming effect of requiring different comment syntax in
765 different portions of the litmus test. The C- 765 different portions of the litmus test. The C-syntax portions use
766 C-language comments (either "/* */" or "//"), 766 C-language comments (either "/* */" or "//"), while the other portions
767 use Ocaml comments "(* *)". 767 use Ocaml comments "(* *)".
768 768
769 The following litmus test illustrates the comm 769 The following litmus test illustrates the comment style corresponding
770 to each syntactic unit of the test: 770 to each syntactic unit of the test:
771 771
772 1 C MP+onceassign+derefonce (* A *) 772 1 C MP+onceassign+derefonce (* A *)
773 2 773 2
774 3 (* B *) 774 3 (* B *)
775 4 775 4
776 5 { 776 5 {
777 6 y=z; (* C *) 777 6 y=z; (* C *)
778 7 z=0; 778 7 z=0;
779 8 } // D 779 8 } // D
780 9 780 9
781 10 // E 781 10 // E
782 11 782 11
783 12 P0(int *x, int **y) // F 783 12 P0(int *x, int **y) // F
784 13 { 784 13 {
785 14 WRITE_ONCE(*x, 1); // G 785 14 WRITE_ONCE(*x, 1); // G
786 15 rcu_assign_pointer(*y, x); 786 15 rcu_assign_pointer(*y, x);
787 16 } 787 16 }
788 17 788 17
789 18 // H 789 18 // H
790 19 790 19
791 20 P1(int *x, int **y) 791 20 P1(int *x, int **y)
792 21 { 792 21 {
793 22 int *r0; 793 22 int *r0;
794 23 int r1; 794 23 int r1;
795 24 795 24
796 25 rcu_read_lock(); 796 25 rcu_read_lock();
797 26 r0 = rcu_dereference(*y); 797 26 r0 = rcu_dereference(*y);
798 27 r1 = READ_ONCE(*r0); 798 27 r1 = READ_ONCE(*r0);
799 28 rcu_read_unlock(); 799 28 rcu_read_unlock();
800 29 } 800 29 }
801 30 801 30
802 31 // I 802 31 // I
803 32 803 32
804 33 exists (* J *) (1:r0=x /\ (* K *) 1:r1=0) ( 804 33 exists (* J *) (1:r0=x /\ (* K *) 1:r1=0) (* L *)
805 805
806 In short, use C-language comments in the C cod 806 In short, use C-language comments in the C code and Ocaml comments in
807 the rest of the litmus test. 807 the rest of the litmus test.
808 808
809 On the other hand, if you prefer C-style comme 809 On the other hand, if you prefer C-style comments everywhere, the
810 C preprocessor is your friend. 810 C preprocessor is your friend.
811 811
812 812
813 Asynchronous RCU Grace Periods 813 Asynchronous RCU Grace Periods
814 ------------------------------ 814 ------------------------------
815 815
816 The following litmus test is derived from the 816 The following litmus test is derived from the example show in
817 Documentation/litmus-tests/rcu/RCU+sync+free.l 817 Documentation/litmus-tests/rcu/RCU+sync+free.litmus, but converted to
818 emulate call_rcu(): 818 emulate call_rcu():
819 819
820 1 C RCU+sync+free 820 1 C RCU+sync+free
821 2 821 2
822 3 { 822 3 {
823 4 int x = 1; 823 4 int x = 1;
824 5 int *y = &x; 824 5 int *y = &x;
825 6 int z = 1; 825 6 int z = 1;
826 7 } 826 7 }
827 8 827 8
828 9 P0(int *x, int *z, int **y) 828 9 P0(int *x, int *z, int **y)
829 10 { 829 10 {
830 11 int *r0; 830 11 int *r0;
831 12 int r1; 831 12 int r1;
832 13 832 13
833 14 rcu_read_lock(); 833 14 rcu_read_lock();
834 15 r0 = rcu_dereference(*y); 834 15 r0 = rcu_dereference(*y);
835 16 r1 = READ_ONCE(*r0); 835 16 r1 = READ_ONCE(*r0);
836 17 rcu_read_unlock(); 836 17 rcu_read_unlock();
837 18 } 837 18 }
838 19 838 19
839 20 P1(int *z, int **y, int *c) 839 20 P1(int *z, int **y, int *c)
840 21 { 840 21 {
841 22 rcu_assign_pointer(*y, z); 841 22 rcu_assign_pointer(*y, z);
842 23 smp_store_release(*c, 1); // Emulate call 842 23 smp_store_release(*c, 1); // Emulate call_rcu().
843 24 } 843 24 }
844 25 844 25
845 26 P2(int *x, int *z, int **y, int *c) 845 26 P2(int *x, int *z, int **y, int *c)
846 27 { 846 27 {
847 28 int r0; 847 28 int r0;
848 29 848 29
849 30 r0 = smp_load_acquire(*c); // Note call_r 849 30 r0 = smp_load_acquire(*c); // Note call_rcu() request.
850 31 synchronize_rcu(); // Wait one grace peri 850 31 synchronize_rcu(); // Wait one grace period.
851 32 WRITE_ONCE(*x, 0); // Emulate the RCU cal 851 32 WRITE_ONCE(*x, 0); // Emulate the RCU callback.
852 33 } 852 33 }
853 34 853 34
854 35 filter (2:r0=1) (* Reject too-early starts. 854 35 filter (2:r0=1) (* Reject too-early starts. *)
855 36 exists (0:r0=x /\ 0:r1=0) 855 36 exists (0:r0=x /\ 0:r1=0)
856 856
857 Lines 4-6 initialize a linked list headed by " 857 Lines 4-6 initialize a linked list headed by "y" that initially contains
858 "x". In addition, "z" is pre-initialized to p 858 "x". In addition, "z" is pre-initialized to prepare for P1(), which
859 will replace "x" with "z" in this list. 859 will replace "x" with "z" in this list.
860 860
861 P0() on lines 9-18 enters an RCU read-side cri 861 P0() on lines 9-18 enters an RCU read-side critical section, loads the
862 list header "y" and dereferences it, leaving t 862 list header "y" and dereferences it, leaving the node in "0:r0" and
863 the node's value in "0:r1". 863 the node's value in "0:r1".
864 864
865 P1() on lines 20-24 updates the list header to 865 P1() on lines 20-24 updates the list header to instead reference "z",
866 then emulates call_rcu() by doing a release st 866 then emulates call_rcu() by doing a release store into "c".
867 867
868 P2() on lines 27-33 emulates the behind-the-sc 868 P2() on lines 27-33 emulates the behind-the-scenes effect of doing a
869 call_rcu(). Line 30 first does an acquire loa 869 call_rcu(). Line 30 first does an acquire load from "c", then line 31
870 waits for an RCU grace period to elapse, and f 870 waits for an RCU grace period to elapse, and finally line 32 emulates
871 the RCU callback, which in turn emulates a cal 871 the RCU callback, which in turn emulates a call to kfree().
872 872
873 Of course, it is possible for P2() to start to 873 Of course, it is possible for P2() to start too soon, so that the
874 value of "2:r0" is zero rather than the requir 874 value of "2:r0" is zero rather than the required value of "1".
875 The "filter" clause on line 35 handles this po 875 The "filter" clause on line 35 handles this possibility, rejecting
876 all executions in which "2:r0" is not equal to 876 all executions in which "2:r0" is not equal to the value "1".
877 877
878 878
879 Performance 879 Performance
880 ----------- 880 -----------
881 881
882 LKMM's exploration of the full state-space can 882 LKMM's exploration of the full state-space can be extremely helpful,
883 but it does not come for free. The price is e 883 but it does not come for free. The price is exponential computational
884 complexity in terms of the number of processes 884 complexity in terms of the number of processes, the average number
885 of statements in each process, and the total n 885 of statements in each process, and the total number of stores in the
886 litmus test. 886 litmus test.
887 887
888 So it is best to start small and then work up. 888 So it is best to start small and then work up. Where possible, break
889 your code down into small pieces each represen 889 your code down into small pieces each representing a core concurrency
890 requirement. 890 requirement.
891 891
892 That said, herd7 is quite fast. On an unprepo 892 That said, herd7 is quite fast. On an unprepossessing x86 laptop, it
893 was able to analyze the following 10-process R 893 was able to analyze the following 10-process RCU litmus test in about
894 six seconds. 894 six seconds.
895 895
896 https://github.com/paulmckrcu/litmus/blob/mast 896 https://github.com/paulmckrcu/litmus/blob/master/auto/C-RW-R+RW-R+RW-G+RW-G+RW-G+RW-G+RW-R+RW-R+RW-R+RW-R.litmus
897 897
898 One way to make herd7 run faster is to use the 898 One way to make herd7 run faster is to use the "-speedcheck true" option.
899 This option prevents herd7 from generating all 899 This option prevents herd7 from generating all possible end states,
900 instead causing it to focus solely on whether 900 instead causing it to focus solely on whether or not the "exists"
901 clause can be satisfied. With this option, he 901 clause can be satisfied. With this option, herd7 evaluates the above
902 litmus test in about 300 milliseconds, for mor 902 litmus test in about 300 milliseconds, for more than an order of magnitude
903 improvement in performance. 903 improvement in performance.
904 904
905 Larger 16-process litmus tests that would norm 905 Larger 16-process litmus tests that would normally consume 15 minutes
906 of time complete in about 40 seconds with this 906 of time complete in about 40 seconds with this option. To be fair,
907 you do get an extra 65,535 states when you lea 907 you do get an extra 65,535 states when you leave off the "-speedcheck
908 true" option. 908 true" option.
909 909
910 https://github.com/paulmckrcu/litmus/blob/mast 910 https://github.com/paulmckrcu/litmus/blob/master/auto/C-RW-R+RW-R+RW-G+RW-G+RW-G+RW-G+RW-R+RW-R+RW-R+RW-R+RW-G+RW-G+RW-G+RW-G+RW-R+RW-R.litmus
911 911
912 Nevertheless, litmus-test analysis really is o 912 Nevertheless, litmus-test analysis really is of exponential complexity,
913 whether with or without "-speedcheck true". I 913 whether with or without "-speedcheck true". Increasing by just three
914 processes to a 19-process litmus test requires 914 processes to a 19-process litmus test requires 2 hours and 40 minutes
915 without, and about 8 minutes with "-speedcheck 915 without, and about 8 minutes with "-speedcheck true". Each of these
916 results represent roughly an order of magnitud 916 results represent roughly an order of magnitude slowdown compared to the
917 16-process litmus test. Again, to be fair, th 917 16-process litmus test. Again, to be fair, the multi-hour run explores
918 no fewer than 524,287 additional states compar 918 no fewer than 524,287 additional states compared to the shorter one.
919 919
920 https://github.com/paulmckrcu/litmus/blob/mast 920 https://github.com/paulmckrcu/litmus/blob/master/auto/C-RW-R+RW-R+RW-G+RW-G+RW-G+RW-G+RW-R+RW-R+RW-R+RW-R+RW-R+RW-R+RW-G+RW-G+RW-G+RW-G+RW-R+RW-R+RW-R.litmus
921 921
922 If you don't like command-line arguments, you 922 If you don't like command-line arguments, you can obtain a similar speedup
923 by adding a "filter" clause with exactly the s 923 by adding a "filter" clause with exactly the same expression as your
924 "exists" clause. 924 "exists" clause.
925 925
926 However, please note that seeing the full set 926 However, please note that seeing the full set of states can be extremely
927 helpful when developing and debugging litmus t 927 helpful when developing and debugging litmus tests.
928 928
929 929
930 LIMITATIONS 930 LIMITATIONS
931 =========== 931 ===========
932 932
933 Limitations of the Linux-kernel memory model ( 933 Limitations of the Linux-kernel memory model (LKMM) include:
934 934
935 1. Compiler optimizations are not accurat 935 1. Compiler optimizations are not accurately modeled. Of course,
936 the use of READ_ONCE() and WRITE_ONCE( 936 the use of READ_ONCE() and WRITE_ONCE() limits the compiler's
937 ability to optimize, but under some ci 937 ability to optimize, but under some circumstances it is possible
938 for the compiler to undermine the memo 938 for the compiler to undermine the memory model. For more
939 information, see Documentation/explana 939 information, see Documentation/explanation.txt (in particular,
940 the "THE PROGRAM ORDER RELATION: po AN 940 the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING"
941 sections). 941 sections).
942 942
943 Note that this limitation in turn limi 943 Note that this limitation in turn limits LKMM's ability to
944 accurately model address, control, and 944 accurately model address, control, and data dependencies.
945 For example, if the compiler can deduc 945 For example, if the compiler can deduce the value of some variable
946 carrying a dependency, then the compil 946 carrying a dependency, then the compiler can break that dependency
947 by substituting a constant of that val 947 by substituting a constant of that value.
948 948
949 Conversely, LKMM will sometimes overes 949 Conversely, LKMM will sometimes overestimate the amount of
950 reordering compilers and CPUs can carr 950 reordering compilers and CPUs can carry out, leading it to miss
951 some pretty obvious cases of ordering. 951 some pretty obvious cases of ordering. A simple example is:
952 952
953 r1 = READ_ONCE(x); 953 r1 = READ_ONCE(x);
954 if (r1 == 0) 954 if (r1 == 0)
955 smp_mb(); 955 smp_mb();
956 WRITE_ONCE(y, 1); 956 WRITE_ONCE(y, 1);
957 957
958 The WRITE_ONCE() does not depend on th 958 The WRITE_ONCE() does not depend on the READ_ONCE(), and as a
959 result, LKMM does not claim ordering. 959 result, LKMM does not claim ordering. However, even though no
960 dependency is present, the WRITE_ONCE( 960 dependency is present, the WRITE_ONCE() will not be executed before
961 the READ_ONCE(). There are two reason 961 the READ_ONCE(). There are two reasons for this:
962 962
963 The presence of the smp_mb() i 963 The presence of the smp_mb() in one of the branches
964 prevents the compiler from mov 964 prevents the compiler from moving the WRITE_ONCE()
965 up before the "if" statement, 965 up before the "if" statement, since the compiler has
966 to assume that r1 will sometim 966 to assume that r1 will sometimes be 0 (but see the
967 comment below); 967 comment below);
968 968
969 CPUs do not execute stores bef 969 CPUs do not execute stores before po-earlier conditional
970 branches, even in cases where 970 branches, even in cases where the store occurs after the
971 two arms of the branch have re 971 two arms of the branch have recombined.
972 972
973 It is clear that it is not dangerous i 973 It is clear that it is not dangerous in the slightest for LKMM to
974 make weaker guarantees than architectu 974 make weaker guarantees than architectures. In fact, it is
975 desirable, as it gives compilers room 975 desirable, as it gives compilers room for making optimizations.
976 For instance, suppose that a 0 value i 976 For instance, suppose that a 0 value in r1 would trigger undefined
977 behavior elsewhere. Then a clever com 977 behavior elsewhere. Then a clever compiler might deduce that r1
978 can never be 0 in the if condition. A 978 can never be 0 in the if condition. As a result, said clever
979 compiler might deem it safe to optimiz 979 compiler might deem it safe to optimize away the smp_mb(),
980 eliminating the branch and any orderin 980 eliminating the branch and any ordering an architecture would
981 guarantee otherwise. 981 guarantee otherwise.
982 982
983 2. Multiple access sizes for a single var 983 2. Multiple access sizes for a single variable are not supported,
984 and neither are misaligned or partiall 984 and neither are misaligned or partially overlapping accesses.
985 985
986 3. Exceptions and interrupts are not mode 986 3. Exceptions and interrupts are not modeled. In some cases,
987 this limitation can be overcome by mod 987 this limitation can be overcome by modeling the interrupt or
988 exception with an additional process. 988 exception with an additional process.
989 989
990 4. I/O such as MMIO or DMA is not support 990 4. I/O such as MMIO or DMA is not supported.
991 991
992 5. Self-modifying code (such as that foun 992 5. Self-modifying code (such as that found in the kernel's
993 alternatives mechanism, function trace 993 alternatives mechanism, function tracer, Berkeley Packet Filter
994 JIT compiler, and module loader) is no 994 JIT compiler, and module loader) is not supported.
995 995
996 6. Complete modeling of all variants of a 996 6. Complete modeling of all variants of atomic read-modify-write
997 operations, locking primitives, and RC 997 operations, locking primitives, and RCU is not provided.
998 For example, call_rcu() and rcu_barrie 998 For example, call_rcu() and rcu_barrier() are not supported.
999 However, a substantial amount of suppo 999 However, a substantial amount of support is provided for these
1000 operations, as shown in the linux-ker 1000 operations, as shown in the linux-kernel.def file.
1001 1001
1002 Here are specific limitations: 1002 Here are specific limitations:
1003 1003
1004 a. When rcu_assign_pointer() is 1004 a. When rcu_assign_pointer() is passed NULL, the Linux
1005 kernel provides no ordering, 1005 kernel provides no ordering, but LKMM models this
1006 case as a store release. 1006 case as a store release.
1007 1007
1008 b. The "unless" RMW operations a 1008 b. The "unless" RMW operations are not currently modeled:
1009 atomic_long_add_unless(), ato 1009 atomic_long_add_unless(), atomic_inc_unless_negative(),
1010 and atomic_dec_unless_positiv 1010 and atomic_dec_unless_positive(). These can be emulated
1011 in litmus tests, for example, 1011 in litmus tests, for example, by using atomic_cmpxchg().
1012 1012
1013 One exception of this limitat 1013 One exception of this limitation is atomic_add_unless(),
1014 which is provided directly by 1014 which is provided directly by herd7 (so no corresponding
1015 definition in linux-kernel.de 1015 definition in linux-kernel.def). atomic_add_unless() is
1016 modeled by herd7 therefore it 1016 modeled by herd7 therefore it can be used in litmus tests.
1017 1017
1018 c. The call_rcu() function is no 1018 c. The call_rcu() function is not modeled. As was shown above,
1019 it can be emulated in litmus 1019 it can be emulated in litmus tests by adding another
1020 process that invokes synchron 1020 process that invokes synchronize_rcu() and the body of the
1021 callback function, with (for 1021 callback function, with (for example) a release-acquire
1022 from the site of the emulated 1022 from the site of the emulated call_rcu() to the beginning
1023 of the additional process. 1023 of the additional process.
1024 1024
1025 d. The rcu_barrier() function is 1025 d. The rcu_barrier() function is not modeled. It can be
1026 emulated in litmus tests emul 1026 emulated in litmus tests emulating call_rcu() via
1027 (for example) a release-acqui 1027 (for example) a release-acquire from the end of each
1028 additional call_rcu() process 1028 additional call_rcu() process to the site of the
1029 emulated rcu-barrier(). 1029 emulated rcu-barrier().
1030 1030
1031 e. Reader-writer locking is not 1031 e. Reader-writer locking is not modeled. It can be
1032 emulated in litmus tests usin 1032 emulated in litmus tests using atomic read-modify-write
1033 operations. 1033 operations.
1034 1034
1035 The fragment of the C language supported by t 1035 The fragment of the C language supported by these litmus tests is quite
1036 limited and in some ways non-standard: 1036 limited and in some ways non-standard:
1037 1037
1038 1. There is no automatic C-preprocessor 1038 1. There is no automatic C-preprocessor pass. You can of course
1039 run it manually, if you choose. 1039 run it manually, if you choose.
1040 1040
1041 2. There is no way to create functions o 1041 2. There is no way to create functions other than the Pn() functions
1042 that model the concurrent processes. 1042 that model the concurrent processes.
1043 1043
1044 3. The Pn() functions' formal parameters 1044 3. The Pn() functions' formal parameters must be pointers to the
1045 global shared variables. Nothing can 1045 global shared variables. Nothing can be passed by value into
1046 these functions. 1046 these functions.
1047 1047
1048 4. The only functions that can be invoke 1048 4. The only functions that can be invoked are those built directly
1049 into herd7 or that are defined in the 1049 into herd7 or that are defined in the linux-kernel.def file.
1050 1050
1051 5. The "switch", "do", "for", "while", a 1051 5. The "switch", "do", "for", "while", and "goto" C statements are
1052 not supported. The "switch" statemen 1052 not supported. The "switch" statement can be emulated by the
1053 "if" statement. The "do", "for", and 1053 "if" statement. The "do", "for", and "while" statements can
1054 often be emulated by manually unrolli 1054 often be emulated by manually unrolling the loop, or perhaps by
1055 enlisting the aid of the C preprocess 1055 enlisting the aid of the C preprocessor to minimize the resulting
1056 code duplication. Some uses of "goto 1056 code duplication. Some uses of "goto" can be emulated by "if",
1057 and some others by unrolling. 1057 and some others by unrolling.
1058 1058
1059 6. Although you can use a wide variety o 1059 6. Although you can use a wide variety of types in litmus-test
1060 variable declarations, and especially 1060 variable declarations, and especially in global-variable
1061 declarations, the "herd7" tool unders 1061 declarations, the "herd7" tool understands only int and
1062 pointer types. There is no support f 1062 pointer types. There is no support for floating-point types,
1063 enumerations, characters, strings, ar 1063 enumerations, characters, strings, arrays, or structures.
1064 1064
1065 7. Parsing of variable declarations is v 1065 7. Parsing of variable declarations is very loose, with almost no
1066 type checking. 1066 type checking.
1067 1067
1068 8. Initializers differ from their C-lang 1068 8. Initializers differ from their C-language counterparts.
1069 For example, when an initializer cont 1069 For example, when an initializer contains the name of a shared
1070 variable, that name denotes a pointer 1070 variable, that name denotes a pointer to that variable, not
1071 the current value of that variable. 1071 the current value of that variable. For example, "int x = y"
1072 is interpreted the way "int x = &y" w 1072 is interpreted the way "int x = &y" would be in C.
1073 1073
1074 9. Dynamic memory allocation is not supp 1074 9. Dynamic memory allocation is not supported, although this can
1075 be worked around in some cases by sup 1075 be worked around in some cases by supplying multiple statically
1076 allocated variables. 1076 allocated variables.
1077 1077
1078 Some of these limitations may be overcome in 1078 Some of these limitations may be overcome in the future, but others are
1079 more likely to be addressed by incorporating 1079 more likely to be addressed by incorporating the Linux-kernel memory model
1080 into other tools. 1080 into other tools.
1081 1081
1082 Finally, please note that LKMM is subject to 1082 Finally, please note that LKMM is subject to change as hardware, use cases,
1083 and compilers evolve. 1083 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.