Lines Matching refs:litmus
12 the state space of small litmus tests.
15 to convert a litmus test to a Linux kernel module, which in turn allows
16 that litmus test to be exercised within the Linux kernel.
66 explore the state space of small litmus tests. Documentation describing
67 the format, features, capabilities and limitations of these litmus
68 tests is available in tools/memory-model/Documentation/litmus-tests.txt.
70 Example litmus tests may be found in the Linux-kernel source tree:
72 tools/memory-model/litmus-tests/
73 Documentation/litmus-tests/
75 Several thousand more example litmus tests are available here:
77 https://github.com/paulmckrcu/litmus
79 https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus
81 Documentation describing litmus tests and now to use them may be found
84 tools/memory-model/Documentation/litmus-tests.txt
86 The remainder of this section uses the SB+fencembonceonces.litmus test
89 To run SB+fencembonceonces.litmus against the memory model:
92 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
110 this litmus test's "exists" clause can not be satisfied.
116 people focusing on writing, understanding, and running LKMM litmus tests.
123 The "klitmus7" tool converts a litmus test into a Linux kernel module,
126 For example, to run SB+fencembonceonces.litmus against hardware:
129 $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
149 that during two million trials, the state specified in this litmus
157 running LKMM litmus tests.
190 Maps from C-like syntax to herd7's internal litmus-test
193 litmus-tests
194 Directory containing a few representative litmus tests, which
195 are listed in litmus-tests/README. A great deal more litmus
196 tests are available at https://github.com/paulmckrcu/litmus.