Lines Matching +full:no +full:- +full:high +full:- +full:z
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
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
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
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
101 For now, you can use C-language comments in the C code, and these comments
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,
119 must contain a two-process litmus test.
122 used by that function. Unlike normal C-language function parameters, the
130 P0() has no local variables, but P1() has two of them named "r0" and "r1".
132 other litmus-test formats, it is conventional to use names consisting of
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.
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".
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
193 6 No
212 Another important part of this output is shown in lines 2-5, repeated here:
219 Line 2 gives the total number of end states, and each of lines 3-5 list
232 "No" says that the "exists" clause was not satisfied by any execution,
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.
241 Line 12 gives a hash of the contents for the litmus-test file, and is used
249 --------------
279 Lines 3-6 now initialize both "x" and "y" to the value 42. This also
291 6 No
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
344 executed only if line 9 loads a non-zero value from "x". Because P1()'s
352 5 No
360 However, there is no "while" statement due to the fact that full
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
414 1 Test SB+rfionceonce-poonceonces Allowed
424 11 Observation SB+rfionceonce-poonceonces Sometimes 1 3
425 12 Time SB+rfionceonce-poonceonces 0.01
439 1 C SB+rfionceonce-poonceonces
468 1 Test SB+rfionceonce-poonceonces Allowed
478 11 Observation SB+rfionceonce-poonceonces Sometimes 1 3
479 12 Time SB+rfionceonce-poonceonces 0.01
487 the outcome! For one example, please see the C-READ_ONCE.litmus and
488 C-READ_ONCE-omitted.litmus tests located here:
494 ----------
502 Fortunately, it is possible to avoid state-space explosion by specially
508 models, if for no other reason that these are much faster. However, 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
544 …cm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus
572 1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed
576 5 No
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
588 insight behind this litmus test is that spin loops have no effect on the
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,
610 But what if the litmus test were to temporarily set "0:r2" to a non-zero
617 the "filter" clause. Line 24 does a known-true "if" condition to avoid
622 1 C C-SB+l-o-o-u+l-o-o-u-X
656 execution, running this litmus test would display no executions because
660 1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed
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
679 ------------
685 at tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus:
690 4 y=z;
691 5 z=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
726 from "y", replacing "z".
729 pointer. The RCU read-side critical section spanning lines 19-22 is just
741 4 1:r0=z; 1:r1=0;
742 5 No
750 The only possible outcomes feature P1() loading a pointer to "z"
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
777 6 y=z; (* C *)
778 7 z=0;
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)
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
859 will replace "x" with "z" in this list.
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
880 -----------
882 LKMM's exploration of the full state-space can be extremely helpful,
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
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:
940 the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING"
959 result, LKMM does not claim ordering. However, even though no
969 CPUs do not execute stores before po-earlier conditional
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.
1005 kernel provides no ordering, but LKMM models this
1014 which is provided directly by herd7 (so no corresponding
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
1041 2. There is no way to create functions other than the Pn() functions
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,
1065 7. Parsing of variable declarations is very loose, with almost no
1068 8. Initializers differ from their C-language counterparts.
1079 more likely to be addressed by incorporating the Linux-kernel memory model