Name
Date
Size
#Lines
LOC

..--

Documentation/H--6,8755,452

litmus-tests/H--1,4451,115

scripts/H--1,171748

.gitignoreH A D01-Sep-202047 32

READMEH A D13-Dec-20227.2 KiB224167

linux-kernel.bellH A D30-Aug-20233.1 KiB8572

linux-kernel.catH A D30-Aug-20237.8 KiB217184

linux-kernel.cfgH A D04-Jun-2018391 2221

linux-kernel.defH A D30-Aug-20234.8 KiB120104

lock.catH A D04-Aug-20244.5 KiB144116

README

1 		=====================================
2 		LINUX KERNEL MEMORY CONSISTENCY MODEL
3 		=====================================
4 
5 ============
6 INTRODUCTION
7 ============
8 
9 This directory contains the memory consistency model (memory model, for
10 short) of the Linux kernel, written in the "cat" language and executable
11 by the externally provided "herd7" simulator, which exhaustively explores
12 the state space of small litmus tests.
13 
14 In addition, the "klitmus7" tool (also externally provided) may be used
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.
17 
18 
19 ============
20 REQUIREMENTS
21 ============
22 
23 Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
24 downloaded separately:
25 
26   https://github.com/herd/herdtools7
27 
28 See "herdtools7/INSTALL.md" for installation instructions.
29 
30 Note that although these tools usually provide backwards compatibility,
31 this is not absolutely guaranteed.
32 
33 For example, a future version of herd7 might not work with the model
34 in this release.  A compatible model will likely be made available in
35 a later release of Linux kernel.
36 
37 If you absolutely need to run the model in this particular release,
38 please try using the exact version called out above.
39 
40 klitmus7 is independent of the model provided here.  It has its own
41 dependency on a target kernel release where converted code is built
42 and executed.  Any change in kernel APIs essential to klitmus7 will
43 necessitate an upgrade of klitmus7.
44 
45 If you find any compatibility issues in klitmus7, please inform the
46 memory model maintainers.
47 
48 klitmus7 Compatibility Table
49 ----------------------------
50 
51 	============  ==========
52 	target Linux  herdtools7
53 	------------  ----------
54 	     -- 4.14  7.48 --
55 	4.15 -- 4.19  7.49 --
56 	4.20 -- 5.5   7.54 --
57 	5.6  -- 5.16  7.56 --
58 	5.17 --       7.56.1 --
59 	============  ==========
60 
61 
62 ==================
63 BASIC USAGE: HERD7
64 ==================
65 
66 The memory model is used, in conjunction with "herd7", to exhaustively
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.
70 
71 Example litmus tests may be found in the Linux-kernel source tree:
72 
73 	tools/memory-model/litmus-tests/
74 	Documentation/litmus-tests/
75 
76 Several thousand more example litmus tests are available here:
77 
78 	https://github.com/paulmckrcu/litmus
79 	https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd
80 	https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus
81 
82 Documentation describing litmus tests and now to use them may be found
83 here:
84 
85 	tools/memory-model/Documentation/litmus-tests.txt
86 
87 The remainder of this section uses the SB+fencembonceonces.litmus test
88 located in the tools/memory-model directory.
89 
90 To run SB+fencembonceonces.litmus against the memory model:
91 
92   $ cd $LINUX_SOURCE_TREE/tools/memory-model
93   $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
94 
95 Here is the corresponding output:
96 
97   Test SB+fencembonceonces Allowed
98   States 3
99   0:r0=0; 1:r0=1;
100   0:r0=1; 1:r0=0;
101   0:r0=1; 1:r0=1;
102   No
103   Witnesses
104   Positive: 0 Negative: 3
105   Condition exists (0:r0=0 /\ 1:r0=0)
106   Observation SB+fencembonceonces Never 0 3
107   Time SB+fencembonceonces 0.01
108   Hash=d66d99523e2cac6b06e66f4c995ebb48
109 
110 The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
111 this litmus test's "exists" clause can not be satisfied.
112 
113 See "herd7 -help" or "herdtools7/doc/" for more information on running the
114 tool itself, but please be aware that this documentation is intended for
115 people who work on the memory model itself, that is, people making changes
116 to the tools/memory-model/linux-kernel.* files.  It is not intended for
117 people focusing on writing, understanding, and running LKMM litmus tests.
118 
119 
120 =====================
121 BASIC USAGE: KLITMUS7
122 =====================
123 
124 The "klitmus7" tool converts a litmus test into a Linux kernel module,
125 which may then be loaded and run.
126 
127 For example, to run SB+fencembonceonces.litmus against hardware:
128 
129   $ mkdir mymodules
130   $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
131   $ cd mymodules ; make
132   $ sudo sh run.sh
133 
134 The corresponding output includes:
135 
136   Test SB+fencembonceonces Allowed
137   Histogram (3 states)
138   644580  :>0:r0=1; 1:r0=0;
139   644328  :>0:r0=0; 1:r0=1;
140   711092  :>0:r0=1; 1:r0=1;
141   No
142   Witnesses
143   Positive: 0, Negative: 2000000
144   Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
145   Hash=d66d99523e2cac6b06e66f4c995ebb48
146   Observation SB+fencembonceonces Never 0 2000000
147   Time SB+fencembonceonces 0.16
148 
149 The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
150 that during two million trials, the state specified in this litmus
151 test's "exists" clause was not reached.
152 
153 And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
154 for more information.  And again, please be aware that this documentation
155 is intended for people who work on the memory model itself, that is,
156 people making changes to the tools/memory-model/linux-kernel.* files.
157 It is not intended for people focusing on writing, understanding, and
158 running LKMM litmus tests.
159 
160 
161 ====================
162 DESCRIPTION OF FILES
163 ====================
164 
165 Documentation/README
166 	Guide to the other documents in the Documentation/ directory.
167 
168 linux-kernel.bell
169 	Categorizes the relevant instructions, including memory
170 	references, memory barriers, atomic read-modify-write operations,
171 	lock acquisition/release, and RCU operations.
172 
173 	More formally, this file (1) lists the subtypes of the various
174 	event types used by the memory model and (2) performs RCU
175 	read-side critical section nesting analysis.
176 
177 linux-kernel.cat
178 	Specifies what reorderings are forbidden by memory references,
179 	memory barriers, atomic read-modify-write operations, and RCU.
180 
181 	More formally, this file specifies what executions are forbidden
182 	by the memory model.  Allowed executions are those which
183 	satisfy the model's "coherence", "atomic", "happens-before",
184 	"propagation", and "rcu" axioms, which are defined in the file.
185 
186 linux-kernel.cfg
187 	Convenience file that gathers the common-case herd7 command-line
188 	arguments.
189 
190 linux-kernel.def
191 	Maps from C-like syntax to herd7's internal litmus-test
192 	instruction-set architecture.
193 
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.
198 
199 	By "representative", it means the one in the litmus-tests
200 	directory is:
201 
202 		1) simple, the number of threads should be relatively
203 		   small and each thread function should be relatively
204 		   simple.
205 		2) orthogonal, there should be no two litmus tests
206 		   describing the same aspect of the memory model.
207 		3) textbook, developers can easily copy-paste-modify
208 		   the litmus tests to use the patterns on their own
209 		   code.
210 
211 lock.cat
212 	Provides a front-end analysis of lock acquisition and release,
213 	for example, associating a lock acquisition with the preceding
214 	and following releases and checking for self-deadlock.
215 
216 	More formally, this file defines a performance-enhanced scheme
217 	for generation of the possible reads-from and coherence order
218 	relations on the locking primitives.
219 
220 README
221 	This file.
222 
223 scripts	Various scripts, see scripts/README.
224