1 ==============================
2 LINUX KERNEL MEMORY CONSISTENC
3 ==============================
4
5 ============
6 INTRODUCTION
7 ============
8
9 This directory contains the memory consistency
10 short) of the Linux kernel, written in the "ca
11 by the externally provided "herd7" simulator,
12 the state space of small litmus tests.
13
14 In addition, the "klitmus7" tool (also externa
15 to convert a litmus test to a Linux kernel mod
16 that litmus test to be exercised within the Li
17
18
19 ============
20 REQUIREMENTS
21 ============
22
23 Version 7.52 or higher of the "herd7" and "kli
24 downloaded separately:
25
26 https://github.com/herd/herdtools7
27
28 See "herdtools7/INSTALL.md" for installation i
29
30 Note that although these tools usually provide
31 this is not absolutely guaranteed.
32
33 For example, a future version of herd7 might n
34 in this release. A compatible model will like
35 a later release of Linux kernel.
36
37 If you absolutely need to run the model in thi
38 please try using the exact version called out
39
40 klitmus7 is independent of the model provided
41 dependency on a target kernel release where co
42 and executed. Any change in kernel APIs essen
43 necessitate an upgrade of klitmus7.
44
45 If you find any compatibility issues in klitmu
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
67 explore the state space of small litmus tests.
68 the format, features, capabilities and limitat
69 tests is available in tools/memory-model/Docum
70
71 Example litmus tests may be found in the Linux
72
73 tools/memory-model/litmus-tests/
74 Documentation/litmus-tests/
75
76 Several thousand more example litmus tests are
77
78 https://github.com/paulmckrcu/litmus
79 https://git.kernel.org/pub/scm/linux/k
80 https://git.kernel.org/pub/scm/linux/k
81
82 Documentation describing litmus tests and now
83 here:
84
85 tools/memory-model/Documentation/litmu
86
87 The remainder of this section uses the SB+fenc
88 located in the tools/memory-model directory.
89
90 To run SB+fencembonceonces.litmus against the
91
92 $ cd $LINUX_SOURCE_TREE/tools/memory-model
93 $ herd7 -conf linux-kernel.cfg litmus-tests/
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
111 this litmus test's "exists" clause can not be
112
113 See "herd7 -help" or "herdtools7/doc/" for mor
114 tool itself, but please be aware that this doc
115 people who work on the memory model itself, th
116 to the tools/memory-model/linux-kernel.* files
117 people focusing on writing, understanding, and
118
119
120 =====================
121 BASIC USAGE: KLITMUS7
122 =====================
123
124 The "klitmus7" tool converts a litmus test int
125 which may then be loaded and run.
126
127 For example, to run SB+fencembonceonces.litmus
128
129 $ mkdir mymodules
130 $ klitmus7 -o mymodules litmus-tests/SB+fenc
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 v
145 Hash=d66d99523e2cac6b06e66f4c995ebb48
146 Observation SB+fencembonceonces Never 0 2000
147 Time SB+fencembonceonces 0.16
148
149 The "Positive: 0 Negative: 2000000" and the "N
150 that during two million trials, the state spec
151 test's "exists" clause was not reached.
152
153 And, as with "herd7", please see "klitmus7 -he
154 for more information. And again, please be aw
155 is intended for people who work on the memory
156 people making changes to the tools/memory-mode
157 It is not intended for people focusing on writ
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 Do
167
168 linux-kernel.bell
169 Categorizes the relevant instructions,
170 references, memory barriers, atomic re
171 lock acquisition/release, and RCU oper
172
173 More formally, this file (1) lists the
174 event types used by the memory model a
175 read-side critical section nesting ana
176
177 linux-kernel.cat
178 Specifies what reorderings are forbidd
179 memory barriers, atomic read-modify-wr
180
181 More formally, this file specifies wha
182 by the memory model. Allowed executio
183 satisfy the model's "coherence", "atom
184 "propagation", and "rcu" axioms, which
185
186 linux-kernel.cfg
187 Convenience file that gathers the comm
188 arguments.
189
190 linux-kernel.def
191 Maps from C-like syntax to herd7's int
192 instruction-set architecture.
193
194 litmus-tests
195 Directory containing a few representat
196 are listed in litmus-tests/README. A
197 tests are available at https://github.
198
199 By "representative", it means the one
200 directory is:
201
202 1) simple, the number of threa
203 small and each thread funct
204 simple.
205 2) orthogonal, there should be
206 describing the same aspect
207 3) textbook, developers can ea
208 the litmus tests to use the
209 code.
210
211 lock.cat
212 Provides a front-end analysis of lock
213 for example, associating a lock acquis
214 and following releases and checking fo
215
216 More formally, this file defines a per
217 for generation of the possible reads-f
218 relations on the locking primitives.
219
220 README
221 This file.
222
223 scripts Various scripts, see scripts/README.
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.