Lines Matching +full:acquisition +full:- +full:time
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
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
198 11 Time MP+pooncerelease+poacquireonce 0.00
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
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.
238 The number at the end of line 11 (which begins with "Time") gives the
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
249 --------------
279 Lines 3-6 now initialize both "x" and "y" to the value 42. This also
296 11 Time MP+pooncerelease+poacquireonce 0.02
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
357 10 Time LB+fencembonceonce+ctrlonceonce 0.00
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 ----------
497 at best of exponential time complexity. Adding processes and increasing
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
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
549 that process sets "sl" back to "0". P0()'s lock acquisition is emulated
552 the lock acquisition was successful or unsuccessful (due to "sl" already
572 1 Test C-SB+l-o-o-u+l-o-o-u-X Allowed
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
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,
592 each lock acquisition will eventually succeed. Because herd7 already
593 explores the full state space, the length of time required to actually
602 only at the end of time, thus requiring herd7 to waste time on bogus
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
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:
729 pointer. The RCU read-side critical section spanning lines 19-22 is just
747 10 Time MP+onceassign+derefonce 0.00
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
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
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
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
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
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
933 Limitations of the Linux-kernel memory model (LKMM) include:
940 the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING"
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.
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.
1079 more likely to be addressed by incorporating the Linux-kernel memory model