1 =====================================
2 LINUX KERNEL MEMORY CONSISTENCY MODEL
3 =====================================
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.
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.
23 Version 7.49 of the "herd7" and "klitmus7" tools must be downloaded
26 https://github.com/herd/herdtools7
28 See "herdtools7/INSTALL.md" for installation instructions.
35 The memory model is used, in conjunction with "herd7", to exhaustively
36 explore the state space of small litmus tests.
38 For example, to run SB+fencembonceonces.litmus against the memory model:
40 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
42 Here is the corresponding output:
44 Test SB+fencembonceonces Allowed
51 Positive: 0 Negative: 3
52 Condition exists (0:r0=0 /\ 1:r0=0)
53 Observation SB+fencembonceonces Never 0 3
54 Time SB+fencembonceonces 0.01
55 Hash=d66d99523e2cac6b06e66f4c995ebb48
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.
60 See "herd7 -help" or "herdtools7/doc/" for more information.
67 The "klitmus7" tool converts a litmus test into a Linux kernel module,
68 which may then be loaded and run.
70 For example, to run SB+fencembonceonces.litmus against hardware:
73 $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
77 The corresponding output includes:
79 Test SB+fencembonceonces Allowed
81 644580 :>0:r0=1; 1:r0=0;
82 644328 :>0:r0=0; 1:r0=1;
83 711092 :>0:r0=1; 1:r0=1;
86 Positive: 0, Negative: 2000000
87 Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
88 Hash=d66d99523e2cac6b06e66f4c995ebb48
89 Observation SB+fencembonceonces Never 0 2000000
90 Time SB+fencembonceonces 0.16
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.
96 And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
104 Documentation/cheatsheet.txt
105 Quick-reference guide to the Linux-kernel memory model.
107 Documentation/explanation.txt
108 Describes the memory model in detail.
110 Documentation/recipes.txt
111 Lists common memory-ordering patterns.
113 Documentation/references.txt
114 Provides background reading.
117 Categorizes the relevant instructions, including memory
118 references, memory barriers, atomic read-modify-write operations,
119 lock acquisition/release, and RCU operations.
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.
126 Specifies what reorderings are forbidden by memory references,
127 memory barriers, atomic read-modify-write operations, and RCU.
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.
135 Convenience file that gathers the common-case herd7 command-line
139 Maps from C-like syntax to herd7's internal litmus-test
140 instruction-set architecture.
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.
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.
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.
164 The Linux-kernel memory model has the following limitations:
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).
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.
180 2. Multiple access sizes for a single variable are not supported,
181 and neither are misaligned or partially overlapping accesses.
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.
187 4. I/O such as MMIO or DMA is not supported.
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.
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.
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.
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().
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.
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().
222 e. Sleepable RCU (SRCU) is not modeled. It can be
223 emulated, but perhaps not simply.
225 f. Reader-writer locking is not modeled. It can be
226 emulated in litmus tests using atomic read-modify-write
229 The "herd7" tool has some additional limitations of its own, apart from
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.
236 2. Dynamic memory allocation is not supported, although this can
237 be worked around in some cases by supplying multiple statically
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
244 Finally, please note that LKMM is subject to change as hardware, use cases,
245 and compilers evolve.