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 | ||
5b62832c | 23 | Version 7.49 of the "herd7" and "klitmus7" tools must be downloaded |
8f7f2fbd | 24 | separately: |
1c27b644 PM |
25 | |
26 | https://github.com/herd/herdtools7 | |
27 | ||
28 | See "herdtools7/INSTALL.md" for installation instructions. | |
29 | ||
1c27b644 PM |
30 | |
31 | ================== | |
32 | BASIC USAGE: HERD7 | |
33 | ================== | |
34 | ||
35 | The memory model is used, in conjunction with "herd7", to exhaustively | |
36 | explore the state space of small litmus tests. | |
37 | ||
71b7ff5e | 38 | For example, to run SB+fencembonceonces.litmus against the memory model: |
1c27b644 | 39 | |
71b7ff5e | 40 | $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus |
1c27b644 PM |
41 | |
42 | Here is the corresponding output: | |
43 | ||
71b7ff5e | 44 | Test SB+fencembonceonces Allowed |
1c27b644 PM |
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) | |
71b7ff5e AP |
53 | Observation SB+fencembonceonces Never 0 3 |
54 | Time SB+fencembonceonces 0.01 | |
1c27b644 PM |
55 | Hash=d66d99523e2cac6b06e66f4c995ebb48 |
56 | ||
57 | The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that | |
58 | this litmus test's "exists" clause can not be satisfied. | |
59 | ||
60 | See "herd7 -help" or "herdtools7/doc/" for more information. | |
61 | ||
62 | ||
63 | ===================== | |
64 | BASIC USAGE: KLITMUS7 | |
65 | ===================== | |
66 | ||
67 | The "klitmus7" tool converts a litmus test into a Linux kernel module, | |
68 | which may then be loaded and run. | |
69 | ||
71b7ff5e | 70 | For example, to run SB+fencembonceonces.litmus against hardware: |
1c27b644 PM |
71 | |
72 | $ mkdir mymodules | |
71b7ff5e | 73 | $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus |
1c27b644 PM |
74 | $ cd mymodules ; make |
75 | $ sudo sh run.sh | |
76 | ||
77 | The corresponding output includes: | |
78 | ||
71b7ff5e | 79 | Test SB+fencembonceonces Allowed |
1c27b644 PM |
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 | |
71b7ff5e AP |
89 | Observation SB+fencembonceonces Never 0 2000000 |
90 | Time SB+fencembonceonces 0.16 | |
1c27b644 PM |
91 | |
92 | The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate | |
93 | that during two million trials, the state specified in this litmus | |
94 | test's "exists" clause was not reached. | |
95 | ||
96 | And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/" | |
97 | for more information. | |
98 | ||
99 | ||
100 | ==================== | |
101 | DESCRIPTION OF FILES | |
102 | ==================== | |
103 | ||
104 | Documentation/cheatsheet.txt | |
105 | Quick-reference guide to the Linux-kernel memory model. | |
106 | ||
107 | Documentation/explanation.txt | |
108 | Describes the memory model in detail. | |
109 | ||
110 | Documentation/recipes.txt | |
111 | Lists common memory-ordering patterns. | |
112 | ||
113 | Documentation/references.txt | |
114 | Provides background reading. | |
115 | ||
116 | linux-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 | ||
125 | linux-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 | ||
134 | linux-kernel.cfg | |
135 | Convenience file that gathers the common-case herd7 command-line | |
136 | arguments. | |
137 | ||
138 | linux-kernel.def | |
139 | Maps from C-like syntax to herd7's internal litmus-test | |
140 | instruction-set architecture. | |
141 | ||
142 | litmus-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 | ||
147 | lock.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 | ||
156 | README | |
157 | This file. | |
158 | ||
159 | ||
160 | =========== | |
161 | LIMITATIONS | |
162 | =========== | |
163 | ||
164 | The Linux-kernel memory model has the following limitations: | |
165 | ||
166 | 1. 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 | ||
d8fa25c4 PM |
174 | Note that this limitation in turn limits LKMM's ability to |
175 | accurately model address, control, and data dependencies. | |
176 | For example, if the compiler can deduce the value of some variable | |
177 | carrying a dependency, then the compiler can break that dependency | |
178 | by substituting a constant of that value. | |
179 | ||
1c27b644 PM |
180 | 2. Multiple access sizes for a single variable are not supported, |
181 | and neither are misaligned or partially overlapping accesses. | |
182 | ||
183 | 3. Exceptions and interrupts are not modeled. In some cases, | |
184 | this limitation can be overcome by modeling the interrupt or | |
185 | exception with an additional process. | |
186 | ||
187 | 4. I/O such as MMIO or DMA is not supported. | |
188 | ||
189 | 5. Self-modifying code (such as that found in the kernel's | |
190 | alternatives mechanism, function tracer, Berkeley Packet Filter | |
191 | JIT compiler, and module loader) is not supported. | |
192 | ||
193 | 6. Complete modeling of all variants of atomic read-modify-write | |
194 | operations, locking primitives, and RCU is not provided. | |
195 | For example, call_rcu() and rcu_barrier() are not supported. | |
196 | However, a substantial amount of support is provided for these | |
197 | operations, as shown in the linux-kernel.def file. | |
198 | ||
d8fa25c4 PM |
199 | a. When rcu_assign_pointer() is passed NULL, the Linux |
200 | kernel provides no ordering, but LKMM models this | |
201 | case as a store release. | |
202 | ||
203 | b. The "unless" RMW operations are not currently modeled: | |
204 | atomic_long_add_unless(), atomic_add_unless(), | |
205 | atomic_inc_unless_negative(), and | |
206 | atomic_dec_unless_positive(). These can be emulated | |
207 | in litmus tests, for example, by using atomic_cmpxchg(). | |
208 | ||
209 | c. The call_rcu() function is not modeled. It can be | |
210 | emulated in litmus tests by adding another process that | |
211 | invokes synchronize_rcu() and the body of the callback | |
212 | function, with (for example) a release-acquire from | |
213 | the site of the emulated call_rcu() to the beginning | |
214 | of the additional process. | |
215 | ||
216 | d. The rcu_barrier() function is not modeled. It can be | |
217 | emulated in litmus tests emulating call_rcu() via | |
218 | (for example) a release-acquire from the end of each | |
219 | additional call_rcu() process to the site of the | |
220 | emulated rcu-barrier(). | |
221 | ||
222 | e. Sleepable RCU (SRCU) is not modeled. It can be | |
223 | emulated, but perhaps not simply. | |
224 | ||
225 | f. Reader-writer locking is not modeled. It can be | |
226 | emulated in litmus tests using atomic read-modify-write | |
227 | operations. | |
228 | ||
1c27b644 PM |
229 | The "herd7" tool has some additional limitations of its own, apart from |
230 | the memory model: | |
231 | ||
232 | 1. Non-trivial data structures such as arrays or structures are | |
233 | not supported. However, pointers are supported, allowing trivial | |
234 | linked lists to be constructed. | |
235 | ||
236 | 2. Dynamic memory allocation is not supported, although this can | |
237 | be worked around in some cases by supplying multiple statically | |
238 | allocated variables. | |
239 | ||
240 | Some of these limitations may be overcome in the future, but others are | |
241 | more likely to be addressed by incorporating the Linux-kernel memory model | |
242 | into other tools. | |
d8fa25c4 PM |
243 | |
244 | Finally, please note that LKMM is subject to change as hardware, use cases, | |
245 | and compilers evolve. |