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.
159 scripts Various scripts, see scripts/README.
166 The Linux-kernel memory model has the following limitations:
168 1. Compiler optimizations are not modeled. Of course, the use
169 of READ_ONCE() and WRITE_ONCE() limits the compiler's ability
170 to optimize, but there is Linux-kernel code that uses bare C
171 memory accesses. Handling this code is on the to-do list.
172 For more information, see Documentation/explanation.txt (in
173 particular, the "THE PROGRAM ORDER RELATION: po AND po-loc"
174 and "A WARNING" sections).
176 Note that this limitation in turn limits LKMM's ability to
177 accurately model address, control, and data dependencies.
178 For example, if the compiler can deduce the value of some variable
179 carrying a dependency, then the compiler can break that dependency
180 by substituting a constant of that value.
182 2. Multiple access sizes for a single variable are not supported,
183 and neither are misaligned or partially overlapping accesses.
185 3. Exceptions and interrupts are not modeled. In some cases,
186 this limitation can be overcome by modeling the interrupt or
187 exception with an additional process.
189 4. I/O such as MMIO or DMA is not supported.
191 5. Self-modifying code (such as that found in the kernel's
192 alternatives mechanism, function tracer, Berkeley Packet Filter
193 JIT compiler, and module loader) is not supported.
195 6. Complete modeling of all variants of atomic read-modify-write
196 operations, locking primitives, and RCU is not provided.
197 For example, call_rcu() and rcu_barrier() are not supported.
198 However, a substantial amount of support is provided for these
199 operations, as shown in the linux-kernel.def file.
201 a. When rcu_assign_pointer() is passed NULL, the Linux
202 kernel provides no ordering, but LKMM models this
203 case as a store release.
205 b. The "unless" RMW operations are not currently modeled:
206 atomic_long_add_unless(), atomic_add_unless(),
207 atomic_inc_unless_negative(), and
208 atomic_dec_unless_positive(). These can be emulated
209 in litmus tests, for example, by using atomic_cmpxchg().
211 c. The call_rcu() function is not modeled. It can be
212 emulated in litmus tests by adding another process that
213 invokes synchronize_rcu() and the body of the callback
214 function, with (for example) a release-acquire from
215 the site of the emulated call_rcu() to the beginning
216 of the additional process.
218 d. The rcu_barrier() function is not modeled. It can be
219 emulated in litmus tests emulating call_rcu() via
220 (for example) a release-acquire from the end of each
221 additional call_rcu() process to the site of the
222 emulated rcu-barrier().
224 e. Sleepable RCU (SRCU) is not modeled. It can be
225 emulated, but perhaps not simply.
227 f. Reader-writer locking is not modeled. It can be
228 emulated in litmus tests using atomic read-modify-write
231 The "herd7" tool has some additional limitations of its own, apart from
234 1. Non-trivial data structures such as arrays or structures are
235 not supported. However, pointers are supported, allowing trivial
236 linked lists to be constructed.
238 2. Dynamic memory allocation is not supported, although this can
239 be worked around in some cases by supplying multiple statically
242 Some of these limitations may be overcome in the future, but others are
243 more likely to be addressed by incorporating the Linux-kernel memory model
246 Finally, please note that LKMM is subject to change as hardware, use cases,
247 and compilers evolve.