Commit | Line | Data |
---|---|---|
48d44d4e AP |
1 | ===================================== |
2 | LINUX KERNEL MEMORY CONSISTENCY MODEL | |
3 | ===================================== | |
1c27b644 PM |
4 | |
5 | ============ | |
6 | INTRODUCTION | |
7 | ============ | |
8 | ||
48d44d4e AP |
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. | |
1c27b644 PM |
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 | ||
034fb712 AP |
23 | Version 7.52 or higher of the "herd7" and "klitmus7" tools must be |
24 | downloaded separately: | |
1c27b644 PM |
25 | |
26 | https://github.com/herd/herdtools7 | |
27 | ||
28 | See "herdtools7/INSTALL.md" for installation instructions. | |
29 | ||
034fb712 | 30 | Note that although these tools usually provide backwards compatibility, |
d075a78a AY |
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 | ------------ ---------- | |
3d5c7032 | 54 | -- 4.14 7.48 -- |
d075a78a AY |
55 | 4.15 -- 4.19 7.49 -- |
56 | 4.20 -- 5.5 7.54 -- | |
5b759db4 AY |
57 | 5.6 -- 5.16 7.56 -- |
58 | 5.17 -- 7.56.1 -- | |
d075a78a | 59 | ============ ========== |
034fb712 | 60 | |
1c27b644 PM |
61 | |
62 | ================== | |
63 | BASIC USAGE: HERD7 | |
64 | ================== | |
65 | ||
66 | The memory model is used, in conjunction with "herd7", to exhaustively | |
984f272b PM |
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. | |
1c27b644 | 70 | |
984f272b | 71 | Example litmus tests may be found in the Linux-kernel source tree: |
1c27b644 | 72 | |
984f272b PM |
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 | |
71b7ff5e | 93 | $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus |
1c27b644 PM |
94 | |
95 | Here is the corresponding output: | |
96 | ||
71b7ff5e | 97 | Test SB+fencembonceonces Allowed |
1c27b644 PM |
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) | |
71b7ff5e AP |
106 | Observation SB+fencembonceonces Never 0 3 |
107 | Time SB+fencembonceonces 0.01 | |
1c27b644 PM |
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 | ||
984f272b PM |
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. | |
1c27b644 PM |
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 | ||
71b7ff5e | 127 | For example, to run SB+fencembonceonces.litmus against hardware: |
1c27b644 PM |
128 | |
129 | $ mkdir mymodules | |
71b7ff5e | 130 | $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus |
1c27b644 PM |
131 | $ cd mymodules ; make |
132 | $ sudo sh run.sh | |
133 | ||
134 | The corresponding output includes: | |
135 | ||
71b7ff5e | 136 | Test SB+fencembonceonces Allowed |
1c27b644 PM |
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 | |
71b7ff5e AP |
146 | Observation SB+fencembonceonces Never 0 2000000 |
147 | Time SB+fencembonceonces 0.16 | |
1c27b644 PM |
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/" | |
984f272b PM |
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. | |
1c27b644 PM |
159 | |
160 | ||
161 | ==================== | |
162 | DESCRIPTION OF FILES | |
163 | ==================== | |
164 | ||
ab8bcad6 PM |
165 | Documentation/README |
166 | Guide to the other documents in the Documentation/ directory. | |
0b8c06b7 | 167 | |
1c27b644 PM |
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 | ||
b47c05ec BF |
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 | ||
1c27b644 PM |
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 | ||
b02eb5b0 | 223 | scripts Various scripts, see scripts/README. |