Lines Matching refs:litmus
4 This file describes the LKMM litmus-test format by example, describes
27 existing litmus test than it is to create one from scratch. A number
28 of litmus tests may be found in the kernel source tree:
30 tools/memory-model/litmus-tests/
31 Documentation/litmus-tests/
33 Several thousand more example litmus tests are available on github
36 https://github.com/paulmckrcu/litmus
38 https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus
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.
49 This section describes the overall format of litmus tests, starting
58 This section gives an overview of the format of a litmus test using an
92 the test, which by convention is the filename with the ".litmus"
94 tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
97 Mechanically generated litmus tests will often have an optional
99 when running the test. Yes, you can add your own comments to litmus
103 cover the full litmus-test commenting story.
118 for example, a .litmus file matching "^P1(" but not matching "^P2("
119 must contain a two-process litmus test.
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
165 Note that the assertion expression is written in the litmus-test
183 herd7 -conf linux-kernel.cfg litmus-tests/MP+pooncerelease+poacquireonce.litmus
224 litmus test.
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
242 by tooling that manages litmus tests and their output. This tooling is
244 people know which of the several thousand relevant litmus tests were
252 "x" and "y", but a similar litmus test could instead initialize them
371 spin loops, handling trivial linked lists, adding comments to litmus tests,
373 in order to better handle large litmus tests.
381 aided by the values of other variables. Consider this litmus test
382 (tools/memory-order/litmus-tests/SB+rfionceonce-poonceonces.litmus but
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:
490 https://github.com/paulmckrcu/litmus/blob/master/manual/kernel/
503 modeling such loops. For example, the following litmus tests emulates
542 This litmus test may be found here:
544 …cm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus
586 Why doesn't the litmus test take the simpler approach of using a spin loop
588 insight behind this litmus test is that spin loops have no effect on the
610 But what if the litmus test were to temporarily set "0:r2" to a non-zero
614 Why not just try it? Line 4 of the following modified litmus test
656 execution, running this litmus test would display no executions because
684 can be done within these confines, as can be seen in the litmus test
685 at tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus:
763 Different portions of a litmus test are processed by different parsers,
765 different portions of the litmus test. The C-syntax portions use
769 The following litmus test illustrates the comment style corresponding
807 the rest of the litmus test.
816 The following litmus test is derived from the example show in
817 Documentation/litmus-tests/rcu/RCU+sync+free.litmus, but converted to
886 litmus test.
893 was able to analyze the following 10-process RCU litmus test in about
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-…
902 litmus test in about 300 milliseconds, for more than an order of magnitude
905 Larger 16-process litmus tests that would normally consume 15 minutes
910 …thub.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…
912 Nevertheless, litmus-test analysis really is of exponential complexity,
914 processes to a 19-process litmus test requires 2 hours and 40 minutes
917 16-process litmus test. Again, to be fair, the multi-hour run explores
920 …m/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…
927 helpful when developing and debugging litmus tests.
1011 in litmus tests, for example, by using atomic_cmpxchg().
1016 modeled by herd7 therefore it can be used in litmus tests.
1019 it can be emulated in litmus tests by adding another
1026 emulated in litmus tests emulating call_rcu() via
1057 emulated in litmus tests using atomic read-modify-write
1060 The fragment of the C language supported by these litmus tests is quite
1084 6. Although you can use a wide variety of types in litmus-test