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.
67 explore the state space of small litmus tests.  Documentation describing
68 the format, features, capabilities and limitations of these litmus
69 tests is available in tools/memory-model/Documentation/litmus-tests.txt.
71 Example litmus tests may be found in the Linux-kernel source tree:
73 	tools/memory-model/litmus-tests/
74 	Documentation/litmus-tests/
76 Several thousand more example litmus tests are available here:
78 	https://github.com/paulmckrcu/litmus
80 	https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus
82 Documentation describing litmus tests and now to use them may be found
85 	tools/memory-model/Documentation/litmus-tests.txt
87 The remainder of this section uses the SB+fencembonceonces.litmus test
90 To run SB+fencembonceonces.litmus against the memory model:
93   $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
111 this litmus test's "exists" clause can not be satisfied.
117 people focusing on writing, understanding, and running LKMM litmus tests.
124 The "klitmus7" tool converts a litmus test into a Linux kernel module,
127 For example, to run SB+fencembonceonces.litmus against hardware:
130   $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
150 that during two million trials, the state specified in this litmus
158 running LKMM litmus tests.
191 	Maps from C-like syntax to herd7's internal litmus-test
194 litmus-tests
195 	Directory containing a few representative litmus tests, which
196 	are listed in litmus-tests/README.  A great deal more litmus
197 	tests are available at https://github.com/paulmckrcu/litmus.
199 	By "representative", it means the one in the litmus-tests
205 		2) orthogonal, there should be no two litmus tests
208 		   the litmus tests to use the patterns on their own