Lines Matching +full:1 +full:- +full:to +full:- +full:1
1 Linux-Kernel Memory Model Litmus Tests
4 This file describes the LKMM litmus-test format by example, describes
9 A formal kernel memory-ordering model (part 2)
20 tool, please see tools/memory-model/README.
23 Copy-Pasta
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 from scratch. A number
30 tools/memory-model/litmus-tests/
31 Documentation/litmus-tests/
40 The -l and -L arguments to "git grep" can be quite helpful in identifying
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 still helpful to have a
43 good understanding of the litmus-test format.
50 with a small example of the message-passing pattern and moving on to
52 minimalistic set of flow-control statements.
55 Message-Passing Example
56 -----------------------
59 example based on the common message-passing use case. This use case
63 flag set, but, due to memory misordering, saw old values in the buffer.
66 suffices to avoid this bad outcome:
68 1 C MP+pooncerelease+poacquireonce
74 7 WRITE_ONCE(*x, 1);
75 8 smp_store_release(y, 1);
87 20 exists (1:r0=1 /\ 1:r1=0)
89 Line 1 starts with "C", which identifies this file as being in the
90 LKMM C-language format (which, as we will see, is a small fragment
91 of the full C language). The remainder of line 1 is the name of
94 tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
95 in the Linux-kernel source tree.
98 double-quoted comment string on the second line. Such strings are ignored
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 use of multiple parsers.
101 For now, you can use C-language comments in the C code, and these comments
103 cover the full litmus-test commenting story.
106 to zero suffices for this test, the "{}" syntax is used, which mean the
107 initialization section is empty. Litmus tests requiring non-default
108 initialization must have non-empty initialization sections, as in the
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 kthread, workqueue, thread,
119 must contain a two-process litmus test.
121 The argument list for each function are pointers to the global variables
122 used by that function. Unlike normal C-language function parameters, the
127 variables, "x" and "y". Global variables are always passed to processes
132 other litmus-test formats, it is conventional to use names consisting of
134 is forgetting to add a global variable to a process's parameter list.
136 intended global to instead be silently treated as an undeclared local
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 Linux kernel's atomic
141 operations, some of its exclusive-lock functions, and some of its RCU
143 functions may be found in the linux-kernel.def file.
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 unordered store to global
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 release store to global
158 Line 20 is the "exists" assertion expression to evaluate the final state.
161 have propagated to all parts of the system. The references to the local
162 variables "r0" and "r1" in line 24 must be prefixed with "1:" to specify
163 which process they are local to.
165 Note that the assertion expression is written in the litmus-test
168 "and". Similarly, "\/" stands for "or". Both of these are ASCII-art
170 "~" stands for "logical not", which is "!" in C, and not to be confused
171 with the C-language "~" operator which instead stands for "bitwise not".
172 Parentheses may be used to override precedence.
176 loaded a value from "x" that was equal to 1 but loaded a value from "y"
177 that was still equal to zero.
180 absolutely must be run from the tools/memory-model directory and from
183 herd7 -conf linux-kernel.cfg litmus-tests/MP+pooncerelease+poacquireonce.litmus
185 The output is the result of something similar to a full state-space
188 1 Test MP+pooncerelease+poacquireonce Allowed
190 3 1:r0=0; 1:r1=0;
191 4 1:r0=0; 1:r1=1;
192 5 1:r0=1; 1:r1=1;
196 9 Condition exists (1:r0=1 /\ 1:r1=0)
203 happens. This line might instead say "Sometimes" to indicate that the
205 "Always" to indicate that the bad result happened in all executions.
207 "exists" clause indicates a bad result. To see this, invert the "exists"
212 Another important part of this output is shown in lines 2-5, repeated here:
215 3 1:r0=0; 1:r1=0;
216 4 1:r0=0; 1:r1=1;
217 5 1:r0=1; 1:r1=1;
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; 1:r1=0;") indicating that
226 The rest of the output is not normally needed, either due to irrelevance
227 or due to being redundant with the lines discussed above. However, the
229 an insatiable curiosity. Other readers should feel free to skip ahead.
231 Line 1 echos the test name, along with the "Test" and "Allowed". Line 6's
234 lead-in to line 8's "Positive: 0 Negative: 3", which lists the number
237 clause so that you don't have to look it up in the litmus-test file.
239 time in seconds required to analyze the litmus test. Small tests such
241 Line 12 gives a hash of the contents for the litmus-test file, and is used
245 affected by a given change to LKMM.
249 --------------
253 to some other value:
255 1 C MP+pooncerelease+poacquireonce
264 10 WRITE_ONCE(*x, 1);
265 11 smp_store_release(y, 1);
277 23 exists (1:r0=1 /\ 1:r1=42)
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 change "1:r1=0" to
281 "1:r1=42".
286 1 Test MP+pooncerelease+poacquireonce Allowed
288 3 1:r0=1; 1:r1=1;
289 4 1:r0=42; 1:r1=1;
290 5 1:r0=42; 1:r1=42;
294 9 Condition exists (1:r0=1 /\ 1:r1=42)
299 It is tempting to avoid the open-coded repetitions of the value "42"
302 initialize "x" and "y" to 42, but instead to the address of "initval"
303 (try it!). See the section below on linked lists to learn more about
304 why this approach to initialization can be useful.
308 ------------------
310 LKMM supports the C-language "if" statement, which allows modeling of
313 to optimize away conditional branches). The following example shows
314 the "load buffering" (LB) use case that is used in the Linux kernel to
315 synchronize between ring-buffer producers and consumers. In the example
316 below, P0() is one side checking to see if an operation may proceed and
319 1 C LB+fencembonceonce+ctrlonceonce
329 11 WRITE_ONCE(*y, 1);
338 20 WRITE_ONCE(*x, 1);
341 23 exists (0:r0=1 /\ 1:r0=1)
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 read from "y", one would
348 1 Test LB+fencembonceonce+ctrlonceonce Allowed
350 3 0:r0=0; 1:r0=0;
351 4 0:r0=1; 1:r0=0;
355 8 Condition exists (0:r0=1 /\ 1:r0=1)
360 However, there is no "while" statement due to the fact that full
361 state-space search has some difficulty with iteration. However, there
362 are tricks that may be used to handle some special cases, which are
363 discussed below. In addition, loop-unrolling tricks may be applied,
371 spin loops, handling trivial linked lists, adding comments to litmus tests,
372 emulating call_rcu(), and finally tricks to improve herd7 performance
373 in order to better handle large litmus tests.
377 ------------
382 (tools/memory-order/litmus-tests/SB+rfionceonce-poonceonces.litmus but
386 1 C SB+rfionceonce-poonceonces
395 10 WRITE_ONCE(*x, 1);
405 20 WRITE_ONCE(*y, 1);
410 25 exists (0:r2=0 /\ 1:r4=0)
414 1 Test SB+rfionceonce-poonceonces Allowed
416 3 0:r2=0; 1:r4=0;
417 4 0:r2=0; 1:r4=1;
418 5 0:r2=1; 1:r4=0;
419 6 0:r2=1; 1:r4=1;
422 9 Positive: 1 Negative: 3
423 10 Condition exists (0:r2=0 /\ 1:r4=0)
424 11 Observation SB+rfionceonce-poonceonces Sometimes 1 3
425 12 Time SB+rfionceonce-poonceonces 0.01
428 (This output indicates that CPUs are permitted to "snoop their own
434 "exists" clause. Someone modifying this test might wish to know the
436 statement on line 25 shows how to cause herd7 to display additional
439 1 C SB+rfionceonce-poonceonces
448 10 WRITE_ONCE(*x, 1);
458 20 WRITE_ONCE(*y, 1);
463 25 locations [0:r1; 1:r3; x; y]
464 26 exists (0:r2=0 /\ 1:r4=0)
468 1 Test SB+rfionceonce-poonceonces Allowed
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;
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;
476 9 Positive: 1 Negative: 3
477 10 Condition exists (0:r2=0 /\ 1:r4=0)
478 11 Observation SB+rfionceonce-poonceonces Sometimes 1 3
479 12 Time SB+rfionceonce-poonceonces 0.01
482 What if you would like to know the value of a particular global variable
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 "locations" clause.
487 the outcome! For one example, please see the C-READ_ONCE.litmus and
488 C-READ_ONCE-omitted.litmus tests located here:
494 ----------
499 Potentially infinite loops, such as those used to wait for locks to
502 Fortunately, it is possible to avoid state-space explosion by specially
505 in a spin loop, it instead excludes executions that fail to acquire the
510 such as emulating reader-writer locking, which LKMM does not yet model.
512 1 C C-SB+l-o-o-u+l-o-o-u-X
522 11 r2 = xchg_acquire(sl, 1);
523 12 WRITE_ONCE(*x0, 1);
533 22 r2 = xchg_acquire(sl, 1);
534 23 WRITE_ONCE(*x1, 1);
539 28 filter (0:r2=0 /\ 1:r2=0)
540 29 exists (0:r1=0 /\ 1:r1=0)
544 …cm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus
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 lock acquisition is emulated
551 "1" to "sl" and stores either "0" or "1" to "r2", depending on whether
552 the lock acquisition was successful or unsuccessful (due to "sl" already
553 having the value "1"), respectively. P1() operates in a similar manner.
555 Rather unconventionally, execution appears to proceed to the critical
557 smp_store_release() to store zero to "sl", thus emulating lock release.
559 The case where xchg_acquire() fails to acquire the lock is handled by
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 zero, that is to pay
562 attention only to those executions in which both locks are actually
567 evaluates to true. In other words, the "filter" clause says what to
568 keep, not what to discard.
572 1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed
574 3 0:r1=0; 1:r1=1;
575 4 0:r1=1; 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 2
581 10 Time C-SB+l-o-o-u+l-o-o-u-X 0.03
587 to handle failed spinlock acquisitions, like the kernel does? The key
589 possible "exists"-clause outcomes of program execution in the absence
590 of deadlock. In other words, given a high-quality lock-acquisition
591 primitive in a deadlock-free program running on high-quality hardware,
593 explores the full state space, the length of time required to actually
597 Why not just add the "filter" clause to the "exists" clause, thus
600 herd7 knows to abandon an execution as soon as the "filter" expression
601 fails to be satisfied. In contrast, the "exists" clause is evaluated
602 only at the end of time, thus requiring herd7 to waste time on bogus
608 free to skip the remainder of this section.
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 the execution prematurely
612 due to an early mismatch of the "filter" clause?
615 introduces a new global variable "x2" that is initialized to "1". Line 23
616 of P1() reads that variable into "1:r2" to force an early mismatch with
617 the "filter" clause. Line 24 does a known-true "if" condition to avoid
619 on line 32 is updated to a condition that is alway satisfied at the end
622 1 C C-SB+l-o-o-u+l-o-o-u-X
625 4 x2=1;
633 12 r2 = xchg_acquire(sl, 1);
634 13 WRITE_ONCE(*x0, 1);
646 25 r2 = xchg_acquire(sl, 1);
647 26 WRITE_ONCE(*x1, 1);
652 31 filter (0:r2=0 /\ 1:r2=0)
653 32 exists (x1=1)
655 If the "filter" clause were to check each variable at each point in the
660 1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed
661 2 States 1
662 3 x1=1;
666 7 Condition exists (x1=1)
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
672 so the "filter" clause is evaluated only on the last assignment to
675 assignment to "0:r2" and once at the final assignment to "1:r2".
679 ------------
682 contains nothing except a pointer to the next node in the list. This is
685 at tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus:
687 1 C MP+onceassign+derefonce
696 10 WRITE_ONCE(*x, 1);
711 25 exists (1:r0=x /\ 1:r1=0)
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". Lines 4 and 5 therefore
716 create a simple linked list, with "y" pointing to "z" and "z" having a
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 address. This term of the
725 P0()'s line 10 initializes "x" to the value 1 then line 11 links to "x"
729 pointer. The RCU read-side critical section spanning lines 19-22 is just
733 This particular address dependency extends from the load on line 20 to the
738 1 Test MP+onceassign+derefonce Allowed
740 3 1:r0=x; 1:r1=1;
741 4 1:r0=z; 1:r1=0;
745 8 Condition exists (1:r0=x /\ 1:r1=0)
750 The only possible outcomes feature P1() loading a pointer to "z"
751 (which contains zero) on the one hand and P1() loading a pointer to "x"
756 loaded a pointer to "x", but obtained the pre-initialization value of
761 --------
765 different portions of the litmus test. The C-syntax portions use
766 C-language comments (either "/* */" or "//"), while the other portions
770 to each syntactic unit of the test:
772 1 C MP+onceassign+derefonce (* A *)
785 14 WRITE_ONCE(*x, 1); // G
804 33 exists (* J *) (1:r0=x /\ (* K *) 1:r1=0) (* L *)
806 In short, use C-language comments in the C code and Ocaml comments in
809 On the other hand, if you prefer C-style comments everywhere, the
814 ------------------------------
817 Documentation/litmus-tests/rcu/RCU+sync+free.litmus, but converted to
820 1 C RCU+sync+free
823 4 int x = 1;
825 6 int z = 1;
842 23 smp_store_release(*c, 1); // Emulate call_rcu().
854 35 filter (2:r0=1) (* Reject too-early starts. *)
857 Lines 4-6 initialize a linked list headed by "y" that initially contains
858 "x". In addition, "z" is pre-initialized to prepare for P1(), which
861 P0() on lines 9-18 enters an RCU read-side critical section, loads the
865 P1() on lines 20-24 updates the list header to instead reference "z",
868 P2() on lines 27-33 emulates the behind-the-scenes effect of doing a
870 waits for an RCU grace period to elapse, and finally line 32 emulates
871 the RCU callback, which in turn emulates a call to kfree().
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 required value of "1".
876 all executions in which "2:r0" is not equal to the value "1".
880 -----------
882 LKMM's exploration of the full state-space can be extremely helpful,
888 So it is best to start small and then work up. Where possible, break
893 was able to analyze the following 10-process RCU litmus test in about
896 …ps://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+…
898 One way to make herd7 run faster is to use the "-speedcheck true" option.
900 instead causing it to focus solely on whether or not the "exists"
905 Larger 16-process litmus tests that would normally consume 15 minutes
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 leave off the "-speedcheck
910 …/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+…
912 Nevertheless, litmus-test analysis really is of exponential complexity,
913 whether with or without "-speedcheck true". Increasing by just three
914 processes to a 19-process litmus test requires 2 hours and 40 minutes
915 without, and about 8 minutes with "-speedcheck true". Each of these
916 results represent roughly an order of magnitude slowdown compared to the
917 16-process litmus test. Again, to be fair, the multi-hour run explores
918 no fewer than 524,287 additional states compared to the shorter one.
920 …rcu/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-…
922 If you don't like command-line arguments, you can obtain a similar speedup
933 Limitations of the Linux-kernel memory model (LKMM) include:
935 1. Compiler optimizations are not accurately modeled. Of course,
937 ability to optimize, but under some circumstances it is possible
938 for the compiler to undermine the memory model. For more
940 the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING"
943 Note that this limitation in turn limits LKMM's ability to
950 reordering compilers and CPUs can carry out, leading it to miss
956 WRITE_ONCE(y, 1);
966 to assume that r1 will sometimes be 0 (but see the
969 CPUs do not execute stores before po-earlier conditional
973 It is clear that it is not dangerous in the slightest for LKMM to
979 compiler might deem it safe to optimize away the smp_mb(),
992 5. Self-modifying code (such as that found in the kernel's
996 6. Complete modeling of all variants of atomic read-modify-write
1000 operations, as shown in the linux-kernel.def file.
1015 definition in linux-kernel.def). atomic_add_unless() is
1021 callback function, with (for example) a release-acquire
1022 from the site of the emulated call_rcu() to the beginning
1027 (for example) a release-acquire from the end of each
1028 additional call_rcu() process to the site of the
1029 emulated rcu-barrier().
1031 e. Reader-writer locking is not modeled. It can be
1032 emulated in litmus tests using atomic read-modify-write
1036 limited and in some ways non-standard:
1038 1. There is no automatic C-preprocessor pass. You can of course
1041 2. There is no way to create functions other than the Pn() functions
1044 3. The Pn() functions' formal parameters must be pointers to the
1049 into herd7 or that are defined in the linux-kernel.def file.
1055 enlisting the aid of the C preprocessor to minimize the resulting
1059 6. Although you can use a wide variety of types in litmus-test
1060 variable declarations, and especially in global-variable
1062 pointer types. There is no support for floating-point types,
1068 8. Initializers differ from their C-language counterparts.
1070 variable, that name denotes a pointer to that variable, not
1079 more likely to be addressed by incorporating the Linux-kernel memory model
1082 Finally, please note that LKMM is subject to change as hardware, use cases,