1 Explanation of the Linux-Kernel Memory Consistency Model
2 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4 :Author: Alan Stern <stern@rowland.harvard.edu>
12 4. A SELECTION OF MEMORY MODELS
13 5. ORDERING AND CYCLES
15 7. THE PROGRAM ORDER RELATION: po AND po-loc
17 9. DEPENDENCY RELATIONS: data, addr, and ctrl
18 10. THE READS-FROM RELATION: rf, rfi, and rfe
19 11. CACHE COHERENCE AND THE COHERENCE ORDER RELATION: co, coi, and coe
20 12. THE FROM-READS RELATION: fr, fri, and fre
21 13. AN OPERATIONAL MODEL
22 14. PROPAGATION ORDER RELATION: cumul-fence
23 15. DERIVATION OF THE LKMM FROM THE OPERATIONAL MODEL
24 16. SEQUENTIAL CONSISTENCY PER VARIABLE
25 17. ATOMIC UPDATES: rmw
26 18. THE PRESERVED PROGRAM ORDER RELATION: ppo
27 19. AND THEN THERE WAS ALPHA
28 20. THE HAPPENS-BEFORE RELATION: hb
29 21. THE PROPAGATES-BEFORE RELATION: pb
30 22. RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb
32 24. PLAIN ACCESSES AND DATA RACES
40 The Linux-kernel memory consistency model (LKMM) is rather complex and
41 obscure. This is particularly evident if you read through the
42 linux-kernel.bell and linux-kernel.cat files that make up the formal
43 version of the model; they are extremely terse and their meanings are
46 This document describes the ideas underlying the LKMM. It is meant
47 for people who want to understand how the model was designed. It does
48 not go into the details of the code in the .bell and .cat files;
49 rather, it explains in English what the code expresses symbolically.
51 Sections 2 (BACKGROUND) through 5 (ORDERING AND CYCLES) are aimed
52 toward beginners; they explain what memory consistency models are and
53 the basic notions shared by all such models. People already familiar
54 with these concepts can skim or skip over them. Sections 6 (EVENTS)
55 through 12 (THE FROM_READS RELATION) describe the fundamental
56 relations used in many models. Starting in Section 13 (AN OPERATIONAL
57 MODEL), the workings of the LKMM itself are covered.
59 Warning: The code examples in this document are not written in the
60 proper format for litmus tests. They don't include a header line, the
61 initializations are not enclosed in braces, the global variables are
62 not passed by pointers, and they don't have an "exists" clause at the
63 end. Converting them to the right format is left as an exercise for
70 A memory consistency model (or just memory model, for short) is
71 something which predicts, given a piece of computer code running on a
72 particular kind of system, what values may be obtained by the code's
73 load instructions. The LKMM makes these predictions for code running
74 as part of the Linux kernel.
76 In practice, people tend to use memory models the other way around.
77 That is, given a piece of code and a collection of values specified
78 for the loads, the model will predict whether it is possible for the
79 code to run in such a way that the loads will indeed obtain the
80 specified values. Of course, this is just another way of expressing
83 For code running on a uniprocessor system, the predictions are easy:
84 Each load instruction must obtain the value written by the most recent
85 store instruction accessing the same location (we ignore complicating
86 factors such as DMA and mixed-size accesses.) But on multiprocessor
87 systems, with multiple CPUs making concurrent accesses to shared
88 memory locations, things aren't so simple.
90 Different architectures have differing memory models, and the Linux
91 kernel supports a variety of architectures. The LKMM has to be fairly
92 permissive, in the sense that any behavior allowed by one of these
93 architectures also has to be allowed by the LKMM.
99 Here is a simple example to illustrate the basic concepts. Consider
100 some code running as part of a device driver for an input device. The
101 driver might contain an interrupt handler which collects data from the
102 device, stores it in a buffer, and sets a flag to indicate the buffer
103 is full. Running concurrently on a different CPU might be a part of
104 the driver code being executed by a process in the midst of a read(2)
105 system call. This code tests the flag to see whether the buffer is
106 ready, and if it is, copies the data back to userspace. The buffer
107 and the flag are memory locations shared between the two CPUs.
109 We can abstract out the important pieces of the driver code as follows
110 (the reason for using WRITE_ONCE() and READ_ONCE() instead of simple
111 assignment statements is discussed later):
113 int buf = 0, flag = 0;
126 r1 = READ_ONCE(flag);
131 Here the P0() function represents the interrupt handler running on one
132 CPU and P1() represents the read() routine running on another. The
133 value 1 stored in buf represents input data collected from the device.
134 Thus, P0 stores the data in buf and then sets flag. Meanwhile, P1
135 reads flag into the private variable r1, and if it is set, reads the
136 data from buf into a second private variable r2 for copying to
137 userspace. (Presumably if flag is not set then the driver will wait a
138 while and try again.)
140 This pattern of memory accesses, where one CPU stores values to two
141 shared memory locations and another CPU loads from those locations in
142 the opposite order, is widely known as the "Message Passing" or MP
143 pattern. It is typical of memory access patterns in the kernel.
145 Please note that this example code is a simplified abstraction. Real
146 buffers are usually larger than a single integer, real device drivers
147 usually use sleep and wakeup mechanisms rather than polling for I/O
148 completion, and real code generally doesn't bother to copy values into
149 private variables before using them. All that is beside the point;
150 the idea here is simply to illustrate the overall pattern of memory
151 accesses by the CPUs.
153 A memory model will predict what values P1 might obtain for its loads
154 from flag and buf, or equivalently, what values r1 and r2 might end up
155 with after the code has finished running.
157 Some predictions are trivial. For instance, no sane memory model would
158 predict that r1 = 42 or r2 = -7, because neither of those values ever
159 gets stored in flag or buf.
161 Some nontrivial predictions are nonetheless quite simple. For
162 instance, P1 might run entirely before P0 begins, in which case r1 and
163 r2 will both be 0 at the end. Or P0 might run entirely before P1
164 begins, in which case r1 and r2 will both be 1.
166 The interesting predictions concern what might happen when the two
167 routines run concurrently. One possibility is that P1 runs after P0's
168 store to buf but before the store to flag. In this case, r1 and r2
169 will again both be 0. (If P1 had been designed to read buf
170 unconditionally then we would instead have r1 = 0 and r2 = 1.)
172 However, the most interesting possibility is where r1 = 1 and r2 = 0.
173 If this were to occur it would mean the driver contains a bug, because
174 incorrect data would get sent to the user: 0 instead of 1. As it
175 happens, the LKMM does predict this outcome can occur, and the example
176 driver code shown above is indeed buggy.
179 A SELECTION OF MEMORY MODELS
180 ----------------------------
182 The first widely cited memory model, and the simplest to understand,
183 is Sequential Consistency. According to this model, systems behave as
184 if each CPU executed its instructions in order but with unspecified
185 timing. In other words, the instructions from the various CPUs get
186 interleaved in a nondeterministic way, always according to some single
187 global order that agrees with the order of the instructions in the
188 program source for each CPU. The model says that the value obtained
189 by each load is simply the value written by the most recently executed
190 store to the same memory location, from any CPU.
192 For the MP example code shown above, Sequential Consistency predicts
193 that the undesired result r1 = 1, r2 = 0 cannot occur. The reasoning
196 Since r1 = 1, P0 must store 1 to flag before P1 loads 1 from
197 it, as loads can obtain values only from earlier stores.
199 P1 loads from flag before loading from buf, since CPUs execute
200 their instructions in order.
202 P1 must load 0 from buf before P0 stores 1 to it; otherwise r2
203 would be 1 since a load obtains its value from the most recent
204 store to the same address.
206 P0 stores 1 to buf before storing 1 to flag, since it executes
207 its instructions in order.
209 Since an instruction (in this case, P0's store to flag) cannot
210 execute before itself, the specified outcome is impossible.
212 However, real computer hardware almost never follows the Sequential
213 Consistency memory model; doing so would rule out too many valuable
214 performance optimizations. On ARM and PowerPC architectures, for
215 instance, the MP example code really does sometimes yield r1 = 1 and
218 x86 and SPARC follow yet a different memory model: TSO (Total Store
219 Ordering). This model predicts that the undesired outcome for the MP
220 pattern cannot occur, but in other respects it differs from Sequential
221 Consistency. One example is the Store Buffer (SB) pattern, in which
222 each CPU stores to its own shared location and then loads from the
223 other CPU's location:
243 Sequential Consistency predicts that the outcome r0 = 0, r1 = 0 is
244 impossible. (Exercise: Figure out the reasoning.) But TSO allows
245 this outcome to occur, and in fact it does sometimes occur on x86 and
248 The LKMM was inspired by the memory models followed by PowerPC, ARM,
249 x86, Alpha, and other architectures. However, it is different in
250 detail from each of them.
256 Memory models are all about ordering. Often this is temporal ordering
257 (i.e., the order in which certain events occur) but it doesn't have to
258 be; consider for example the order of instructions in a program's
259 source code. We saw above that Sequential Consistency makes an
260 important assumption that CPUs execute instructions in the same order
261 as those instructions occur in the code, and there are many other
262 instances of ordering playing central roles in memory models.
264 The counterpart to ordering is a cycle. Ordering rules out cycles:
265 It's not possible to have X ordered before Y, Y ordered before Z, and
266 Z ordered before X, because this would mean that X is ordered before
267 itself. The analysis of the MP example under Sequential Consistency
268 involved just such an impossible cycle:
270 W: P0 stores 1 to flag executes before
271 X: P1 loads 1 from flag executes before
272 Y: P1 loads 0 from buf executes before
273 Z: P0 stores 1 to buf executes before
274 W: P0 stores 1 to flag.
276 In short, if a memory model requires certain accesses to be ordered,
277 and a certain outcome for the loads in a piece of code can happen only
278 if those accesses would form a cycle, then the memory model predicts
279 that outcome cannot occur.
281 The LKMM is defined largely in terms of cycles, as we will see.
287 The LKMM does not work directly with the C statements that make up
288 kernel source code. Instead it considers the effects of those
289 statements in a more abstract form, namely, events. The model
290 includes three types of events:
292 Read events correspond to loads from shared memory, such as
293 calls to READ_ONCE(), smp_load_acquire(), or
296 Write events correspond to stores to shared memory, such as
297 calls to WRITE_ONCE(), smp_store_release(), or atomic_set().
299 Fence events correspond to memory barriers (also known as
300 fences), such as calls to smp_rmb() or rcu_read_lock().
302 These categories are not exclusive; a read or write event can also be
303 a fence. This happens with functions like smp_load_acquire() or
304 spin_lock(). However, no single event can be both a read and a write.
305 Atomic read-modify-write accesses, such as atomic_inc() or xchg(),
306 correspond to a pair of events: a read followed by a write. (The
307 write event is omitted for executions where it doesn't occur, such as
308 a cmpxchg() where the comparison fails.)
310 Other parts of the code, those which do not involve interaction with
311 shared memory, do not give rise to events. Thus, arithmetic and
312 logical computations, control-flow instructions, or accesses to
313 private memory or CPU registers are not of central interest to the
314 memory model. They only affect the model's predictions indirectly.
315 For example, an arithmetic computation might determine the value that
316 gets stored to a shared memory location (or in the case of an array
317 index, the address where the value gets stored), but the memory model
318 is concerned only with the store itself -- its value and its address
319 -- not the computation leading up to it.
321 Events in the LKMM can be linked by various relations, which we will
322 describe in the following sections. The memory model requires certain
323 of these relations to be orderings, that is, it requires them not to
327 THE PROGRAM ORDER RELATION: po AND po-loc
328 -----------------------------------------
330 The most important relation between events is program order (po). You
331 can think of it as the order in which statements occur in the source
332 code after branches are taken into account and loops have been
333 unrolled. A better description might be the order in which
334 instructions are presented to a CPU's execution unit. Thus, we say
335 that X is po-before Y (written as "X ->po Y" in formulas) if X occurs
336 before Y in the instruction stream.
338 This is inherently a single-CPU relation; two instructions executing
339 on different CPUs are never linked by po. Also, it is by definition
340 an ordering so it cannot have any cycles.
342 po-loc is a sub-relation of po. It links two memory accesses when the
343 first comes before the second in program order and they access the
344 same memory location (the "-loc" suffix).
346 Although this may seem straightforward, there is one subtle aspect to
347 program order we need to explain. The LKMM was inspired by low-level
348 architectural memory models which describe the behavior of machine
349 code, and it retains their outlook to a considerable extent. The
350 read, write, and fence events used by the model are close in spirit to
351 individual machine instructions. Nevertheless, the LKMM describes
352 kernel code written in C, and the mapping from C to machine code can
353 be extremely complex.
355 Optimizing compilers have great freedom in the way they translate
356 source code to object code. They are allowed to apply transformations
357 that add memory accesses, eliminate accesses, combine them, split them
358 into pieces, or move them around. The use of READ_ONCE(), WRITE_ONCE(),
359 or one of the other atomic or synchronization primitives prevents a
360 large number of compiler optimizations. In particular, it is guaranteed
361 that the compiler will not remove such accesses from the generated code
362 (unless it can prove the accesses will never be executed), it will not
363 change the order in which they occur in the code (within limits imposed
364 by the C standard), and it will not introduce extraneous accesses.
366 The MP and SB examples above used READ_ONCE() and WRITE_ONCE() rather
367 than ordinary memory accesses. Thanks to this usage, we can be certain
368 that in the MP example, the compiler won't reorder P0's write event to
369 buf and P0's write event to flag, and similarly for the other shared
370 memory accesses in the examples.
372 Since private variables are not shared between CPUs, they can be
373 accessed normally without READ_ONCE() or WRITE_ONCE(). In fact, they
374 need not even be stored in normal memory at all -- in principle a
375 private variable could be stored in a CPU register (hence the convention
376 that these variables have names starting with the letter 'r').
382 The protections provided by READ_ONCE(), WRITE_ONCE(), and others are
383 not perfect; and under some circumstances it is possible for the
384 compiler to undermine the memory model. Here is an example. Suppose
385 both branches of an "if" statement store the same value to the same
391 ... /* do something */
394 ... /* do something else */
397 For this code, the LKMM predicts that the load from x will always be
398 executed before either of the stores to y. However, a compiler could
399 lift the stores out of the conditional, transforming the code into
400 something resembling:
405 ... /* do something */
407 ... /* do something else */
410 Given this version of the code, the LKMM would predict that the load
411 from x could be executed after the store to y. Thus, the memory
412 model's original prediction could be invalidated by the compiler.
414 Another issue arises from the fact that in C, arguments to many
415 operators and function calls can be evaluated in any order. For
420 The object code might call f(5) either before or after g(6); the
421 memory model cannot assume there is a fixed program order relation
422 between them. (In fact, if the function calls are inlined then the
423 compiler might even interleave their object code.)
426 DEPENDENCY RELATIONS: data, addr, and ctrl
427 ------------------------------------------
429 We say that two events are linked by a dependency relation when the
430 execution of the second event depends in some way on a value obtained
431 from memory by the first. The first event must be a read, and the
432 value it obtains must somehow affect what the second event does.
433 There are three kinds of dependencies: data, address (addr), and
436 A read and a write event are linked by a data dependency if the value
437 obtained by the read affects the value stored by the write. As a very
443 WRITE_ONCE(y, r1 + 5);
445 The value stored by the WRITE_ONCE obviously depends on the value
446 loaded by the READ_ONCE. Such dependencies can wind through
447 arbitrarily complicated computations, and a write can depend on the
448 values of multiple reads.
450 A read event and another memory access event are linked by an address
451 dependency if the value obtained by the read affects the location
452 accessed by the other event. The second event can be either a read or
453 a write. Here's another simple example:
459 r2 = READ_ONCE(a[r1]);
461 Here the location accessed by the second READ_ONCE() depends on the
462 index value loaded by the first. Pointer indirection also gives rise
463 to address dependencies, since the address of a location accessed
464 through a pointer will depend on the value read earlier from that
467 Finally, a read event and another memory access event are linked by a
468 control dependency if the value obtained by the read affects whether
469 the second event is executed at all. Simple example:
477 Execution of the WRITE_ONCE() is controlled by a conditional expression
478 which depends on the value obtained by the READ_ONCE(); hence there is
479 a control dependency from the load to the store.
481 It should be pretty obvious that events can only depend on reads that
482 come earlier in program order. Symbolically, if we have R ->data X,
483 R ->addr X, or R ->ctrl X (where R is a read event), then we must also
484 have R ->po X. It wouldn't make sense for a computation to depend
485 somehow on a value that doesn't get loaded from shared memory until
488 Here's a trick question: When is a dependency not a dependency? Answer:
489 When it is purely syntactic rather than semantic. We say a dependency
490 between two accesses is purely syntactic if the second access doesn't
491 actually depend on the result of the first. Here is a trivial example:
494 WRITE_ONCE(y, r1 * 0);
496 There appears to be a data dependency from the load of x to the store
497 of y, since the value to be stored is computed from the value that was
498 loaded. But in fact, the value stored does not really depend on
499 anything since it will always be 0. Thus the data dependency is only
500 syntactic (it appears to exist in the code) but not semantic (the
501 second access will always be the same, regardless of the value of the
502 first access). Given code like this, a compiler could simply discard
503 the value returned by the load from x, which would certainly destroy
504 any dependency. (The compiler is not permitted to eliminate entirely
505 the load generated for a READ_ONCE() -- that's one of the nice
506 properties of READ_ONCE() -- but it is allowed to ignore the load's
509 It's natural to object that no one in their right mind would write
510 code like the above. However, macro expansions can easily give rise
511 to this sort of thing, in ways that often are not apparent to the
514 Another mechanism that can lead to purely syntactic dependencies is
515 related to the notion of "undefined behavior". Certain program
516 behaviors are called "undefined" in the C language specification,
517 which means that when they occur there are no guarantees at all about
518 the outcome. Consider the following example:
524 r2 = READ_ONCE(a[r1]);
526 Access beyond the end or before the beginning of an array is one kind
527 of undefined behavior. Therefore the compiler doesn't have to worry
528 about what will happen if r1 is nonzero, and it can assume that r1
529 will always be zero regardless of the value actually loaded from i.
530 (If the assumption turns out to be wrong the resulting behavior will
531 be undefined anyway, so the compiler doesn't care!) Thus the value
532 from the load can be discarded, breaking the address dependency.
534 The LKMM is unaware that purely syntactic dependencies are different
535 from semantic dependencies and therefore mistakenly predicts that the
536 accesses in the two examples above will be ordered. This is another
537 example of how the compiler can undermine the memory model. Be warned.
540 THE READS-FROM RELATION: rf, rfi, and rfe
541 -----------------------------------------
543 The reads-from relation (rf) links a write event to a read event when
544 the value loaded by the read is the value that was stored by the
545 write. In colloquial terms, the load "reads from" the store. We
546 write W ->rf R to indicate that the load R reads from the store W. We
547 further distinguish the cases where the load and the store occur on
548 the same CPU (internal reads-from, or rfi) and where they occur on
549 different CPUs (external reads-from, or rfe).
551 For our purposes, a memory location's initial value is treated as
552 though it had been written there by an imaginary initial store that
553 executes on a separate CPU before the main program runs.
555 Usage of the rf relation implicitly assumes that loads will always
556 read from a single store. It doesn't apply properly in the presence
557 of load-tearing, where a load obtains some of its bits from one store
558 and some of them from another store. Fortunately, use of READ_ONCE()
559 and WRITE_ONCE() will prevent load-tearing; it's not possible to have:
565 WRITE_ONCE(x, 0x1234);
575 and end up with r1 = 0x1200 (partly from x's initial value and partly
576 from the value stored by P0).
578 On the other hand, load-tearing is unavoidable when mixed-size
579 accesses are used. Consider this example:
588 WRITE_ONCE(x.h[0], 0x1234);
589 WRITE_ONCE(x.h[1], 0x5678);
599 If r1 = 0x56781234 (little-endian!) at the end, then P1 must have read
600 from both of P0's stores. It is possible to handle mixed-size and
601 unaligned accesses in a memory model, but the LKMM currently does not
602 attempt to do so. It requires all accesses to be properly aligned and
603 of the location's actual size.
606 CACHE COHERENCE AND THE COHERENCE ORDER RELATION: co, coi, and coe
607 ------------------------------------------------------------------
609 Cache coherence is a general principle requiring that in a
610 multi-processor system, the CPUs must share a consistent view of the
611 memory contents. Specifically, it requires that for each location in
612 shared memory, the stores to that location must form a single global
613 ordering which all the CPUs agree on (the coherence order), and this
614 ordering must be consistent with the program order for accesses to
617 To put it another way, for any variable x, the coherence order (co) of
618 the stores to x is simply the order in which the stores overwrite one
619 another. The imaginary store which establishes x's initial value
620 comes first in the coherence order; the store which directly
621 overwrites the initial value comes second; the store which overwrites
622 that value comes third, and so on.
624 You can think of the coherence order as being the order in which the
625 stores reach x's location in memory (or if you prefer a more
626 hardware-centric view, the order in which the stores get written to
627 x's cache line). We write W ->co W' if W comes before W' in the
628 coherence order, that is, if the value stored by W gets overwritten,
629 directly or indirectly, by the value stored by W'.
631 Coherence order is required to be consistent with program order. This
632 requirement takes the form of four coherency rules:
634 Write-write coherence: If W ->po-loc W' (i.e., W comes before
635 W' in program order and they access the same location), where W
636 and W' are two stores, then W ->co W'.
638 Write-read coherence: If W ->po-loc R, where W is a store and R
639 is a load, then R must read from W or from some other store
640 which comes after W in the coherence order.
642 Read-write coherence: If R ->po-loc W, where R is a load and W
643 is a store, then the store which R reads from must come before
644 W in the coherence order.
646 Read-read coherence: If R ->po-loc R', where R and R' are two
647 loads, then either they read from the same store or else the
648 store read by R comes before the store read by R' in the
651 This is sometimes referred to as sequential consistency per variable,
652 because it means that the accesses to any single memory location obey
653 the rules of the Sequential Consistency memory model. (According to
654 Wikipedia, sequential consistency per variable and cache coherence
655 mean the same thing except that cache coherence includes an extra
656 requirement that every store eventually becomes visible to every CPU.)
658 Any reasonable memory model will include cache coherence. Indeed, our
659 expectation of cache coherence is so deeply ingrained that violations
660 of its requirements look more like hardware bugs than programming
671 If the final value stored in x after this code ran was 17, you would
672 think your computer was broken. It would be a violation of the
673 write-write coherence rule: Since the store of 23 comes later in
674 program order, it must also come later in x's coherence order and
675 thus must overwrite the store of 17.
687 If r1 = 666 at the end, this would violate the read-write coherence
688 rule: The READ_ONCE() load comes before the WRITE_ONCE() store in
689 program order, so it must not read from that store but rather from one
690 coming earlier in the coherence order (in this case, x's initial
708 If r1 = 5 (reading from P0's store) and r2 = 0 (reading from the
709 imaginary store which establishes x's initial value) at the end, this
710 would violate the read-read coherence rule: The r1 load comes before
711 the r2 load in program order, so it must not read from a store that
712 comes later in the coherence order.
714 (As a minor curiosity, if this code had used normal loads instead of
715 READ_ONCE() in P1, on Itanium it sometimes could end up with r1 = 5
716 and r2 = 0! This results from parallel execution of the operations
717 encoded in Itanium's Very-Long-Instruction-Word format, and it is yet
718 another motivation for using READ_ONCE() when accessing shared memory
721 Just like the po relation, co is inherently an ordering -- it is not
722 possible for a store to directly or indirectly overwrite itself! And
723 just like with the rf relation, we distinguish between stores that
724 occur on the same CPU (internal coherence order, or coi) and stores
725 that occur on different CPUs (external coherence order, or coe).
727 On the other hand, stores to different memory locations are never
728 related by co, just as instructions on different CPUs are never
729 related by po. Coherence order is strictly per-location, or if you
730 prefer, each location has its own independent coherence order.
733 THE FROM-READS RELATION: fr, fri, and fre
734 -----------------------------------------
736 The from-reads relation (fr) can be a little difficult for people to
737 grok. It describes the situation where a load reads a value that gets
738 overwritten by a store. In other words, we have R ->fr W when the
739 value that R reads is overwritten (directly or indirectly) by W, or
740 equivalently, when R reads from a store which comes earlier than W in
755 The value loaded from x will be 0 (assuming cache coherence!), and it
756 gets overwritten by the value 2. Thus there is an fr link from the
757 READ_ONCE() to the WRITE_ONCE(). If the code contained any later
758 stores to x, there would also be fr links from the READ_ONCE() to
761 As with rf, rfi, and rfe, we subdivide the fr relation into fri (when
762 the load and the store are on the same CPU) and fre (when they are on
765 Note that the fr relation is determined entirely by the rf and co
766 relations; it is not independent. Given a read event R and a write
767 event W for the same location, we will have R ->fr W if and only if
768 the write which R reads from is co-before W. In symbols,
770 (R ->fr W) := (there exists W' with W' ->rf R and W' ->co W).
776 The LKMM is based on various operational memory models, meaning that
777 the models arise from an abstract view of how a computer system
778 operates. Here are the main ideas, as incorporated into the LKMM.
780 The system as a whole is divided into the CPUs and a memory subsystem.
781 The CPUs are responsible for executing instructions (not necessarily
782 in program order), and they communicate with the memory subsystem.
783 For the most part, executing an instruction requires a CPU to perform
784 only internal operations. However, loads, stores, and fences involve
787 When CPU C executes a store instruction, it tells the memory subsystem
788 to store a certain value at a certain location. The memory subsystem
789 propagates the store to all the other CPUs as well as to RAM. (As a
790 special case, we say that the store propagates to its own CPU at the
791 time it is executed.) The memory subsystem also determines where the
792 store falls in the location's coherence order. In particular, it must
793 arrange for the store to be co-later than (i.e., to overwrite) any
794 other store to the same location which has already propagated to CPU C.
796 When a CPU executes a load instruction R, it first checks to see
797 whether there are any as-yet unexecuted store instructions, for the
798 same location, that come before R in program order. If there are, it
799 uses the value of the po-latest such store as the value obtained by R,
800 and we say that the store's value is forwarded to R. Otherwise, the
801 CPU asks the memory subsystem for the value to load and we say that R
802 is satisfied from memory. The memory subsystem hands back the value
803 of the co-latest store to the location in question which has already
804 propagated to that CPU.
806 (In fact, the picture needs to be a little more complicated than this.
807 CPUs have local caches, and propagating a store to a CPU really means
808 propagating it to the CPU's local cache. A local cache can take some
809 time to process the stores that it receives, and a store can't be used
810 to satisfy one of the CPU's loads until it has been processed. On
811 most architectures, the local caches process stores in
812 First-In-First-Out order, and consequently the processing delay
813 doesn't matter for the memory model. But on Alpha, the local caches
814 have a partitioned design that results in non-FIFO behavior. We will
815 discuss this in more detail later.)
817 Note that load instructions may be executed speculatively and may be
818 restarted under certain circumstances. The memory model ignores these
819 premature executions; we simply say that the load executes at the
820 final time it is forwarded or satisfied.
822 Executing a fence (or memory barrier) instruction doesn't require a
823 CPU to do anything special other than informing the memory subsystem
824 about the fence. However, fences do constrain the way CPUs and the
825 memory subsystem handle other instructions, in two respects.
827 First, a fence forces the CPU to execute various instructions in
828 program order. Exactly which instructions are ordered depends on the
831 Strong fences, including smp_mb() and synchronize_rcu(), force
832 the CPU to execute all po-earlier instructions before any
833 po-later instructions;
835 smp_rmb() forces the CPU to execute all po-earlier loads
836 before any po-later loads;
838 smp_wmb() forces the CPU to execute all po-earlier stores
839 before any po-later stores;
841 Acquire fences, such as smp_load_acquire(), force the CPU to
842 execute the load associated with the fence (e.g., the load
843 part of an smp_load_acquire()) before any po-later
846 Release fences, such as smp_store_release(), force the CPU to
847 execute all po-earlier instructions before the store
848 associated with the fence (e.g., the store part of an
849 smp_store_release()).
851 Second, some types of fence affect the way the memory subsystem
852 propagates stores. When a fence instruction is executed on CPU C:
854 For each other CPU C', smp_wmb() forces all po-earlier stores
855 on C to propagate to C' before any po-later stores do.
857 For each other CPU C', any store which propagates to C before
858 a release fence is executed (including all po-earlier
859 stores executed on C) is forced to propagate to C' before the
860 store associated with the release fence does.
862 Any store which propagates to C before a strong fence is
863 executed (including all po-earlier stores on C) is forced to
864 propagate to all other CPUs before any instructions po-after
865 the strong fence are executed on C.
867 The propagation ordering enforced by release fences and strong fences
868 affects stores from other CPUs that propagate to CPU C before the
869 fence is executed, as well as stores that are executed on C before the
870 fence. We describe this property by saying that release fences and
871 strong fences are A-cumulative. By contrast, smp_wmb() fences are not
872 A-cumulative; they only affect the propagation of stores that are
873 executed on C before the fence (i.e., those which precede the fence in
876 rcu_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
877 other properties which we discuss later.
880 PROPAGATION ORDER RELATION: cumul-fence
881 ---------------------------------------
883 The fences which affect propagation order (i.e., strong, release, and
884 smp_wmb() fences) are collectively referred to as cumul-fences, even
885 though smp_wmb() isn't A-cumulative. The cumul-fence relation is
886 defined to link memory access events E and F whenever:
888 E and F are both stores on the same CPU and an smp_wmb() fence
889 event occurs between them in program order; or
891 F is a release fence and some X comes before F in program order,
892 where either X = E or else E ->rf X; or
894 A strong fence event occurs between some X and F in program
895 order, where either X = E or else E ->rf X.
897 The operational model requires that whenever W and W' are both stores
898 and W ->cumul-fence W', then W must propagate to any given CPU
899 before W' does. However, for different CPUs C and C', it does not
900 require W to propagate to C before W' propagates to C'.
903 DERIVATION OF THE LKMM FROM THE OPERATIONAL MODEL
904 -------------------------------------------------
906 The LKMM is derived from the restrictions imposed by the design
907 outlined above. These restrictions involve the necessity of
908 maintaining cache coherence and the fact that a CPU can't operate on a
909 value before it knows what that value is, among other things.
911 The formal version of the LKMM is defined by six requirements, or
914 Sequential consistency per variable: This requires that the
915 system obey the four coherency rules.
917 Atomicity: This requires that atomic read-modify-write
918 operations really are atomic, that is, no other stores can
919 sneak into the middle of such an update.
921 Happens-before: This requires that certain instructions are
922 executed in a specific order.
924 Propagation: This requires that certain stores propagate to
925 CPUs and to RAM in a specific order.
927 Rcu: This requires that RCU read-side critical sections and
928 grace periods obey the rules of RCU, in particular, the
929 Grace-Period Guarantee.
931 Plain-coherence: This requires that plain memory accesses
932 (those not using READ_ONCE(), WRITE_ONCE(), etc.) must obey
933 the operational model's rules regarding cache coherence.
935 The first and second are quite common; they can be found in many
936 memory models (such as those for C11/C++11). The "happens-before" and
937 "propagation" axioms have analogs in other memory models as well. The
938 "rcu" and "plain-coherence" axioms are specific to the LKMM.
940 Each of these axioms is discussed below.
943 SEQUENTIAL CONSISTENCY PER VARIABLE
944 -----------------------------------
946 According to the principle of cache coherence, the stores to any fixed
947 shared location in memory form a global ordering. We can imagine
948 inserting the loads from that location into this ordering, by placing
949 each load between the store that it reads from and the following
950 store. This leaves the relative positions of loads that read from the
951 same store unspecified; let's say they are inserted in program order,
952 first for CPU 0, then CPU 1, etc.
954 You can check that the four coherency rules imply that the rf, co, fr,
955 and po-loc relations agree with this global ordering; in other words,
956 whenever we have X ->rf Y or X ->co Y or X ->fr Y or X ->po-loc Y, the
957 X event comes before the Y event in the global ordering. The LKMM's
958 "coherence" axiom expresses this by requiring the union of these
959 relations not to have any cycles. This means it must not be possible
962 X0 -> X1 -> X2 -> ... -> Xn -> X0,
964 where each of the links is either rf, co, fr, or po-loc. This has to
965 hold if the accesses to the fixed memory location can be ordered as
966 cache coherence demands.
968 Although it is not obvious, it can be shown that the converse is also
969 true: This LKMM axiom implies that the four coherency rules are
976 What does it mean to say that a read-modify-write (rmw) update, such
977 as atomic_inc(&x), is atomic? It means that the memory location (x in
978 this case) does not get altered between the read and the write events
979 making up the atomic operation. In particular, if two CPUs perform
980 atomic_inc(&x) concurrently, it must be guaranteed that the final
981 value of x will be the initial value plus two. We should never have
982 the following sequence of events:
984 CPU 0 loads x obtaining 13;
985 CPU 1 loads x obtaining 13;
986 CPU 0 stores 14 to x;
987 CPU 1 stores 14 to x;
989 where the final value of x is wrong (14 rather than 15).
991 In this example, CPU 0's increment effectively gets lost because it
992 occurs in between CPU 1's load and store. To put it another way, the
993 problem is that the position of CPU 0's store in x's coherence order
994 is between the store that CPU 1 reads from and the store that CPU 1
997 The same analysis applies to all atomic update operations. Therefore,
998 to enforce atomicity the LKMM requires that atomic updates follow this
999 rule: Whenever R and W are the read and write events composing an
1000 atomic read-modify-write and W' is the write event which R reads from,
1001 there must not be any stores coming between W' and W in the coherence
1002 order. Equivalently,
1004 (R ->rmw W) implies (there is no X with R ->fr X and X ->co W),
1006 where the rmw relation links the read and write events making up each
1007 atomic update. This is what the LKMM's "atomic" axiom says.
1010 THE PRESERVED PROGRAM ORDER RELATION: ppo
1011 -----------------------------------------
1013 There are many situations where a CPU is obliged to execute two
1014 instructions in program order. We amalgamate them into the ppo (for
1015 "preserved program order") relation, which links the po-earlier
1016 instruction to the po-later instruction and is thus a sub-relation of
1019 The operational model already includes a description of one such
1020 situation: Fences are a source of ppo links. Suppose X and Y are
1021 memory accesses with X ->po Y; then the CPU must execute X before Y if
1022 any of the following hold:
1024 A strong (smp_mb() or synchronize_rcu()) fence occurs between
1027 X and Y are both stores and an smp_wmb() fence occurs between
1030 X and Y are both loads and an smp_rmb() fence occurs between
1033 X is also an acquire fence, such as smp_load_acquire();
1035 Y is also a release fence, such as smp_store_release().
1037 Another possibility, not mentioned earlier but discussed in the next
1040 X and Y are both loads, X ->addr Y (i.e., there is an address
1041 dependency from X to Y), and X is a READ_ONCE() or an atomic
1044 Dependencies can also cause instructions to be executed in program
1045 order. This is uncontroversial when the second instruction is a
1046 store; either a data, address, or control dependency from a load R to
1047 a store W will force the CPU to execute R before W. This is very
1048 simply because the CPU cannot tell the memory subsystem about W's
1049 store before it knows what value should be stored (in the case of a
1050 data dependency), what location it should be stored into (in the case
1051 of an address dependency), or whether the store should actually take
1052 place (in the case of a control dependency).
1054 Dependencies to load instructions are more problematic. To begin with,
1055 there is no such thing as a data dependency to a load. Next, a CPU
1056 has no reason to respect a control dependency to a load, because it
1057 can always satisfy the second load speculatively before the first, and
1058 then ignore the result if it turns out that the second load shouldn't
1059 be executed after all. And lastly, the real difficulties begin when
1060 we consider address dependencies to loads.
1062 To be fair about it, all Linux-supported architectures do execute
1063 loads in program order if there is an address dependency between them.
1064 After all, a CPU cannot ask the memory subsystem to load a value from
1065 a particular location before it knows what that location is. However,
1066 the split-cache design used by Alpha can cause it to behave in a way
1067 that looks as if the loads were executed out of order (see the next
1068 section for more details). The kernel includes a workaround for this
1069 problem when the loads come from READ_ONCE(), and therefore the LKMM
1070 includes address dependencies to loads in the ppo relation.
1072 On the other hand, dependencies can indirectly affect the ordering of
1073 two loads. This happens when there is a dependency from a load to a
1074 store and a second, po-later load reads from that store:
1078 where the dep link can be either an address or a data dependency. In
1079 this situation we know it is possible for the CPU to execute R' before
1080 W, because it can forward the value that W will store to R'. But it
1081 cannot execute R' before R, because it cannot forward the value before
1082 it knows what that value is, or that W and R' do access the same
1083 location. However, if there is merely a control dependency between R
1084 and W then the CPU can speculatively forward W to R' before executing
1085 R; if the speculation turns out to be wrong then the CPU merely has to
1086 restart or abandon R'.
1088 (In theory, a CPU might forward a store to a load when it runs across
1089 an address dependency like this:
1091 r1 = READ_ONCE(ptr);
1092 WRITE_ONCE(*r1, 17);
1093 r2 = READ_ONCE(*r1);
1095 because it could tell that the store and the second load access the
1096 same location even before it knows what the location's address is.
1097 However, none of the architectures supported by the Linux kernel do
1100 Two memory accesses of the same location must always be executed in
1101 program order if the second access is a store. Thus, if we have
1105 (the po-loc link says that R comes before W in program order and they
1106 access the same location), the CPU is obliged to execute W after R.
1107 If it executed W first then the memory subsystem would respond to R's
1108 read request with the value stored by W (or an even later store), in
1109 violation of the read-write coherence rule. Similarly, if we had
1113 and the CPU executed W' before W, then the memory subsystem would put
1114 W' before W in the coherence order. It would effectively cause W to
1115 overwrite W', in violation of the write-write coherence rule.
1116 (Interestingly, an early ARMv8 memory model, now obsolete, proposed
1117 allowing out-of-order writes like this to occur. The model avoided
1118 violating the write-write coherence rule by requiring the CPU not to
1119 send the W write to the memory subsystem at all!)
1122 AND THEN THERE WAS ALPHA
1123 ------------------------
1125 As mentioned above, the Alpha architecture is unique in that it does
1126 not appear to respect address dependencies to loads. This means that
1127 code such as the following:
1137 WRITE_ONCE(ptr, &x);
1146 r2 = READ_ONCE(*r1);
1149 can malfunction on Alpha systems (notice that P1 uses an ordinary load
1150 to read ptr instead of READ_ONCE()). It is quite possible that r1 = &x
1151 and r2 = 0 at the end, in spite of the address dependency.
1153 At first glance this doesn't seem to make sense. We know that the
1154 smp_wmb() forces P0's store to x to propagate to P1 before the store
1155 to ptr does. And since P1 can't execute its second load
1156 until it knows what location to load from, i.e., after executing its
1157 first load, the value x = 1 must have propagated to P1 before the
1158 second load executed. So why doesn't r2 end up equal to 1?
1160 The answer lies in the Alpha's split local caches. Although the two
1161 stores do reach P1's local cache in the proper order, it can happen
1162 that the first store is processed by a busy part of the cache while
1163 the second store is processed by an idle part. As a result, the x = 1
1164 value may not become available for P1's CPU to read until after the
1165 ptr = &x value does, leading to the undesirable result above. The
1166 final effect is that even though the two loads really are executed in
1167 program order, it appears that they aren't.
1169 This could not have happened if the local cache had processed the
1170 incoming stores in FIFO order. By contrast, other architectures
1171 maintain at least the appearance of FIFO order.
1173 In practice, this difficulty is solved by inserting a special fence
1174 between P1's two loads when the kernel is compiled for the Alpha
1175 architecture. In fact, as of version 4.15, the kernel automatically
1176 adds this fence after every READ_ONCE() and atomic load on Alpha. The
1177 effect of the fence is to cause the CPU not to execute any po-later
1178 instructions until after the local cache has finished processing all
1179 the stores it has already received. Thus, if the code was changed to:
1186 r1 = READ_ONCE(ptr);
1187 r2 = READ_ONCE(*r1);
1190 then we would never get r1 = &x and r2 = 0. By the time P1 executed
1191 its second load, the x = 1 store would already be fully processed by
1192 the local cache and available for satisfying the read request. Thus
1193 we have yet another reason why shared data should always be read with
1194 READ_ONCE() or another synchronization primitive rather than accessed
1197 The LKMM requires that smp_rmb(), acquire fences, and strong fences
1198 share this property: They do not allow the CPU to execute any po-later
1199 instructions (or po-later loads in the case of smp_rmb()) until all
1200 outstanding stores have been processed by the local cache. In the
1201 case of a strong fence, the CPU first has to wait for all of its
1202 po-earlier stores to propagate to every other CPU in the system; then
1203 it has to wait for the local cache to process all the stores received
1204 as of that time -- not just the stores received when the strong fence
1207 And of course, none of this matters for any architecture other than
1211 THE HAPPENS-BEFORE RELATION: hb
1212 -------------------------------
1214 The happens-before relation (hb) links memory accesses that have to
1215 execute in a certain order. hb includes the ppo relation and two
1216 others, one of which is rfe.
1218 W ->rfe R implies that W and R are on different CPUs. It also means
1219 that W's store must have propagated to R's CPU before R executed;
1220 otherwise R could not have read the value stored by W. Therefore W
1221 must have executed before R, and so we have W ->hb R.
1223 The equivalent fact need not hold if W ->rfi R (i.e., W and R are on
1224 the same CPU). As we have already seen, the operational model allows
1225 W's value to be forwarded to R in such cases, meaning that R may well
1226 execute before W does.
1228 It's important to understand that neither coe nor fre is included in
1229 hb, despite their similarities to rfe. For example, suppose we have
1230 W ->coe W'. This means that W and W' are stores to the same location,
1231 they execute on different CPUs, and W comes before W' in the coherence
1232 order (i.e., W' overwrites W). Nevertheless, it is possible for W' to
1233 execute before W, because the decision as to which store overwrites
1234 the other is made later by the memory subsystem. When the stores are
1235 nearly simultaneous, either one can come out on top. Similarly,
1236 R ->fre W means that W overwrites the value which R reads, but it
1237 doesn't mean that W has to execute after R. All that's necessary is
1238 for the memory subsystem not to propagate W to R's CPU until after R
1239 has executed, which is possible if W executes shortly before R.
1241 The third relation included in hb is like ppo, in that it only links
1242 events that are on the same CPU. However it is more difficult to
1243 explain, because it arises only indirectly from the requirement of
1244 cache coherence. The relation is called prop, and it links two events
1245 on CPU C in situations where a store from some other CPU comes after
1246 the first event in the coherence order and propagates to C before the
1247 second event executes.
1249 This is best explained with some examples. The simplest case looks
1267 If r1 = 8 at the end then P0's accesses must have executed in program
1268 order. We can deduce this from the operational model; if P0's load
1269 had executed before its store then the value of the store would have
1270 been forwarded to the load, so r1 would have ended up equal to 1, not
1271 8. In this case there is a prop link from P0's write event to its read
1272 event, because P1's store came after P0's store in x's coherence
1273 order, and P1's store propagated to P0 before P0's load executed.
1275 An equally simple case involves two loads of the same location that
1276 read from different stores:
1293 If r1 = 0 and r2 = 9 at the end then P0's accesses must have executed
1294 in program order. If the second load had executed before the first
1295 then the x = 9 store must have been propagated to P0 before the first
1296 load executed, and so r1 would have been 9 rather than 0. In this
1297 case there is a prop link from P0's first read event to its second,
1298 because P1's store overwrote the value read by P0's first load, and
1299 P1's store propagated to P0 before P0's second load executed.
1301 Less trivial examples of prop all involve fences. Unlike the simple
1302 examples above, they can require that some instructions are executed
1303 out of program order. This next one should look familiar:
1305 int buf = 0, flag = 0;
1311 WRITE_ONCE(flag, 1);
1319 r1 = READ_ONCE(flag);
1320 r2 = READ_ONCE(buf);
1323 This is the MP pattern again, with an smp_wmb() fence between the two
1324 stores. If r1 = 1 and r2 = 0 at the end then there is a prop link
1325 from P1's second load to its first (backwards!). The reason is
1326 similar to the previous examples: The value P1 loads from buf gets
1327 overwritten by P0's store to buf, the fence guarantees that the store
1328 to buf will propagate to P1 before the store to flag does, and the
1329 store to flag propagates to P1 before P1 reads flag.
1331 The prop link says that in order to obtain the r1 = 1, r2 = 0 result,
1332 P1 must execute its second load before the first. Indeed, if the load
1333 from flag were executed first, then the buf = 1 store would already
1334 have propagated to P1 by the time P1's load from buf executed, so r2
1335 would have been 1 at the end, not 0. (The reasoning holds even for
1336 Alpha, although the details are more complicated and we will not go
1339 But what if we put an smp_rmb() fence between P1's loads? The fence
1340 would force the two loads to be executed in program order, and it
1341 would generate a cycle in the hb relation: The fence would create a ppo
1342 link (hence an hb link) from the first load to the second, and the
1343 prop relation would give an hb link from the second load to the first.
1344 Since an instruction can't execute before itself, we are forced to
1345 conclude that if an smp_rmb() fence is added, the r1 = 1, r2 = 0
1346 outcome is impossible -- as it should be.
1348 The formal definition of the prop relation involves a coe or fre link,
1349 followed by an arbitrary number of cumul-fence links, ending with an
1350 rfe link. You can concoct more exotic examples, containing more than
1351 one fence, although this quickly leads to diminishing returns in terms
1352 of complexity. For instance, here's an example containing a coe link
1353 followed by two cumul-fences and an rfe link, utilizing the fact that
1354 release fences are A-cumulative:
1378 smp_store_release(&z, 1);
1381 If x = 2, r0 = 1, and r2 = 1 after this code runs then there is a prop
1382 link from P0's store to its load. This is because P0's store gets
1383 overwritten by P1's store since x = 2 at the end (a coe link), the
1384 smp_wmb() ensures that P1's store to x propagates to P2 before the
1385 store to y does (the first cumul-fence), the store to y propagates to P2
1386 before P2's load and store execute, P2's smp_store_release()
1387 guarantees that the stores to x and y both propagate to P0 before the
1388 store to z does (the second cumul-fence), and P0's load executes after the
1389 store to z has propagated to P0 (an rfe link).
1391 In summary, the fact that the hb relation links memory access events
1392 in the order they execute means that it must not have cycles. This
1393 requirement is the content of the LKMM's "happens-before" axiom.
1395 The LKMM defines yet another relation connected to times of
1396 instruction execution, but it is not included in hb. It relies on the
1397 particular properties of strong fences, which we cover in the next
1401 THE PROPAGATES-BEFORE RELATION: pb
1402 ----------------------------------
1404 The propagates-before (pb) relation capitalizes on the special
1405 features of strong fences. It links two events E and F whenever some
1406 store is coherence-later than E and propagates to every CPU and to RAM
1407 before F executes. The formal definition requires that E be linked to
1408 F via a coe or fre link, an arbitrary number of cumul-fences, an
1409 optional rfe link, a strong fence, and an arbitrary number of hb
1410 links. Let's see how this definition works out.
1412 Consider first the case where E is a store (implying that the sequence
1413 of links begins with coe). Then there are events W, X, Y, and Z such
1416 E ->coe W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F,
1418 where the * suffix indicates an arbitrary number of links of the
1419 specified type, and the ? suffix indicates the link is optional (Y may
1420 be equal to X). Because of the cumul-fence links, we know that W will
1421 propagate to Y's CPU before X does, hence before Y executes and hence
1422 before the strong fence executes. Because this fence is strong, we
1423 know that W will propagate to every CPU and to RAM before Z executes.
1424 And because of the hb links, we know that Z will execute before F.
1425 Thus W, which comes later than E in the coherence order, will
1426 propagate to every CPU and to RAM before F executes.
1428 The case where E is a load is exactly the same, except that the first
1429 link in the sequence is fre instead of coe.
1431 The existence of a pb link from E to F implies that E must execute
1432 before F. To see why, suppose that F executed first. Then W would
1433 have propagated to E's CPU before E executed. If E was a store, the
1434 memory subsystem would then be forced to make E come after W in the
1435 coherence order, contradicting the fact that E ->coe W. If E was a
1436 load, the memory subsystem would then be forced to satisfy E's read
1437 request with the value stored by W or an even later store,
1438 contradicting the fact that E ->fre W.
1440 A good example illustrating how pb works is the SB pattern with strong
1463 If r0 = 0 at the end then there is a pb link from P0's load to P1's
1464 load: an fre link from P0's load to P1's store (which overwrites the
1465 value read by P0), and a strong fence between P1's store and its load.
1466 In this example, the sequences of cumul-fence and hb links are empty.
1467 Note that this pb link is not included in hb as an instance of prop,
1468 because it does not start and end on the same CPU.
1470 Similarly, if r1 = 0 at the end then there is a pb link from P1's load
1471 to P0's. This means that if both r1 and r2 were 0 there would be a
1472 cycle in pb, which is not possible since an instruction cannot execute
1473 before itself. Thus, adding smp_mb() fences to the SB pattern
1474 prevents the r0 = 0, r1 = 0 outcome.
1476 In summary, the fact that the pb relation links events in the order
1477 they execute means that it cannot have cycles. This requirement is
1478 the content of the LKMM's "propagation" axiom.
1481 RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb
1482 ------------------------------------------------------------------------
1484 RCU (Read-Copy-Update) is a powerful synchronization mechanism. It
1485 rests on two concepts: grace periods and read-side critical sections.
1487 A grace period is the span of time occupied by a call to
1488 synchronize_rcu(). A read-side critical section (or just critical
1489 section, for short) is a region of code delimited by rcu_read_lock()
1490 at the start and rcu_read_unlock() at the end. Critical sections can
1491 be nested, although we won't make use of this fact.
1493 As far as memory models are concerned, RCU's main feature is its
1494 Grace-Period Guarantee, which states that a critical section can never
1495 span a full grace period. In more detail, the Guarantee says:
1497 For any critical section C and any grace period G, at least
1498 one of the following statements must hold:
1500 (1) C ends before G does, and in addition, every store that
1501 propagates to C's CPU before the end of C must propagate to
1502 every CPU before G ends.
1504 (2) G starts before C does, and in addition, every store that
1505 propagates to G's CPU before the start of G must propagate
1506 to every CPU before C starts.
1508 In particular, it is not possible for a critical section to both start
1509 before and end after a grace period.
1511 Here is a simple example of RCU in action:
1532 The Grace Period Guarantee tells us that when this code runs, it will
1533 never end with r1 = 1 and r2 = 0. The reasoning is as follows. r1 = 1
1534 means that P0's store to x propagated to P1 before P1 called
1535 synchronize_rcu(), so P0's critical section must have started before
1536 P1's grace period, contrary to part (2) of the Guarantee. On the
1537 other hand, r2 = 0 means that P0's store to y, which occurs before the
1538 end of the critical section, did not propagate to P1 before the end of
1539 the grace period, contrary to part (1). Together the results violate
1542 In the kernel's implementations of RCU, the requirements for stores
1543 to propagate to every CPU are fulfilled by placing strong fences at
1544 suitable places in the RCU-related code. Thus, if a critical section
1545 starts before a grace period does then the critical section's CPU will
1546 execute an smp_mb() fence after the end of the critical section and
1547 some time before the grace period's synchronize_rcu() call returns.
1548 And if a critical section ends after a grace period does then the
1549 synchronize_rcu() routine will execute an smp_mb() fence at its start
1550 and some time before the critical section's opening rcu_read_lock()
1553 What exactly do we mean by saying that a critical section "starts
1554 before" or "ends after" a grace period? Some aspects of the meaning
1555 are pretty obvious, as in the example above, but the details aren't
1556 entirely clear. The LKMM formalizes this notion by means of the
1557 rcu-link relation. rcu-link encompasses a very general notion of
1558 "before": If E and F are RCU fence events (i.e., rcu_read_lock(),
1559 rcu_read_unlock(), or synchronize_rcu()) then among other things,
1560 E ->rcu-link F includes cases where E is po-before some memory-access
1561 event X, F is po-after some memory-access event Y, and we have any of
1562 X ->rfe Y, X ->co Y, or X ->fr Y.
1564 The formal definition of the rcu-link relation is more than a little
1565 obscure, and we won't give it here. It is closely related to the pb
1566 relation, and the details don't matter unless you want to comb through
1567 a somewhat lengthy formal proof. Pretty much all you need to know
1568 about rcu-link is the information in the preceding paragraph.
1570 The LKMM also defines the rcu-gp and rcu-rscsi relations. They bring
1571 grace periods and read-side critical sections into the picture, in the
1574 E ->rcu-gp F means that E and F are in fact the same event,
1575 and that event is a synchronize_rcu() fence (i.e., a grace
1578 E ->rcu-rscsi F means that E and F are the rcu_read_unlock()
1579 and rcu_read_lock() fence events delimiting some read-side
1580 critical section. (The 'i' at the end of the name emphasizes
1581 that this relation is "inverted": It links the end of the
1582 critical section to the start.)
1584 If we think of the rcu-link relation as standing for an extended
1585 "before", then X ->rcu-gp Y ->rcu-link Z roughly says that X is a
1586 grace period which ends before Z begins. (In fact it covers more than
1587 this, because it also includes cases where some store propagates to
1588 Z's CPU before Z begins but doesn't propagate to some other CPU until
1589 after X ends.) Similarly, X ->rcu-rscsi Y ->rcu-link Z says that X is
1590 the end of a critical section which starts before Z begins.
1592 The LKMM goes on to define the rcu-order relation as a sequence of
1593 rcu-gp and rcu-rscsi links separated by rcu-link links, in which the
1594 number of rcu-gp links is >= the number of rcu-rscsi links. For
1597 X ->rcu-gp Y ->rcu-link Z ->rcu-rscsi T ->rcu-link U ->rcu-gp V
1599 would imply that X ->rcu-order V, because this sequence contains two
1600 rcu-gp links and one rcu-rscsi link. (It also implies that
1601 X ->rcu-order T and Z ->rcu-order V.) On the other hand:
1603 X ->rcu-rscsi Y ->rcu-link Z ->rcu-rscsi T ->rcu-link U ->rcu-gp V
1605 does not imply X ->rcu-order V, because the sequence contains only
1606 one rcu-gp link but two rcu-rscsi links.
1608 The rcu-order relation is important because the Grace Period Guarantee
1609 means that rcu-order links act kind of like strong fences. In
1610 particular, E ->rcu-order F implies not only that E begins before F
1611 ends, but also that any write po-before E will propagate to every CPU
1612 before any instruction po-after F can execute. (However, it does not
1613 imply that E must execute before F; in fact, each synchronize_rcu()
1614 fence event is linked to itself by rcu-order as a degenerate case.)
1616 To prove this in full generality requires some intellectual effort.
1617 We'll consider just a very simple case:
1619 G ->rcu-gp W ->rcu-link Z ->rcu-rscsi F.
1621 This formula means that G and W are the same event (a grace period),
1622 and there are events X, Y and a read-side critical section C such that:
1624 1. G = W is po-before or equal to X;
1626 2. X comes "before" Y in some sense (including rfe, co and fr);
1628 3. Y is po-before Z;
1630 4. Z is the rcu_read_unlock() event marking the end of C;
1632 5. F is the rcu_read_lock() event marking the start of C.
1634 From 1 - 4 we deduce that the grace period G ends before the critical
1635 section C. Then part (2) of the Grace Period Guarantee says not only
1636 that G starts before C does, but also that any write which executes on
1637 G's CPU before G starts must propagate to every CPU before C starts.
1638 In particular, the write propagates to every CPU before F finishes
1639 executing and hence before any instruction po-after F can execute.
1640 This sort of reasoning can be extended to handle all the situations
1641 covered by rcu-order.
1643 The rcu-fence relation is a simple extension of rcu-order. While
1644 rcu-order only links certain fence events (calls to synchronize_rcu(),
1645 rcu_read_lock(), or rcu_read_unlock()), rcu-fence links any events
1646 that are separated by an rcu-order link. This is analogous to the way
1647 the strong-fence relation links events that are separated by an
1648 smp_mb() fence event (as mentioned above, rcu-order links act kind of
1649 like strong fences). Written symbolically, X ->rcu-fence Y means
1650 there are fence events E and F such that:
1652 X ->po E ->rcu-order F ->po Y.
1654 From the discussion above, we see this implies not only that X
1655 executes before Y, but also (if X is a store) that X propagates to
1656 every CPU before Y executes. Thus rcu-fence is sort of a
1657 "super-strong" fence: Unlike the original strong fences (smp_mb() and
1658 synchronize_rcu()), rcu-fence is able to link events on different
1659 CPUs. (Perhaps this fact should lead us to say that rcu-fence isn't
1660 really a fence at all!)
1662 Finally, the LKMM defines the RCU-before (rb) relation in terms of
1663 rcu-fence. This is done in essentially the same way as the pb
1664 relation was defined in terms of strong-fence. We will omit the
1665 details; the end result is that E ->rb F implies E must execute
1666 before F, just as E ->pb F does (and for much the same reasons).
1668 Putting this all together, the LKMM expresses the Grace Period
1669 Guarantee by requiring that the rb relation does not contain a cycle.
1670 Equivalently, this "rcu" axiom requires that there are no events E
1671 and F with E ->rcu-link F ->rcu-order E. Or to put it a third way,
1672 the axiom requires that there are no cycles consisting of rcu-gp and
1673 rcu-rscsi alternating with rcu-link, where the number of rcu-gp links
1674 is >= the number of rcu-rscsi links.
1676 Justifying the axiom isn't easy, but it is in fact a valid
1677 formalization of the Grace Period Guarantee. We won't attempt to go
1678 through the detailed argument, but the following analysis gives a
1679 taste of what is involved. Suppose both parts of the Guarantee are
1680 violated: A critical section starts before a grace period, and some
1681 store propagates to the critical section's CPU before the end of the
1682 critical section but doesn't propagate to some other CPU until after
1683 the end of the grace period.
1685 Putting symbols to these ideas, let L and U be the rcu_read_lock() and
1686 rcu_read_unlock() fence events delimiting the critical section in
1687 question, and let S be the synchronize_rcu() fence event for the grace
1688 period. Saying that the critical section starts before S means there
1689 are events Q and R where Q is po-after L (which marks the start of the
1690 critical section), Q is "before" R in the sense used by the rcu-link
1691 relation, and R is po-before the grace period S. Thus we have:
1695 Let W be the store mentioned above, let Y come before the end of the
1696 critical section and witness that W propagates to the critical
1697 section's CPU by reading from W, and let Z on some arbitrary CPU be a
1698 witness that W has not propagated to that CPU, where Z happens after
1699 some event X which is po-after S. Symbolically, this amounts to:
1701 S ->po X ->hb* Z ->fr W ->rf Y ->po U.
1703 The fr link from Z to W indicates that W has not propagated to Z's CPU
1704 at the time that Z executes. From this, it can be shown (see the
1705 discussion of the rcu-link relation earlier) that S and U are related
1710 Since S is a grace period we have S ->rcu-gp S, and since L and U are
1711 the start and end of the critical section C we have U ->rcu-rscsi L.
1712 From this we obtain:
1714 S ->rcu-gp S ->rcu-link U ->rcu-rscsi L ->rcu-link S,
1716 a forbidden cycle. Thus the "rcu" axiom rules out this violation of
1717 the Grace Period Guarantee.
1719 For something a little more down-to-earth, let's see how the axiom
1720 works out in practice. Consider the RCU code example from above, this
1721 time with statement labels added:
1728 X: WRITE_ONCE(x, 1);
1729 Y: WRITE_ONCE(y, 1);
1730 U: rcu_read_unlock();
1737 Z: r1 = READ_ONCE(x);
1738 S: synchronize_rcu();
1739 W: r2 = READ_ONCE(y);
1743 If r2 = 0 at the end then P0's store at Y overwrites the value that
1744 P1's load at W reads from, so we have W ->fre Y. Since S ->po W and
1745 also Y ->po U, we get S ->rcu-link U. In addition, S ->rcu-gp S
1746 because S is a grace period.
1748 If r1 = 1 at the end then P1's load at Z reads from P0's store at X,
1749 so we have X ->rfe Z. Together with L ->po X and Z ->po S, this
1750 yields L ->rcu-link S. And since L and U are the start and end of a
1751 critical section, we have U ->rcu-rscsi L.
1753 Then U ->rcu-rscsi L ->rcu-link S ->rcu-gp S ->rcu-link U is a
1754 forbidden cycle, violating the "rcu" axiom. Hence the outcome is not
1755 allowed by the LKMM, as we would expect.
1757 For contrast, let's see what can happen in a more complicated example:
1765 L0: rcu_read_lock();
1768 U0: rcu_read_unlock();
1776 S1: synchronize_rcu();
1784 L2: rcu_read_lock();
1787 U2: rcu_read_unlock();
1790 If r0 = r1 = r2 = 1 at the end, then similar reasoning to before shows
1791 that U0 ->rcu-rscsi L0 ->rcu-link S1 ->rcu-gp S1 ->rcu-link U2 ->rcu-rscsi
1792 L2 ->rcu-link U0. However this cycle is not forbidden, because the
1793 sequence of relations contains fewer instances of rcu-gp (one) than of
1794 rcu-rscsi (two). Consequently the outcome is allowed by the LKMM.
1795 The following instruction timing diagram shows how it might actually
1799 -------------------- -------------------- --------------------
1803 synchronize_rcu() starts
1808 synchronize_rcu() ends
1813 This requires P0 and P2 to execute their loads and stores out of
1814 program order, but of course they are allowed to do so. And as you
1815 can see, the Grace Period Guarantee is not violated: The critical
1816 section in P0 both starts before P1's grace period does and ends
1817 before it does, and the critical section in P2 both starts after P1's
1818 grace period does and ends after it does.
1820 Addendum: The LKMM now supports SRCU (Sleepable Read-Copy-Update) in
1821 addition to normal RCU. The ideas involved are much the same as
1822 above, with new relations srcu-gp and srcu-rscsi added to represent
1823 SRCU grace periods and read-side critical sections. There is a
1824 restriction on the srcu-gp and srcu-rscsi links that can appear in an
1825 rcu-order sequence (the srcu-rscsi links must be paired with srcu-gp
1826 links having the same SRCU domain with proper nesting); the details
1827 are relatively unimportant.
1833 The LKMM includes locking. In fact, there is special code for locking
1834 in the formal model, added in order to make tools run faster.
1835 However, this special code is intended to be more or less equivalent
1836 to concepts we have already covered. A spinlock_t variable is treated
1837 the same as an int, and spin_lock(&s) is treated almost the same as:
1839 while (cmpxchg_acquire(&s, 0, 1) != 0)
1842 This waits until s is equal to 0 and then atomically sets it to 1,
1843 and the read part of the cmpxchg operation acts as an acquire fence.
1844 An alternate way to express the same thing would be:
1846 r = xchg_acquire(&s, 1);
1848 along with a requirement that at the end, r = 0. Similarly,
1849 spin_trylock(&s) is treated almost the same as:
1851 return !cmpxchg_acquire(&s, 0, 1);
1853 which atomically sets s to 1 if it is currently equal to 0 and returns
1854 true if it succeeds (the read part of the cmpxchg operation acts as an
1855 acquire fence only if the operation is successful). spin_unlock(&s)
1856 is treated almost the same as:
1858 smp_store_release(&s, 0);
1860 The "almost" qualifiers above need some explanation. In the LKMM, the
1861 store-release in a spin_unlock() and the load-acquire which forms the
1862 first half of the atomic rmw update in a spin_lock() or a successful
1863 spin_trylock() -- we can call these things lock-releases and
1864 lock-acquires -- have two properties beyond those of ordinary releases
1867 First, when a lock-acquire reads from or is po-after a lock-release,
1868 the LKMM requires that every instruction po-before the lock-release
1869 must execute before any instruction po-after the lock-acquire. This
1870 would naturally hold if the release and acquire operations were on
1871 different CPUs and accessed the same lock variable, but the LKMM says
1872 it also holds when they are on the same CPU, even if they access
1873 different lock variables. For example:
1897 Here the second spin_lock() is po-after the first spin_unlock(), and
1898 therefore the load of x must execute before the load of y, even though
1899 the two locking operations use different locks. Thus we cannot have
1900 r1 = 1 and r2 = 0 at the end (this is an instance of the MP pattern).
1902 This requirement does not apply to ordinary release and acquire
1903 fences, only to lock-related operations. For instance, suppose P0()
1904 in the example had been written as:
1911 smp_store_release(&s, 1);
1912 r3 = smp_load_acquire(&s);
1916 Then the CPU would be allowed to forward the s = 1 value from the
1917 smp_store_release() to the smp_load_acquire(), executing the
1918 instructions in the following order:
1920 r3 = smp_load_acquire(&s); // Obtains r3 = 1
1923 smp_store_release(&s, 1); // Value is forwarded
1925 and thus it could load y before x, obtaining r2 = 0 and r1 = 1.
1927 Second, when a lock-acquire reads from or is po-after a lock-release,
1928 and some other stores W and W' occur po-before the lock-release and
1929 po-after the lock-acquire respectively, the LKMM requires that W must
1930 propagate to each CPU before W' does. For example, consider:
1961 If r1 = 1 at the end then the spin_lock() in P1 must have read from
1962 the spin_unlock() in P0. Hence the store to x must propagate to P2
1963 before the store to y does, so we cannot have r2 = 1 and r3 = 0. But
1964 if P1 had used a lock variable different from s, the writes could have
1965 propagated in either order. (On the other hand, if the code in P0 and
1966 P1 had all executed on a single CPU, as in the example before this
1967 one, then the writes would have propagated in order even if the two
1968 critical sections used different lock variables.)
1970 These two special requirements for lock-release and lock-acquire do
1971 not arise from the operational model. Nevertheless, kernel developers
1972 have come to expect and rely on them because they do hold on all
1973 architectures supported by the Linux kernel, albeit for various
1977 PLAIN ACCESSES AND DATA RACES
1978 -----------------------------
1980 In the LKMM, memory accesses such as READ_ONCE(x), atomic_inc(&y),
1981 smp_load_acquire(&z), and so on are collectively referred to as
1982 "marked" accesses, because they are all annotated with special
1983 operations of one kind or another. Ordinary C-language memory
1984 accesses such as x or y = 0 are simply called "plain" accesses.
1986 Early versions of the LKMM had nothing to say about plain accesses.
1987 The C standard allows compilers to assume that the variables affected
1988 by plain accesses are not concurrently read or written by any other
1989 threads or CPUs. This leaves compilers free to implement all manner
1990 of transformations or optimizations of code containing plain accesses,
1991 making such code very difficult for a memory model to handle.
1993 Here is just one example of a possible pitfall:
2005 r2 = READ_ONCE(*r1);
2010 WRITE_ONCE(x, NULL);
2013 On the face of it, one would expect that when this code runs, the only
2014 possible final values for r2 are 6 and 0, depending on whether or not
2015 P1's store to x propagates to P0 before P0's load from x executes.
2016 But since P0's load from x is a plain access, the compiler may decide
2017 to carry out the load twice (for the comparison against NULL, then again
2018 for the READ_ONCE()) and eliminate the temporary variable r1. The
2019 object code generated for P0 could therefore end up looking rather
2030 And now it is obvious that this code runs the risk of dereferencing a
2031 NULL pointer, because P1's store to x might propagate to P0 after the
2032 test against NULL has been made but before the READ_ONCE() executes.
2033 If the original code had said "r1 = READ_ONCE(x)" instead of "r1 = x",
2034 the compiler would not have performed this optimization and there
2035 would be no possibility of a NULL-pointer dereference.
2037 Given the possibility of transformations like this one, the LKMM
2038 doesn't try to predict all possible outcomes of code containing plain
2039 accesses. It is instead content to determine whether the code
2040 violates the compiler's assumptions, which would render the ultimate
2043 In technical terms, the compiler is allowed to assume that when the
2044 program executes, there will not be any data races. A "data race"
2045 occurs when there are two memory accesses such that:
2047 1. they access the same location,
2049 2. at least one of them is a store,
2051 3. at least one of them is plain,
2053 4. they occur on different CPUs (or in different threads on the
2056 5. they execute concurrently.
2058 In the literature, two accesses are said to "conflict" if they satisfy
2059 1 and 2 above. We'll go a little farther and say that two accesses
2060 are "race candidates" if they satisfy 1 - 4. Thus, whether or not two
2061 race candidates actually do race in a given execution depends on
2062 whether they are concurrent.
2064 The LKMM tries to determine whether a program contains race candidates
2065 which may execute concurrently; if it does then the LKMM says there is
2066 a potential data race and makes no predictions about the program's
2069 Determining whether two accesses are race candidates is easy; you can
2070 see that all the concepts involved in the definition above are already
2071 part of the memory model. The hard part is telling whether they may
2072 execute concurrently. The LKMM takes a conservative attitude,
2073 assuming that accesses may be concurrent unless it can prove they
2076 If two memory accesses aren't concurrent then one must execute before
2077 the other. Therefore the LKMM decides two accesses aren't concurrent
2078 if they can be connected by a sequence of hb, pb, and rb links
2079 (together referred to as xb, for "executes before"). However, there
2080 are two complicating factors.
2082 If X is a load and X executes before a store Y, then indeed there is
2083 no danger of X and Y being concurrent. After all, Y can't have any
2084 effect on the value obtained by X until the memory subsystem has
2085 propagated Y from its own CPU to X's CPU, which won't happen until
2086 some time after Y executes and thus after X executes. But if X is a
2087 store, then even if X executes before Y it is still possible that X
2088 will propagate to Y's CPU just as Y is executing. In such a case X
2089 could very well interfere somehow with Y, and we would have to
2090 consider X and Y to be concurrent.
2092 Therefore when X is a store, for X and Y to be non-concurrent the LKMM
2093 requires not only that X must execute before Y but also that X must
2094 propagate to Y's CPU before Y executes. (Or vice versa, of course, if
2095 Y executes before X -- then Y must propagate to X's CPU before X
2096 executes if Y is a store.) This is expressed by the visibility
2097 relation (vis), where X ->vis Y is defined to hold if there is an
2098 intermediate event Z such that:
2100 X is connected to Z by a possibly empty sequence of
2101 cumul-fence links followed by an optional rfe link (if none of
2102 these links are present, X and Z are the same event),
2106 Z is connected to Y by a strong-fence link followed by a
2107 possibly empty sequence of xb links,
2111 Z is on the same CPU as Y and is connected to Y by a possibly
2112 empty sequence of xb links (again, if the sequence is empty it
2113 means Z and Y are the same event).
2115 The motivations behind this definition are straightforward:
2117 cumul-fence memory barriers force stores that are po-before
2118 the barrier to propagate to other CPUs before stores that are
2119 po-after the barrier.
2121 An rfe link from an event W to an event R says that R reads
2122 from W, which certainly means that W must have propagated to
2123 R's CPU before R executed.
2125 strong-fence memory barriers force stores that are po-before
2126 the barrier, or that propagate to the barrier's CPU before the
2127 barrier executes, to propagate to all CPUs before any events
2128 po-after the barrier can execute.
2130 To see how this works out in practice, consider our old friend, the MP
2131 pattern (with fences and statement labels, but without the conditional
2134 int buf = 0, flag = 0;
2138 X: WRITE_ONCE(buf, 1);
2140 W: WRITE_ONCE(flag, 1);
2148 Z: r1 = READ_ONCE(flag);
2150 Y: r2 = READ_ONCE(buf);
2153 The smp_wmb() memory barrier gives a cumul-fence link from X to W, and
2154 assuming r1 = 1 at the end, there is an rfe link from W to Z. This
2155 means that the store to buf must propagate from P0 to P1 before Z
2156 executes. Next, Z and Y are on the same CPU and the smp_rmb() fence
2157 provides an xb link from Z to Y (i.e., it forces Z to execute before
2158 Y). Therefore we have X ->vis Y: X must propagate to Y's CPU before Y
2161 The second complicating factor mentioned above arises from the fact
2162 that when we are considering data races, some of the memory accesses
2163 are plain. Now, although we have not said so explicitly, up to this
2164 point most of the relations defined by the LKMM (ppo, hb, prop,
2165 cumul-fence, pb, and so on -- including vis) apply only to marked
2168 There are good reasons for this restriction. The compiler is not
2169 allowed to apply fancy transformations to marked accesses, and
2170 consequently each such access in the source code corresponds more or
2171 less directly to a single machine instruction in the object code. But
2172 plain accesses are a different story; the compiler may combine them,
2173 split them up, duplicate them, eliminate them, invent new ones, and
2174 who knows what else. Seeing a plain access in the source code tells
2175 you almost nothing about what machine instructions will end up in the
2178 Fortunately, the compiler isn't completely free; it is subject to some
2179 limitations. For one, it is not allowed to introduce a data race into
2180 the object code if the source code does not already contain a data
2181 race (if it could, memory models would be useless and no multithreaded
2182 code would be safe!). For another, it cannot move a plain access past
2185 A compiler barrier is a kind of fence, but as the name implies, it
2186 only affects the compiler; it does not necessarily have any effect on
2187 how instructions are executed by the CPU. In Linux kernel source
2188 code, the barrier() function is a compiler barrier. It doesn't give
2189 rise directly to any machine instructions in the object code; rather,
2190 it affects how the compiler generates the rest of the object code.
2191 Given source code like this:
2193 ... some memory accesses ...
2195 ... some other memory accesses ...
2197 the barrier() function ensures that the machine instructions
2198 corresponding to the first group of accesses will all end po-before
2199 any machine instructions corresponding to the second group of accesses
2200 -- even if some of the accesses are plain. (Of course, the CPU may
2201 then execute some of those accesses out of program order, but we
2202 already know how to deal with such issues.) Without the barrier()
2203 there would be no such guarantee; the two groups of accesses could be
2204 intermingled or even reversed in the object code.
2206 The LKMM doesn't say much about the barrier() function, but it does
2207 require that all fences are also compiler barriers. In addition, it
2208 requires that the ordering properties of memory barriers such as
2209 smp_rmb() or smp_store_release() apply to plain accesses as well as to
2212 This is the key to analyzing data races. Consider the MP pattern
2213 again, now using plain accesses for buf:
2215 int buf = 0, flag = 0;
2221 X: WRITE_ONCE(flag, 1);
2229 Y: r1 = READ_ONCE(flag);
2236 This program does not contain a data race. Although the U and V
2237 accesses are race candidates, the LKMM can prove they are not
2238 concurrent as follows:
2240 The smp_wmb() fence in P0 is both a compiler barrier and a
2241 cumul-fence. It guarantees that no matter what hash of
2242 machine instructions the compiler generates for the plain
2243 access U, all those instructions will be po-before the fence.
2244 Consequently U's store to buf, no matter how it is carried out
2245 at the machine level, must propagate to P1 before X's store to
2248 X and Y are both marked accesses. Hence an rfe link from X to
2249 Y is a valid indicator that X propagated to P1 before Y
2250 executed, i.e., X ->vis Y. (And if there is no rfe link then
2251 r1 will be 0, so V will not be executed and ipso facto won't
2254 The smp_rmb() fence in P1 is a compiler barrier as well as a
2255 fence. It guarantees that all the machine-level instructions
2256 corresponding to the access V will be po-after the fence, and
2257 therefore any loads among those instructions will execute
2258 after the fence does and hence after Y does.
2260 Thus U's store to buf is forced to propagate to P1 before V's load
2261 executes (assuming V does execute), ruling out the possibility of a
2262 data race between them.
2264 This analysis illustrates how the LKMM deals with plain accesses in
2265 general. Suppose R is a plain load and we want to show that R
2266 executes before some marked access E. We can do this by finding a
2267 marked access X such that R and X are ordered by a suitable fence and
2268 X ->xb* E. If E was also a plain access, we would also look for a
2269 marked access Y such that X ->xb* Y, and Y and E are ordered by a
2270 fence. We describe this arrangement by saying that R is
2271 "post-bounded" by X and E is "pre-bounded" by Y.
2273 In fact, we go one step further: Since R is a read, we say that R is
2274 "r-post-bounded" by X. Similarly, E would be "r-pre-bounded" or
2275 "w-pre-bounded" by Y, depending on whether E was a store or a load.
2276 This distinction is needed because some fences affect only loads
2277 (i.e., smp_rmb()) and some affect only stores (smp_wmb()); otherwise
2278 the two types of bounds are the same. And as a degenerate case, we
2279 say that a marked access pre-bounds and post-bounds itself (e.g., if R
2280 above were a marked load then X could simply be taken to be R itself.)
2282 The need to distinguish between r- and w-bounding raises yet another
2283 issue. When the source code contains a plain store, the compiler is
2284 allowed to put plain loads of the same location into the object code.
2285 For example, given the source code:
2289 the compiler is theoretically allowed to generate object code that
2295 thereby adding a load (and possibly replacing the store entirely).
2296 For this reason, whenever the LKMM requires a plain store to be
2297 w-pre-bounded or w-post-bounded by a marked access, it also requires
2298 the store to be r-pre-bounded or r-post-bounded, so as to handle cases
2299 where the compiler adds a load.
2301 (This may be overly cautious. We don't know of any examples where a
2302 compiler has augmented a store with a load in this fashion, and the
2303 Linux kernel developers would probably fight pretty hard to change a
2304 compiler if it ever did this. Still, better safe than sorry.)
2306 Incidentally, the other tranformation -- augmenting a plain load by
2307 adding in a store to the same location -- is not allowed. This is
2308 because the compiler cannot know whether any other CPUs might perform
2309 a concurrent load from that location. Two concurrent loads don't
2310 constitute a race (they can't interfere with each other), but a store
2311 does race with a concurrent load. Thus adding a store might create a
2312 data race where one was not already present in the source code,
2313 something the compiler is forbidden to do. Augmenting a store with a
2314 load, on the other hand, is acceptable because doing so won't create a
2315 data race unless one already existed.
2317 The LKMM includes a second way to pre-bound plain accesses, in
2318 addition to fences: an address dependency from a marked load. That
2319 is, in the sequence:
2324 the LKMM says that the marked load of ptr pre-bounds the plain load of
2325 *p; the marked load must execute before any of the machine
2326 instructions corresponding to the plain load. This is a reasonable
2327 stipulation, since after all, the CPU can't perform the load of *p
2328 until it knows what value p will hold. Furthermore, without some
2329 assumption like this one, some usages typical of RCU would count as
2330 data races. For example:
2338 rcu_assign_pointer(ptr, &b);
2347 p = rcu_dereference(ptr);
2352 (In this example the rcu_read_lock() and rcu_read_unlock() calls don't
2353 really do anything, because there aren't any grace periods. They are
2354 included merely for the sake of good form; typically P0 would call
2355 synchronize_rcu() somewhere after the rcu_assign_pointer().)
2357 rcu_assign_pointer() performs a store-release, so the plain store to b
2358 is definitely w-post-bounded before the store to ptr, and the two
2359 stores will propagate to P1 in that order. However, rcu_dereference()
2360 is only equivalent to READ_ONCE(). While it is a marked access, it is
2361 not a fence or compiler barrier. Hence the only guarantee we have
2362 that the load of ptr in P1 is r-pre-bounded before the load of *p
2363 (thus avoiding a race) is the assumption about address dependencies.
2365 This is a situation where the compiler can undermine the memory model,
2366 and a certain amount of care is required when programming constructs
2367 like this one. In particular, comparisons between the pointer and
2368 other known addresses can cause trouble. If you have something like:
2370 p = rcu_dereference(ptr);
2374 then the compiler just might generate object code resembling:
2376 p = rcu_dereference(ptr);
2383 p = rcu_dereference(ptr);
2387 which would invalidate the memory model's assumption, since the CPU
2388 could now perform the load of x before the load of ptr (there might be
2389 a control dependency but no address dependency at the machine level).
2391 Finally, it turns out there is a situation in which a plain write does
2392 not need to be w-post-bounded: when it is separated from the other
2393 race-candidate access by a fence. At first glance this may seem
2394 impossible. After all, to be race candidates the two accesses must
2395 be on different CPUs, and fences don't link events on different CPUs.
2396 Well, normal fences don't -- but rcu-fence can! Here's an example:
2410 if (READ_ONCE(x) == 0)
2415 Do the plain stores to y race? Clearly not if P1 reads a non-zero
2416 value for x, so let's assume the READ_ONCE(x) does obtain 0. This
2417 means that the read-side critical section in P1 must finish executing
2418 before the grace period in P0 does, because RCU's Grace-Period
2419 Guarantee says that otherwise P0's store to x would have propagated to
2420 P1 before the critical section started and so would have been visible
2421 to the READ_ONCE(). (Another way of putting it is that the fre link
2422 from the READ_ONCE() to the WRITE_ONCE() gives rise to an rcu-link
2423 between those two events.)
2425 This means there is an rcu-fence link from P1's "y = 2" store to P0's
2426 "y = 3" store, and consequently the first must propagate from P1 to P0
2427 before the second can execute. Therefore the two stores cannot be
2428 concurrent and there is no race, even though P1's plain store to y
2429 isn't w-post-bounded by any marked accesses.
2431 Putting all this material together yields the following picture. For
2432 race-candidate stores W and W', where W ->co W', the LKMM says the
2433 stores don't race if W can be linked to W' by a
2435 w-post-bounded ; vis ; w-pre-bounded
2437 sequence. If W is plain then they also have to be linked by an
2439 r-post-bounded ; xb* ; w-pre-bounded
2441 sequence, and if W' is plain then they also have to be linked by a
2443 w-post-bounded ; vis ; r-pre-bounded
2445 sequence. For race-candidate load R and store W, the LKMM says the
2446 two accesses don't race if R can be linked to W by an
2448 r-post-bounded ; xb* ; w-pre-bounded
2450 sequence or if W can be linked to R by a
2452 w-post-bounded ; vis ; r-pre-bounded
2454 sequence. For the cases involving a vis link, the LKMM also accepts
2455 sequences in which W is linked to W' or R by a
2457 strong-fence ; xb* ; {w and/or r}-pre-bounded
2459 sequence with no post-bounding, and in every case the LKMM also allows
2460 the link simply to be a fence with no bounding at all. If no sequence
2461 of the appropriate sort exists, the LKMM says that the accesses race.
2463 There is one more part of the LKMM related to plain accesses (although
2464 not to data races) we should discuss. Recall that many relations such
2465 as hb are limited to marked accesses only. As a result, the
2466 happens-before, propagates-before, and rcu axioms (which state that
2467 various relation must not contain a cycle) doesn't apply to plain
2468 accesses. Nevertheless, we do want to rule out such cycles, because
2469 they don't make sense even for plain accesses.
2471 To this end, the LKMM imposes three extra restrictions, together
2472 called the "plain-coherence" axiom because of their resemblance to the
2473 rules used by the operational model to ensure cache coherence (that
2474 is, the rules governing the memory subsystem's choice of a store to
2475 satisfy a load request and its determination of where a store will
2476 fall in the coherence order):
2478 If R and W are race candidates and it is possible to link R to
2479 W by one of the xb* sequences listed above, then W ->rfe R is
2480 not allowed (i.e., a load cannot read from a store that it
2481 executes before, even if one or both is plain).
2483 If W and R are race candidates and it is possible to link W to
2484 R by one of the vis sequences listed above, then R ->fre W is
2485 not allowed (i.e., if a store is visible to a load then the
2486 load must read from that store or one coherence-after it).
2488 If W and W' are race candidates and it is possible to link W
2489 to W' by one of the vis sequences listed above, then W' ->co W
2490 is not allowed (i.e., if one store is visible to a second then
2491 the second must come after the first in the coherence order).
2493 This is the extent to which the LKMM deals with plain accesses.
2494 Perhaps it could say more (for example, plain accesses might
2495 contribute to the ppo relation), but at the moment it seems that this
2496 minimal, conservative approach is good enough.
2502 This section covers material that didn't quite fit anywhere in the
2505 The descriptions in this document don't always match the formal
2506 version of the LKMM exactly. For example, the actual formal
2507 definition of the prop relation makes the initial coe or fre part
2508 optional, and it doesn't require the events linked by the relation to
2509 be on the same CPU. These differences are very unimportant; indeed,
2510 instances where the coe/fre part of prop is missing are of no interest
2511 because all the other parts (fences and rfe) are already included in
2512 hb anyway, and where the formal model adds prop into hb, it includes
2513 an explicit requirement that the events being linked are on the same
2516 Another minor difference has to do with events that are both memory
2517 accesses and fences, such as those corresponding to smp_load_acquire()
2518 calls. In the formal model, these events aren't actually both reads
2519 and fences; rather, they are read events with an annotation marking
2520 them as acquires. (Or write events annotated as releases, in the case
2521 smp_store_release().) The final effect is the same.
2523 Although we didn't mention it above, the instruction execution
2524 ordering provided by the smp_rmb() fence doesn't apply to read events
2525 that are part of a non-value-returning atomic update. For instance,
2532 it is not guaranteed that the load from y will execute after the
2533 update to x. This is because the ARMv8 architecture allows
2534 non-value-returning atomic operations effectively to be executed off
2535 the CPU. Basically, the CPU tells the memory subsystem to increment
2536 x, and then the increment is carried out by the memory hardware with
2537 no further involvement from the CPU. Since the CPU doesn't ever read
2538 the value of x, there is nothing for the smp_rmb() fence to act on.
2540 The LKMM defines a few extra synchronization operations in terms of
2541 things we have already covered. In particular, rcu_dereference() is
2542 treated as READ_ONCE() and rcu_assign_pointer() is treated as
2543 smp_store_release() -- which is basically how the Linux kernel treats
2546 Although we said that plain accesses are not linked by the ppo
2547 relation, they do contribute to it indirectly. Namely, when there is
2548 an address dependency from a marked load R to a plain store W,
2549 followed by smp_wmb() and then a marked store W', the LKMM creates a
2550 ppo link from R to W'. The reasoning behind this is perhaps a little
2551 shaky, but essentially it says there is no way to generate object code
2552 for this source code in which W' could execute before R. Just as with
2553 pre-bounding by address dependencies, it is possible for the compiler
2554 to undermine this relation if sufficient care is not taken.
2556 There are a few oddball fences which need special treatment:
2557 smp_mb__before_atomic(), smp_mb__after_atomic(), and
2558 smp_mb__after_spinlock(). The LKMM uses fence events with special
2559 annotations for them; they act as strong fences just like smp_mb()
2560 except for the sets of events that they order. Instead of ordering
2561 all po-earlier events against all po-later events, as smp_mb() does,
2562 they behave as follows:
2564 smp_mb__before_atomic() orders all po-earlier events against
2565 po-later atomic updates and the events following them;
2567 smp_mb__after_atomic() orders po-earlier atomic updates and
2568 the events preceding them against all po-later events;
2570 smp_mb__after_spinlock() orders po-earlier lock acquisition
2571 events and the events preceding them against all po-later
2574 Interestingly, RCU and locking each introduce the possibility of
2575 deadlock. When faced with code sequences such as:
2588 what does the LKMM have to say? Answer: It says there are no allowed
2589 executions at all, which makes sense. But this can also lead to
2590 misleading results, because if a piece of code has multiple possible
2591 executions, some of which deadlock, the model will report only on the
2592 non-deadlocking executions. For example:
2607 if (READ_ONCE(x) > 0) {
2614 Is it possible to end up with r0 = 36 at the end? The LKMM will tell
2615 you it is not, but the model won't mention that this is because P1
2616 will self-deadlock in the executions where it stores 36 in y.