memory-model/Documentation/litmus-tests.txt

1 Linux-Kernel Memory Model Litmus Tests
4 This file describes the LKMM litmus-test format by example, describes
6 versions of this material appeared in a number of LWN articles, including:
9 	A formal kernel memory-ordering model (part 2)
20 tool, please see tools/memory-model/README.
23 Copy-Pasta
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
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 -----------------------
58 This section gives an overview of the format of a litmus test using an
59 example based on the common message-passing use case.  This use case
60 appears often in the Linux kernel.  For example, a flag (modeled by "y"
61 below) indicates that a buffer (modeled by "x" below) is now completely
76  9 }
87 20 exists (1:r0=1 /\ 1:r1=0)
90 LKMM C-language format (which, as we will see, is a small fragment
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
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
102 may be in either the "/* */" or the "//" style.  A later section will
103 cover the full litmus-test commenting story.
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,
116 of a single "P" followed by a number, and as long as the numbers are
118 for example, a .litmus file matching "^P1(" but not matching "^P2("
119 must contain a two-process litmus test.
122 used by that function.  Unlike normal C-language function parameters, the
123 names are significant.  The fact that both P0() and P1() have a formal
132 other litmus-test formats, it is conventional to use names consisting of
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 process's parameter list.
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
148 is also in P0()'s parameter list, this does a release store to global
153 from global variable "y" into local variable "r0".  Line 17 does a
165 Note that the assertion expression is written in the litmus-test
168 "and".  Similarly, "\/" stands for "or".  Both of these are ASCII-art
171 with the C-language "~" operator which instead stands for "bitwise not".
176 loaded a value from "x" that was equal to 1 but loaded a value from "y"
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
190  3 1:r0=0; 1:r1=0;
191  4 1:r0=0; 1:r1=1;
195  8 Positive: 0 Negative: 3
196  9 Condition exists (1:r0=1 /\ 1:r1=0)
197 10 Observation MP+pooncerelease+poacquireonce Never 0 3
201 The most pertinent line is line 10, which contains "Never 0 3", which
207 "exists" clause indicates a bad result.  To see this, invert the "exists"
208 clause's condition and run the test.)  The numbers ("0 3") at the end
210 clause (0) and the number not not satisfying that clause (3).
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;
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
221 both of P1()'s loads returned the value "0".  As expected, given the
223 listed.  This full list of states can be helpful when debugging a new
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", which lists the number
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 the litmus-test file.
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 litmus-test file, and is used
245 affected by a given change to LKMM.
249 --------------
252 "x" and "y", but a similar litmus test could instead initialize them
263  9 {
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
293  8 Positive: 0 Negative: 3
294  9 Condition exists (1:r0=1 /\ 1:r1=42)
295 10 Observation MP+pooncerelease+poacquireonce Never 0 3
299 It is tempting to avoid the open-coded repetitions of the value "42"
308 ------------------
310 LKMM supports the C-language "if" statement, which allows modeling of
315 synchronize between ring-buffer producers and consumers.  In the example
327  9   r0 = READ_ONCE(*x);
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
350  3 0:r0=0; 1:r0=0;
351  4 0:r0=1; 1:r0=0;
354  7 Positive: 0 Negative: 2
355  8 Condition exists (0:r0=1 /\ 1:r0=1)
356  9 Observation LB+fencembonceonce+ctrlonceonce Never 0 2
361 state-space search has some difficulty with iteration.  However, there
363 discussed below.  In addition, loop-unrolling tricks may be applied,
377 ------------
382 (tools/memory-order/litmus-tests/SB+rfionceonce-poonceonces.litmus but
386  1 C SB+rfionceonce-poonceonces
394  9
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
435 values of "x", "y", "0:r1", and "0:r3" as well.  The "locations"
439  1 C SB+rfionceonce-poonceonces
447  9
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
483 at some particular point in a given process's execution?  One approach
484 is to use a READ_ONCE() to load that global variable into a new local
486 But be careful:  In some litmus tests, adding a READ_ONCE() will change
487 the outcome!  For one example, please see the C-READ_ONCE.litmus and
488 C-READ_ONCE-omitted.litmus tests located here:
494 ----------
498 the amount of code in a give process can greatly increase execution time.
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
506 lock using a herd7 "filter" clause.  Note that for exclusive locking, you
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
520  9   int r1;
525 14   smp_store_release(sl, 0);
536 25   smp_store_release(sl, 0);
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
546 This test uses two global variables, "x1" and "x2", and also emulates a
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
553 having the value "1"), respectively.  P1() operates in a similar manner.
561 executions in which both "0:r2" and "1:r2" are zero, that is to pay
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;
578  7 Positive: 0 Negative: 2
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
583 The "Never" on line 9 indicates that this use of xchg_acquire() and
586 Why doesn't the litmus test take the simpler approach of using a spin loop
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,
607 Readers lacking a pathological interest in odd corner cases should feel
610 But what if the litmus test were to temporarily set "0:r2" to a non-zero
615 introduces a new global variable "x2" that is initialized to "1".  Line 23
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
630  9   int r2;
636 15   smp_store_release(sl, 0);
649 28   smp_store_release(sl, 0);
652 31 filter (0:r2=0 /\ 1:r2=0)
660  1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed
665  6 Positive: 2 Negative: 0
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
673 the variables that it checks.  In this case, the "filter" clause is a
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
683 of course quite restrictive, but there is nevertheless quite a bit that
685 at tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus:
690  4 y=z;
691  5 z=0;
695  9 {
711 25 exists (1:r0=x /\ 1:r1=0)
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 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
717 NULL pointer.  A much longer linked list could be created if desired,
726 from "y", replacing "z".
728 P1()'s line 20 loads a pointer from "y", and line 21 dereferences that
729 pointer.  The RCU read-side critical section spanning lines 19-22 is just
734 load on line 21.  Address dependencies provide a weak form of ordering.
741  4 1:r0=z; 1:r1=0;
744  7 Positive: 0 Negative: 2
745  8 Condition exists (1:r0=x /\ 1:r1=0)
746  9 Observation MP+onceassign+derefonce Never 0 2
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"
754 values when accessing a newly inserted list node.  This undesirable
756 loaded a pointer to "x", but obtained the pre-initialization value of
761 --------
763 Different portions of a litmus test are processed by different parsers,
765 different portions of the litmus test.  The C-syntax portions use
766 C-language comments (either "/* */" or "//"), while the other portions
772  1 C MP+onceassign+derefonce (* A *)
777  6 y=z; (* C *)
778  7 z=0;
780  9
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
825  6 int z = 1;
828  9 P0(int *x, int *z, int **y)
839 20 P1(int *z, int **y, int *c)
841 22   rcu_assign_pointer(*y, z);
845 26 P2(int *x, int *z, int **y, int *c)
851 32   WRITE_ONCE(*x, 0); // Emulate the RCU callback.
854 35 filter (2:r0=1) (* Reject too-early starts. *)
855 36 exists (0:r0=x /\ 0:r1=0)
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
859 will replace "x" with "z" in this list.
861 P0() on lines 9-18 enters an RCU read-side critical section, loads the
862 list header "y" and dereferences it, leaving the node in "0:r0" and
863 the node's value in "0:r1".
865 P1() on lines 20-24 updates the list header to instead reference "z",
866 then emulates call_rcu() by doing a release store into "c".
868 P2() on lines 27-33 emulates the behind-the-scenes effect of doing a
871 the RCU callback, which in turn emulates a call to kfree().
880 -----------
882 LKMM's exploration of the full state-space can be extremely helpful,
889 your code down into small pieces each representing a core concurrency
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.
905 Larger 16-process litmus tests that would normally consume 15 minutes
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
917 16-process litmus test.  Again, to be fair, the multi-hour run explores
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
923 by adding a "filter" clause with exactly the same expression as your
933 Limitations of the Linux-kernel memory model (LKMM) include:
940 	the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING"
946 	carrying a dependency, then the compiler can break that dependency
947 	by substituting a constant of that value.
951 	some pretty obvious cases of ordering.  A simple example is:
954 		if (r1 == 0)
958 	The WRITE_ONCE() does not depend on the READ_ONCE(), and as a
966                 to assume that r1 will sometimes be 0 (but see the
969                 CPUs do not execute stores before po-earlier conditional
976 	For instance, suppose that a 0 value in r1 would trigger undefined
977 	behavior elsewhere.  Then a clever compiler might deduce that r1
978 	can never be 0 in the if condition.  As a result, said clever
983 2.	Multiple access sizes for a single variable are not supported,
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
999 	However, a substantial amount of support is provided for these
1000 	operations, as shown in the linux-kernel.def file.
1004 	a.	When rcu_assign_pointer() is passed NULL, the Linux
1006 		case as a store release.
1015 		definition in linux-kernel.def).  atomic_add_unless() is
1021 		callback function, with (for example) a release-acquire
1027 		(for example) a release-acquire from the end of each
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
1049 	into herd7 or that are defined in the linux-kernel.def file.
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.
1069 	For example, when an initializer contains the name of a shared
1070 	variable, that name denotes a pointer to that variable, not
1074 9.	Dynamic memory allocation is not supported, although this can
1079 more likely to be addressed by incorporating the Linux-kernel memory model