Loading...
1 =====================================
2 LINUX KERNEL MEMORY CONSISTENCY MODEL
3 =====================================
4
5============
6INTRODUCTION
7============
8
9This directory contains the memory consistency model (memory model, for
10short) of the Linux kernel, written in the "cat" language and executable
11by the externally provided "herd7" simulator, which exhaustively explores
12the state space of small litmus tests.
13
14In addition, the "klitmus7" tool (also externally provided) may be used
15to convert a litmus test to a Linux kernel module, which in turn allows
16that litmus test to be exercised within the Linux kernel.
17
18
19============
20REQUIREMENTS
21============
22
23Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
24downloaded separately:
25
26 https://github.com/herd/herdtools7
27
28See "herdtools7/INSTALL.md" for installation instructions.
29
30Note that although these tools usually provide backwards compatibility,
31this is not absolutely guaranteed.
32
33For example, a future version of herd7 might not work with the model
34in this release. A compatible model will likely be made available in
35a later release of Linux kernel.
36
37If you absolutely need to run the model in this particular release,
38please try using the exact version called out above.
39
40klitmus7 is independent of the model provided here. It has its own
41dependency on a target kernel release where converted code is built
42and executed. Any change in kernel APIs essential to klitmus7 will
43necessitate an upgrade of klitmus7.
44
45If you find any compatibility issues in klitmus7, please inform the
46memory model maintainers.
47
48klitmus7 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==================
63BASIC USAGE: HERD7
64==================
65
66The memory model is used, in conjunction with "herd7", to exhaustively
67explore the state space of small litmus tests. Documentation describing
68the format, features, capabilities and limitations of these litmus
69tests is available in tools/memory-model/Documentation/litmus-tests.txt.
70
71Example litmus tests may be found in the Linux-kernel source tree:
72
73 tools/memory-model/litmus-tests/
74 Documentation/litmus-tests/
75
76Several 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
82Documentation describing litmus tests and now to use them may be found
83here:
84
85 tools/memory-model/Documentation/litmus-tests.txt
86
87The remainder of this section uses the SB+fencembonceonces.litmus test
88located in the tools/memory-model directory.
89
90To 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
95Here 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
110The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
111this litmus test's "exists" clause can not be satisfied.
112
113See "herd7 -help" or "herdtools7/doc/" for more information on running the
114tool itself, but please be aware that this documentation is intended for
115people who work on the memory model itself, that is, people making changes
116to the tools/memory-model/linux-kernel.* files. It is not intended for
117people focusing on writing, understanding, and running LKMM litmus tests.
118
119
120=====================
121BASIC USAGE: KLITMUS7
122=====================
123
124The "klitmus7" tool converts a litmus test into a Linux kernel module,
125which may then be loaded and run.
126
127For 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
134The 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
149The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
150that during two million trials, the state specified in this litmus
151test's "exists" clause was not reached.
152
153And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
154for more information. And again, please be aware that this documentation
155is intended for people who work on the memory model itself, that is,
156people making changes to the tools/memory-model/linux-kernel.* files.
157It is not intended for people focusing on writing, understanding, and
158running LKMM litmus tests.
159
160
161====================
162DESCRIPTION OF FILES
163====================
164
165Documentation/README
166 Guide to the other documents in the Documentation/ directory.
167
168linux-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
177linux-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
186linux-kernel.cfg
187 Convenience file that gathers the common-case herd7 command-line
188 arguments.
189
190linux-kernel.def
191 Maps from C-like syntax to herd7's internal litmus-test
192 instruction-set architecture.
193
194litmus-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
211lock.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
220README
221 This file.
222
223scripts Various scripts, see scripts/README.
1 =====================================
2 LINUX KERNEL MEMORY CONSISTENCY MODEL
3 =====================================
4
5============
6INTRODUCTION
7============
8
9This directory contains the memory consistency model (memory model, for
10short) of the Linux kernel, written in the "cat" language and executable
11by the externally provided "herd7" simulator, which exhaustively explores
12the state space of small litmus tests.
13
14In addition, the "klitmus7" tool (also externally provided) may be used
15to convert a litmus test to a Linux kernel module, which in turn allows
16that litmus test to be exercised within the Linux kernel.
17
18
19============
20REQUIREMENTS
21============
22
23Version 7.48 of the "herd7" and "klitmus7" tools must be downloaded
24separately:
25
26 https://github.com/herd/herdtools7
27
28See "herdtools7/INSTALL.md" for installation instructions.
29
30
31==================
32BASIC USAGE: HERD7
33==================
34
35The memory model is used, in conjunction with "herd7", to exhaustively
36explore the state space of small litmus tests.
37
38For example, to run SB+mbonceonces.litmus against the memory model:
39
40 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+mbonceonces.litmus
41
42Here is the corresponding output:
43
44 Test SB+mbonceonces Allowed
45 States 3
46 0:r0=0; 1:r0=1;
47 0:r0=1; 1:r0=0;
48 0:r0=1; 1:r0=1;
49 No
50 Witnesses
51 Positive: 0 Negative: 3
52 Condition exists (0:r0=0 /\ 1:r0=0)
53 Observation SB+mbonceonces Never 0 3
54 Time SB+mbonceonces 0.01
55 Hash=d66d99523e2cac6b06e66f4c995ebb48
56
57The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
58this litmus test's "exists" clause can not be satisfied.
59
60See "herd7 -help" or "herdtools7/doc/" for more information.
61
62
63=====================
64BASIC USAGE: KLITMUS7
65=====================
66
67The "klitmus7" tool converts a litmus test into a Linux kernel module,
68which may then be loaded and run.
69
70For example, to run SB+mbonceonces.litmus against hardware:
71
72 $ mkdir mymodules
73 $ klitmus7 -o mymodules litmus-tests/SB+mbonceonces.litmus
74 $ cd mymodules ; make
75 $ sudo sh run.sh
76
77The corresponding output includes:
78
79 Test SB+mbonceonces Allowed
80 Histogram (3 states)
81 644580 :>0:r0=1; 1:r0=0;
82 644328 :>0:r0=0; 1:r0=1;
83 711092 :>0:r0=1; 1:r0=1;
84 No
85 Witnesses
86 Positive: 0, Negative: 2000000
87 Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
88 Hash=d66d99523e2cac6b06e66f4c995ebb48
89 Observation SB+mbonceonces Never 0 2000000
90 Time SB+mbonceonces 0.16
91
92The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
93that during two million trials, the state specified in this litmus
94test's "exists" clause was not reached.
95
96And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
97for more information.
98
99
100====================
101DESCRIPTION OF FILES
102====================
103
104Documentation/cheatsheet.txt
105 Quick-reference guide to the Linux-kernel memory model.
106
107Documentation/explanation.txt
108 Describes the memory model in detail.
109
110Documentation/recipes.txt
111 Lists common memory-ordering patterns.
112
113Documentation/references.txt
114 Provides background reading.
115
116linux-kernel.bell
117 Categorizes the relevant instructions, including memory
118 references, memory barriers, atomic read-modify-write operations,
119 lock acquisition/release, and RCU operations.
120
121 More formally, this file (1) lists the subtypes of the various
122 event types used by the memory model and (2) performs RCU
123 read-side critical section nesting analysis.
124
125linux-kernel.cat
126 Specifies what reorderings are forbidden by memory references,
127 memory barriers, atomic read-modify-write operations, and RCU.
128
129 More formally, this file specifies what executions are forbidden
130 by the memory model. Allowed executions are those which
131 satisfy the model's "coherence", "atomic", "happens-before",
132 "propagation", and "rcu" axioms, which are defined in the file.
133
134linux-kernel.cfg
135 Convenience file that gathers the common-case herd7 command-line
136 arguments.
137
138linux-kernel.def
139 Maps from C-like syntax to herd7's internal litmus-test
140 instruction-set architecture.
141
142litmus-tests
143 Directory containing a few representative litmus tests, which
144 are listed in litmus-tests/README. A great deal more litmus
145 tests are available at https://github.com/paulmckrcu/litmus.
146
147lock.cat
148 Provides a front-end analysis of lock acquisition and release,
149 for example, associating a lock acquisition with the preceding
150 and following releases and checking for self-deadlock.
151
152 More formally, this file defines a performance-enhanced scheme
153 for generation of the possible reads-from and coherence order
154 relations on the locking primitives.
155
156README
157 This file.
158
159
160===========
161LIMITATIONS
162===========
163
164The Linux-kernel memory model has the following limitations:
165
1661. Compiler optimizations are not modeled. Of course, the use
167 of READ_ONCE() and WRITE_ONCE() limits the compiler's ability
168 to optimize, but there is Linux-kernel code that uses bare C
169 memory accesses. Handling this code is on the to-do list.
170 For more information, see Documentation/explanation.txt (in
171 particular, the "THE PROGRAM ORDER RELATION: po AND po-loc"
172 and "A WARNING" sections).
173
1742. Multiple access sizes for a single variable are not supported,
175 and neither are misaligned or partially overlapping accesses.
176
1773. Exceptions and interrupts are not modeled. In some cases,
178 this limitation can be overcome by modeling the interrupt or
179 exception with an additional process.
180
1814. I/O such as MMIO or DMA is not supported.
182
1835. Self-modifying code (such as that found in the kernel's
184 alternatives mechanism, function tracer, Berkeley Packet Filter
185 JIT compiler, and module loader) is not supported.
186
1876. Complete modeling of all variants of atomic read-modify-write
188 operations, locking primitives, and RCU is not provided.
189 For example, call_rcu() and rcu_barrier() are not supported.
190 However, a substantial amount of support is provided for these
191 operations, as shown in the linux-kernel.def file.
192
193The "herd7" tool has some additional limitations of its own, apart from
194the memory model:
195
1961. Non-trivial data structures such as arrays or structures are
197 not supported. However, pointers are supported, allowing trivial
198 linked lists to be constructed.
199
2002. Dynamic memory allocation is not supported, although this can
201 be worked around in some cases by supplying multiple statically
202 allocated variables.
203
204Some of these limitations may be overcome in the future, but others are
205more likely to be addressed by incorporating the Linux-kernel memory model
206into other tools.