1 Explanation of the Linux-Kernel Memory Consist
2 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3
4 :Author: Alan Stern <stern@rowland.harvard.edu>
5 :Created: October 2017
6
7 .. Contents
8
9 1. INTRODUCTION
10 2. BACKGROUND
11 3. A SIMPLE EXAMPLE
12 4. A SELECTION OF MEMORY MODELS
13 5. ORDERING AND CYCLES
14 6. EVENTS
15 7. THE PROGRAM ORDER RELATION: po AND po-loc
16 8. A WARNING
17 9. DEPENDENCY RELATIONS: data, addr, and ctr
18 10. THE READS-FROM RELATION: rf, rfi, and rf
19 11. CACHE COHERENCE AND THE COHERENCE ORDER
20 12. THE FROM-READS RELATION: fr, fri, and fr
21 13. AN OPERATIONAL MODEL
22 14. PROPAGATION ORDER RELATION: cumul-fence
23 15. DERIVATION OF THE LKMM FROM THE OPERATIO
24 16. SEQUENTIAL CONSISTENCY PER VARIABLE
25 17. ATOMIC UPDATES: rmw
26 18. THE PRESERVED PROGRAM ORDER RELATION: pp
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-rsc
31 23. SRCU READ-SIDE CRITICAL SECTIONS
32 24. LOCKING
33 25. PLAIN ACCESSES AND DATA RACES
34 26. ODDS AND ENDS
35
36
37
38 INTRODUCTION
39 ------------
40
41 The Linux-kernel memory consistency model (LKM
42 obscure. This is particularly evident if you
43 linux-kernel.bell and linux-kernel.cat files t
44 version of the model; they are extremely terse
45 far from clear.
46
47 This document describes the ideas underlying t
48 for people who want to understand how the mode
49 not go into the details of the code in the .be
50 rather, it explains in English what the code e
51
52 Sections 2 (BACKGROUND) through 5 (ORDERING AN
53 toward beginners; they explain what memory con
54 the basic notions shared by all such models.
55 with these concepts can skim or skip over them
56 through 12 (THE FROM_READS RELATION) describe
57 relations used in many models. Starting in Se
58 MODEL), the workings of the LKMM itself are co
59
60 Warning: The code examples in this document ar
61 proper format for litmus tests. They don't in
62 initializations are not enclosed in braces, th
63 not passed by pointers, and they don't have an
64 end. Converting them to the right format is l
65 the reader.
66
67
68 BACKGROUND
69 ----------
70
71 A memory consistency model (or just memory mod
72 something which predicts, given a piece of com
73 particular kind of system, what values may be
74 load instructions. The LKMM makes these predi
75 as part of the Linux kernel.
76
77 In practice, people tend to use memory models
78 That is, given a piece of code and a collectio
79 for the loads, the model will predict whether
80 code to run in such a way that the loads will
81 specified values. Of course, this is just ano
82 the same idea.
83
84 For code running on a uniprocessor system, the
85 Each load instruction must obtain the value wr
86 store instruction accessing the same location
87 factors such as DMA and mixed-size accesses.)
88 systems, with multiple CPUs making concurrent
89 memory locations, things aren't so simple.
90
91 Different architectures have differing memory
92 kernel supports a variety of architectures. T
93 permissive, in the sense that any behavior all
94 architectures also has to be allowed by the LK
95
96
97 A SIMPLE EXAMPLE
98 ----------------
99
100 Here is a simple example to illustrate the bas
101 some code running as part of a device driver f
102 driver might contain an interrupt handler whic
103 device, stores it in a buffer, and sets a flag
104 is full. Running concurrently on a different
105 the driver code being executed by a process in
106 system call. This code tests the flag to see
107 ready, and if it is, copies the data back to u
108 and the flag are memory locations shared betwe
109
110 We can abstract out the important pieces of th
111 (the reason for using WRITE_ONCE() and READ_ON
112 assignment statements is discussed later):
113
114 int buf = 0, flag = 0;
115
116 P0()
117 {
118 WRITE_ONCE(buf, 1);
119 WRITE_ONCE(flag, 1);
120 }
121
122 P1()
123 {
124 int r1;
125 int r2 = 0;
126
127 r1 = READ_ONCE(flag);
128 if (r1)
129 r2 = READ_ONCE(buf);
130 }
131
132 Here the P0() function represents the interrup
133 CPU and P1() represents the read() routine run
134 value 1 stored in buf represents input data co
135 Thus, P0 stores the data in buf and then sets
136 reads flag into the private variable r1, and i
137 data from buf into a second private variable r
138 userspace. (Presumably if flag is not set the
139 while and try again.)
140
141 This pattern of memory accesses, where one CPU
142 shared memory locations and another CPU loads
143 the opposite order, is widely known as the "Me
144 pattern. It is typical of memory access patte
145
146 Please note that this example code is a simpli
147 buffers are usually larger than a single integ
148 usually use sleep and wakeup mechanisms rather
149 completion, and real code generally doesn't bo
150 private variables before using them. All that
151 the idea here is simply to illustrate the over
152 accesses by the CPUs.
153
154 A memory model will predict what values P1 mig
155 from flag and buf, or equivalently, what value
156 with after the code has finished running.
157
158 Some predictions are trivial. For instance, n
159 predict that r1 = 42 or r2 = -7, because neith
160 gets stored in flag or buf.
161
162 Some nontrivial predictions are nonetheless qu
163 instance, P1 might run entirely before P0 begi
164 r2 will both be 0 at the end. Or P0 might run
165 begins, in which case r1 and r2 will both be 1
166
167 The interesting predictions concern what might
168 routines run concurrently. One possibility is
169 store to buf but before the store to flag. In
170 will again both be 0. (If P1 had been designe
171 unconditionally then we would instead have r1
172
173 However, the most interesting possibility is w
174 If this were to occur it would mean the driver
175 incorrect data would get sent to the user: 0 i
176 happens, the LKMM does predict this outcome ca
177 driver code shown above is indeed buggy.
178
179
180 A SELECTION OF MEMORY MODELS
181 ----------------------------
182
183 The first widely cited memory model, and the s
184 is Sequential Consistency. According to this
185 if each CPU executed its instructions in order
186 timing. In other words, the instructions from
187 interleaved in a nondeterministic way, always
188 global order that agrees with the order of the
189 program source for each CPU. The model says t
190 by each load is simply the value written by th
191 store to the same memory location, from any CP
192
193 For the MP example code shown above, Sequentia
194 that the undesired result r1 = 1, r2 = 0 canno
195 goes like this:
196
197 Since r1 = 1, P0 must store 1 to flag
198 it, as loads can obtain values only fr
199
200 P1 loads from flag before loading from
201 their instructions in order.
202
203 P1 must load 0 from buf before P0 stor
204 would be 1 since a load obtains its va
205 store to the same address.
206
207 P0 stores 1 to buf before storing 1 to
208 its instructions in order.
209
210 Since an instruction (in this case, P0
211 execute before itself, the specified o
212
213 However, real computer hardware almost never f
214 Consistency memory model; doing so would rule
215 performance optimizations. On ARM and PowerPC
216 instance, the MP example code really does some
217 r2 = 0.
218
219 x86 and SPARC follow yet a different memory mo
220 Ordering). This model predicts that the undes
221 pattern cannot occur, but in other respects it
222 Consistency. One example is the Store Buffer
223 each CPU stores to its own shared location and
224 other CPU's location:
225
226 int x = 0, y = 0;
227
228 P0()
229 {
230 int r0;
231
232 WRITE_ONCE(x, 1);
233 r0 = READ_ONCE(y);
234 }
235
236 P1()
237 {
238 int r1;
239
240 WRITE_ONCE(y, 1);
241 r1 = READ_ONCE(x);
242 }
243
244 Sequential Consistency predicts that the outco
245 impossible. (Exercise: Figure out the reasoni
246 this outcome to occur, and in fact it does som
247 SPARC systems.
248
249 The LKMM was inspired by the memory models fol
250 x86, Alpha, and other architectures. However,
251 detail from each of them.
252
253
254 ORDERING AND CYCLES
255 -------------------
256
257 Memory models are all about ordering. Often t
258 (i.e., the order in which certain events occur
259 be; consider for example the order of instruct
260 source code. We saw above that Sequential Con
261 important assumption that CPUs execute instruc
262 as those instructions occur in the code, and t
263 instances of ordering playing central roles in
264
265 The counterpart to ordering is a cycle. Order
266 It's not possible to have X ordered before Y,
267 Z ordered before X, because this would mean th
268 itself. The analysis of the MP example under
269 involved just such an impossible cycle:
270
271 W: P0 stores 1 to flag executes befo
272 X: P1 loads 1 from flag executes befo
273 Y: P1 loads 0 from buf executes befo
274 Z: P0 stores 1 to buf executes befo
275 W: P0 stores 1 to flag.
276
277 In short, if a memory model requires certain a
278 and a certain outcome for the loads in a piece
279 if those accesses would form a cycle, then the
280 that outcome cannot occur.
281
282 The LKMM is defined largely in terms of cycles
283
284
285 EVENTS
286 ------
287
288 The LKMM does not work directly with the C sta
289 kernel source code. Instead it considers the
290 statements in a more abstract form, namely, ev
291 includes three types of events:
292
293 Read events correspond to loads from s
294 calls to READ_ONCE(), smp_load_acquire
295 rcu_dereference().
296
297 Write events correspond to stores to s
298 calls to WRITE_ONCE(), smp_store_relea
299
300 Fence events correspond to memory barr
301 fences), such as calls to smp_rmb() or
302
303 These categories are not exclusive; a read or
304 a fence. This happens with functions like smp
305 spin_lock(). However, no single event can be
306 Atomic read-modify-write accesses, such as ato
307 correspond to a pair of events: a read followe
308 write event is omitted for executions where it
309 a cmpxchg() where the comparison fails.)
310
311 Other parts of the code, those which do not in
312 shared memory, do not give rise to events. Th
313 logical computations, control-flow instruction
314 private memory or CPU registers are not of cen
315 memory model. They only affect the model's pr
316 For example, an arithmetic computation might d
317 gets stored to a shared memory location (or in
318 index, the address where the value gets stored
319 is concerned only with the store itself -- its
320 -- not the computation leading up to it.
321
322 Events in the LKMM can be linked by various re
323 describe in the following sections. The memor
324 of these relations to be orderings, that is, i
325 have any cycles.
326
327
328 THE PROGRAM ORDER RELATION: po AND po-loc
329 -----------------------------------------
330
331 The most important relation between events is
332 can think of it as the order in which statemen
333 code after branches are taken into account and
334 unrolled. A better description might be the o
335 instructions are presented to a CPU's executio
336 that X is po-before Y (written as "X ->po Y" i
337 before Y in the instruction stream.
338
339 This is inherently a single-CPU relation; two
340 on different CPUs are never linked by po. Als
341 an ordering so it cannot have any cycles.
342
343 po-loc is a sub-relation of po. It links two
344 first comes before the second in program order
345 same memory location (the "-loc" suffix).
346
347 Although this may seem straightforward, there
348 program order we need to explain. The LKMM wa
349 architectural memory models which describe the
350 code, and it retains their outlook to a consid
351 read, write, and fence events used by the mode
352 individual machine instructions. Nevertheless
353 kernel code written in C, and the mapping from
354 be extremely complex.
355
356 Optimizing compilers have great freedom in the
357 source code to object code. They are allowed
358 that add memory accesses, eliminate accesses,
359 into pieces, or move them around. The use of
360 or one of the other atomic or synchronization
361 large number of compiler optimizations. In pa
362 that the compiler will not remove such accesse
363 (unless it can prove the accesses will never b
364 change the order in which they occur in the co
365 by the C standard), and it will not introduce
366
367 The MP and SB examples above used READ_ONCE()
368 than ordinary memory accesses. Thanks to this
369 that in the MP example, the compiler won't reo
370 buf and P0's write event to flag, and similarl
371 memory accesses in the examples.
372
373 Since private variables are not shared between
374 accessed normally without READ_ONCE() or WRITE
375 need not even be stored in normal memory at al
376 private variable could be stored in a CPU regi
377 that these variables have names starting with
378
379
380 A WARNING
381 ---------
382
383 The protections provided by READ_ONCE(), WRITE
384 not perfect; and under some circumstances it i
385 compiler to undermine the memory model. Here
386 both branches of an "if" statement store the s
387 location:
388
389 r1 = READ_ONCE(x);
390 if (r1) {
391 WRITE_ONCE(y, 2);
392 ... /* do something */
393 } else {
394 WRITE_ONCE(y, 2);
395 ... /* do something else */
396 }
397
398 For this code, the LKMM predicts that the load
399 executed before either of the stores to y. Ho
400 lift the stores out of the conditional, transf
401 something resembling:
402
403 r1 = READ_ONCE(x);
404 WRITE_ONCE(y, 2);
405 if (r1) {
406 ... /* do something */
407 } else {
408 ... /* do something else */
409 }
410
411 Given this version of the code, the LKMM would
412 from x could be executed after the store to y.
413 model's original prediction could be invalidat
414
415 Another issue arises from the fact that in C,
416 operators and function calls can be evaluated
417 example:
418
419 r1 = f(5) + g(6);
420
421 The object code might call f(5) either before
422 memory model cannot assume there is a fixed pr
423 between them. (In fact, if the function calls
424 compiler might even interleave their object co
425
426
427 DEPENDENCY RELATIONS: data, addr, and ctrl
428 ------------------------------------------
429
430 We say that two events are linked by a depende
431 execution of the second event depends in some
432 from memory by the first. The first event mus
433 value it obtains must somehow affect what the
434 There are three kinds of dependencies: data, a
435 control (ctrl).
436
437 A read and a write event are linked by a data
438 obtained by the read affects the value stored
439 simple example:
440
441 int x, y;
442
443 r1 = READ_ONCE(x);
444 WRITE_ONCE(y, r1 + 5);
445
446 The value stored by the WRITE_ONCE obviously d
447 loaded by the READ_ONCE. Such dependencies ca
448 arbitrarily complicated computations, and a wr
449 values of multiple reads.
450
451 A read event and another memory access event a
452 dependency if the value obtained by the read a
453 accessed by the other event. The second event
454 a write. Here's another simple example:
455
456 int a[20];
457 int i;
458
459 r1 = READ_ONCE(i);
460 r2 = READ_ONCE(a[r1]);
461
462 Here the location accessed by the second READ_
463 index value loaded by the first. Pointer indi
464 to address dependencies, since the address of
465 through a pointer will depend on the value rea
466 pointer.
467
468 Finally, a read event X and a write event Y ar
469 dependency if Y syntactically lies within an a
470 X affects the evaluation of the if condition v
471 dependency (or similarly for a switch statemen
472
473 int x, y;
474
475 r1 = READ_ONCE(x);
476 if (r1)
477 WRITE_ONCE(y, 1984);
478
479 Execution of the WRITE_ONCE() is controlled by
480 which depends on the value obtained by the REA
481 a control dependency from the load to the stor
482
483 It should be pretty obvious that events can on
484 come earlier in program order. Symbolically,
485 R ->addr X, or R ->ctrl X (where R is a read e
486 have R ->po X. It wouldn't make sense for a c
487 somehow on a value that doesn't get loaded fro
488 later in the code!
489
490 Here's a trick question: When is a dependency
491 When it is purely syntactic rather than semant
492 between two accesses is purely syntactic if th
493 actually depend on the result of the first. H
494
495 r1 = READ_ONCE(x);
496 WRITE_ONCE(y, r1 * 0);
497
498 There appears to be a data dependency from the
499 of y, since the value to be stored is computed
500 loaded. But in fact, the value stored does no
501 anything since it will always be 0. Thus the
502 syntactic (it appears to exist in the code) bu
503 second access will always be the same, regardl
504 first access). Given code like this, a compil
505 the value returned by the load from x, which w
506 any dependency. (The compiler is not permitte
507 the load generated for a READ_ONCE() -- that's
508 properties of READ_ONCE() -- but it is allowed
509 value.)
510
511 It's natural to object that no one in their ri
512 code like the above. However, macro expansion
513 to this sort of thing, in ways that often are
514 programmer.
515
516 Another mechanism that can lead to purely synt
517 related to the notion of "undefined behavior".
518 behaviors are called "undefined" in the C lang
519 which means that when they occur there are no
520 the outcome. Consider the following example:
521
522 int a[1];
523 int i;
524
525 r1 = READ_ONCE(i);
526 r2 = READ_ONCE(a[r1]);
527
528 Access beyond the end or before the beginning
529 of undefined behavior. Therefore the compiler
530 about what will happen if r1 is nonzero, and i
531 will always be zero regardless of the value ac
532 (If the assumption turns out to be wrong the r
533 be undefined anyway, so the compiler doesn't c
534 from the load can be discarded, breaking the a
535
536 The LKMM is unaware that purely syntactic depe
537 from semantic dependencies and therefore mista
538 accesses in the two examples above will be ord
539 example of how the compiler can undermine the
540
541
542 THE READS-FROM RELATION: rf, rfi, and rfe
543 -----------------------------------------
544
545 The reads-from relation (rf) links a write eve
546 the value loaded by the read is the value that
547 write. In colloquial terms, the load "reads f
548 write W ->rf R to indicate that the load R rea
549 further distinguish the cases where the load a
550 the same CPU (internal reads-from, or rfi) and
551 different CPUs (external reads-from, or rfe).
552
553 For our purposes, a memory location's initial
554 though it had been written there by an imagina
555 executes on a separate CPU before the main pro
556
557 Usage of the rf relation implicitly assumes th
558 read from a single store. It doesn't apply pr
559 of load-tearing, where a load obtains some of
560 and some of them from another store. Fortunat
561 and WRITE_ONCE() will prevent load-tearing; it
562
563 int x = 0;
564
565 P0()
566 {
567 WRITE_ONCE(x, 0x1234);
568 }
569
570 P1()
571 {
572 int r1;
573
574 r1 = READ_ONCE(x);
575 }
576
577 and end up with r1 = 0x1200 (partly from x's i
578 from the value stored by P0).
579
580 On the other hand, load-tearing is unavoidable
581 accesses are used. Consider this example:
582
583 union {
584 u32 w;
585 u16 h[2];
586 } x;
587
588 P0()
589 {
590 WRITE_ONCE(x.h[0], 0x1234);
591 WRITE_ONCE(x.h[1], 0x5678);
592 }
593
594 P1()
595 {
596 int r1;
597
598 r1 = READ_ONCE(x.w);
599 }
600
601 If r1 = 0x56781234 (little-endian!) at the end
602 from both of P0's stores. It is possible to h
603 unaligned accesses in a memory model, but the
604 attempt to do so. It requires all accesses to
605 of the location's actual size.
606
607
608 CACHE COHERENCE AND THE COHERENCE ORDER RELATI
609 ----------------------------------------------
610
611 Cache coherence is a general principle requiri
612 multi-processor system, the CPUs must share a
613 memory contents. Specifically, it requires th
614 shared memory, the stores to that location mus
615 ordering which all the CPUs agree on (the cohe
616 ordering must be consistent with the program o
617 that location.
618
619 To put it another way, for any variable x, the
620 the stores to x is simply the order in which t
621 another. The imaginary store which establishe
622 comes first in the coherence order; the store
623 overwrites the initial value comes second; the
624 that value comes third, and so on.
625
626 You can think of the coherence order as being
627 stores reach x's location in memory (or if you
628 hardware-centric view, the order in which the
629 x's cache line). We write W ->co W' if W come
630 coherence order, that is, if the value stored
631 directly or indirectly, by the value stored by
632
633 Coherence order is required to be consistent w
634 requirement takes the form of four coherency r
635
636 Write-write coherence: If W ->po-loc W
637 W' in program order and they access th
638 and W' are two stores, then W ->co W'.
639
640 Write-read coherence: If W ->po-loc R,
641 is a load, then R must read from W or
642 which comes after W in the coherence o
643
644 Read-write coherence: If R ->po-loc W,
645 is a store, then the store which R rea
646 W in the coherence order.
647
648 Read-read coherence: If R ->po-loc R',
649 loads, then either they read from the
650 store read by R comes before the store
651 coherence order.
652
653 This is sometimes referred to as sequential co
654 because it means that the accesses to any sing
655 the rules of the Sequential Consistency memory
656 Wikipedia, sequential consistency per variable
657 mean the same thing except that cache coherenc
658 requirement that every store eventually become
659
660 Any reasonable memory model will include cache
661 expectation of cache coherence is so deeply in
662 of its requirements look more like hardware bu
663 errors:
664
665 int x;
666
667 P0()
668 {
669 WRITE_ONCE(x, 17);
670 WRITE_ONCE(x, 23);
671 }
672
673 If the final value stored in x after this code
674 think your computer was broken. It would be a
675 write-write coherence rule: Since the store of
676 program order, it must also come later in x's
677 thus must overwrite the store of 17.
678
679 int x = 0;
680
681 P0()
682 {
683 int r1;
684
685 r1 = READ_ONCE(x);
686 WRITE_ONCE(x, 666);
687 }
688
689 If r1 = 666 at the end, this would violate the
690 rule: The READ_ONCE() load comes before the WR
691 program order, so it must not read from that s
692 coming earlier in the coherence order (in this
693 value).
694
695 int x = 0;
696
697 P0()
698 {
699 WRITE_ONCE(x, 5);
700 }
701
702 P1()
703 {
704 int r1, r2;
705
706 r1 = READ_ONCE(x);
707 r2 = READ_ONCE(x);
708 }
709
710 If r1 = 5 (reading from P0's store) and r2 = 0
711 imaginary store which establishes x's initial
712 would violate the read-read coherence rule: Th
713 the r2 load in program order, so it must not r
714 comes later in the coherence order.
715
716 (As a minor curiosity, if this code had used n
717 READ_ONCE() in P1, on Itanium it sometimes cou
718 and r2 = 0! This results from parallel execut
719 encoded in Itanium's Very-Long-Instruction-Wor
720 another motivation for using READ_ONCE() when
721 locations.)
722
723 Just like the po relation, co is inherently an
724 possible for a store to directly or indirectly
725 just like with the rf relation, we distinguish
726 occur on the same CPU (internal coherence orde
727 that occur on different CPUs (external coheren
728
729 On the other hand, stores to different memory
730 related by co, just as instructions on differe
731 related by po. Coherence order is strictly pe
732 prefer, each location has its own independent
733
734
735 THE FROM-READS RELATION: fr, fri, and fre
736 -----------------------------------------
737
738 The from-reads relation (fr) can be a little d
739 grok. It describes the situation where a load
740 overwritten by a store. In other words, we ha
741 value that R reads is overwritten (directly or
742 equivalently, when R reads from a store which
743 the coherence order.
744
745 For example:
746
747 int x = 0;
748
749 P0()
750 {
751 int r1;
752
753 r1 = READ_ONCE(x);
754 WRITE_ONCE(x, 2);
755 }
756
757 The value loaded from x will be 0 (assuming ca
758 gets overwritten by the value 2. Thus there i
759 READ_ONCE() to the WRITE_ONCE(). If the code
760 stores to x, there would also be fr links from
761 them.
762
763 As with rf, rfi, and rfe, we subdivide the fr
764 the load and the store are on the same CPU) an
765 different CPUs).
766
767 Note that the fr relation is determined entire
768 relations; it is not independent. Given a rea
769 event W for the same location, we will have R
770 the write which R reads from is co-before W.
771
772 (R ->fr W) := (there exists W' with W'
773
774
775 AN OPERATIONAL MODEL
776 --------------------
777
778 The LKMM is based on various operational memor
779 the models arise from an abstract view of how
780 operates. Here are the main ideas, as incorpo
781
782 The system as a whole is divided into the CPUs
783 The CPUs are responsible for executing instruc
784 in program order), and they communicate with t
785 For the most part, executing an instruction re
786 only internal operations. However, loads, sto
787 more.
788
789 When CPU C executes a store instruction, it te
790 to store a certain value at a certain location
791 propagates the store to all the other CPUs as
792 special case, we say that the store propagates
793 time it is executed.) The memory subsystem al
794 store falls in the location's coherence order.
795 arrange for the store to be co-later than (i.e
796 other store to the same location which has alr
797
798 When a CPU executes a load instruction R, it f
799 whether there are any as-yet unexecuted store
800 same location, that come before R in program o
801 uses the value of the po-latest such store as
802 and we say that the store's value is forwarded
803 CPU asks the memory subsystem for the value to
804 is satisfied from memory. The memory subsyste
805 of the co-latest store to the location in ques
806 propagated to that CPU.
807
808 (In fact, the picture needs to be a little mor
809 CPUs have local caches, and propagating a stor
810 propagating it to the CPU's local cache. A lo
811 time to process the stores that it receives, a
812 to satisfy one of the CPU's loads until it has
813 most architectures, the local caches process s
814 First-In-First-Out order, and consequently the
815 doesn't matter for the memory model. But on A
816 have a partitioned design that results in non-
817 discuss this in more detail later.)
818
819 Note that load instructions may be executed sp
820 restarted under certain circumstances. The me
821 premature executions; we simply say that the l
822 final time it is forwarded or satisfied.
823
824 Executing a fence (or memory barrier) instruct
825 CPU to do anything special other than informin
826 about the fence. However, fences do constrain
827 memory subsystem handle other instructions, in
828
829 First, a fence forces the CPU to execute vario
830 program order. Exactly which instructions are
831 type of fence:
832
833 Strong fences, including smp_mb() and
834 the CPU to execute all po-earlier inst
835 po-later instructions;
836
837 smp_rmb() forces the CPU to execute al
838 before any po-later loads;
839
840 smp_wmb() forces the CPU to execute al
841 before any po-later stores;
842
843 Acquire fences, such as smp_load_acqui
844 execute the load associated with the f
845 part of an smp_load_acquire()) before
846 instructions;
847
848 Release fences, such as smp_store_rele
849 execute all po-earlier instructions be
850 associated with the fence (e.g., the s
851 smp_store_release()).
852
853 Second, some types of fence affect the way the
854 propagates stores. When a fence instruction i
855
856 For each other CPU C', smp_wmb() force
857 on C to propagate to C' before any po-
858
859 For each other CPU C', any store which
860 a release fence is executed (including
861 stores executed on C) is forced to pro
862 store associated with the release fenc
863
864 Any store which propagates to C before
865 executed (including all po-earlier sto
866 propagate to all other CPUs before any
867 the strong fence are executed on C.
868
869 The propagation ordering enforced by release f
870 affects stores from other CPUs that propagate
871 fence is executed, as well as stores that are
872 fence. We describe this property by saying th
873 strong fences are A-cumulative. By contrast,
874 A-cumulative; they only affect the propagation
875 executed on C before the fence (i.e., those wh
876 program order).
877
878 rcu_read_lock(), rcu_read_unlock(), and synchr
879 other properties which we discuss later.
880
881
882 PROPAGATION ORDER RELATION: cumul-fence
883 ---------------------------------------
884
885 The fences which affect propagation order (i.e
886 smp_wmb() fences) are collectively referred to
887 though smp_wmb() isn't A-cumulative. The cumu
888 defined to link memory access events E and F w
889
890 E and F are both stores on the same CP
891 event occurs between them in program o
892
893 F is a release fence and some X comes
894 where either X = E or else E ->rf X; o
895
896 A strong fence event occurs between so
897 order, where either X = E or else E ->
898
899 The operational model requires that whenever W
900 and W ->cumul-fence W', then W must propagate
901 before W' does. However, for different CPUs C
902 require W to propagate to C before W' propagat
903
904
905 DERIVATION OF THE LKMM FROM THE OPERATIONAL MO
906 ----------------------------------------------
907
908 The LKMM is derived from the restrictions impo
909 outlined above. These restrictions involve th
910 maintaining cache coherence and the fact that
911 value before it knows what that value is, amon
912
913 The formal version of the LKMM is defined by s
914 axioms:
915
916 Sequential consistency per variable: T
917 system obey the four coherency rules.
918
919 Atomicity: This requires that atomic r
920 operations really are atomic, that is,
921 sneak into the middle of such an updat
922
923 Happens-before: This requires that cer
924 executed in a specific order.
925
926 Propagation: This requires that certai
927 CPUs and to RAM in a specific order.
928
929 Rcu: This requires that RCU read-side
930 grace periods obey the rules of RCU, i
931 Grace-Period Guarantee.
932
933 Plain-coherence: This requires that pl
934 (those not using READ_ONCE(), WRITE_ON
935 the operational model's rules regardin
936
937 The first and second are quite common; they ca
938 memory models (such as those for C11/C++11).
939 "propagation" axioms have analogs in other mem
940 "rcu" and "plain-coherence" axioms are specifi
941
942 Each of these axioms is discussed below.
943
944
945 SEQUENTIAL CONSISTENCY PER VARIABLE
946 -----------------------------------
947
948 According to the principle of cache coherence,
949 shared location in memory form a global orderi
950 inserting the loads from that location into th
951 each load between the store that it reads from
952 store. This leaves the relative positions of
953 same store unspecified; let's say they are ins
954 first for CPU 0, then CPU 1, etc.
955
956 You can check that the four coherency rules im
957 and po-loc relations agree with this global or
958 whenever we have X ->rf Y or X ->co Y or X ->f
959 X event comes before the Y event in the global
960 "coherence" axiom expresses this by requiring
961 relations not to have any cycles. This means
962 to find events
963
964 X0 -> X1 -> X2 -> ... -> Xn -> X0,
965
966 where each of the links is either rf, co, fr,
967 hold if the accesses to the fixed memory locat
968 cache coherence demands.
969
970 Although it is not obvious, it can be shown th
971 true: This LKMM axiom implies that the four co
972 obeyed.
973
974
975 ATOMIC UPDATES: rmw
976 -------------------
977
978 What does it mean to say that a read-modify-wr
979 as atomic_inc(&x), is atomic? It means that t
980 this case) does not get altered between the re
981 making up the atomic operation. In particular
982 atomic_inc(&x) concurrently, it must be guaran
983 value of x will be the initial value plus two.
984 the following sequence of events:
985
986 CPU 0 loads x obtaining 13;
987 CPU 1
988 CPU 0 stores 14 to x;
989 CPU 1
990
991 where the final value of x is wrong (14 rather
992
993 In this example, CPU 0's increment effectively
994 occurs in between CPU 1's load and store. To
995 problem is that the position of CPU 0's store
996 is between the store that CPU 1 reads from and
997 performs.
998
999 The same analysis applies to all atomic update
1000 to enforce atomicity the LKMM requires that a
1001 rule: Whenever R and W are the read and write
1002 atomic read-modify-write and W' is the write
1003 there must not be any stores coming between W
1004 order. Equivalently,
1005
1006 (R ->rmw W) implies (there is no X wi
1007
1008 where the rmw relation links the read and wri
1009 atomic update. This is what the LKMM's "atom
1010
1011 Atomic rmw updates play one more role in the
1012 sequences". An rmw sequence is simply a bunc
1013 each update reads from the previous one. Wri
1014 looks like this:
1015
1016 Z0 ->rf Y1 ->rmw Z1 ->rf ... ->rf Yn
1017
1018 where Z0 is some store event and n can be any
1019 degenerate case). We write this relation as:
1020 Note that this implies Z0 and Zn are stores t
1021
1022 Rmw sequences have a special property in the
1023 cumul-fence relation. That is, if we have:
1024
1025 U ->cumul-fence X -> rmw-sequence Y
1026
1027 then also U ->cumul-fence Y. Thinking about
1028 operational model, U ->cumul-fence X says tha
1029 to each CPU before the store X does. Then th
1030 linked by an rmw sequence means that U also p
1031 before Y does. In an analogous way, rmw sequ
1032 the w-post-bounded relation defined below in
1033 DATA RACES section.
1034
1035 (The notion of rmw sequences in the LKMM is s
1036 the same as, that of release sequences in the
1037 were added to the LKMM to fix an obscure bug;
1038 updates with full-barrier semantics did not a
1039 at least as strong as atomic updates with rel
1040
1041
1042 THE PRESERVED PROGRAM ORDER RELATION: ppo
1043 -----------------------------------------
1044
1045 There are many situations where a CPU is obli
1046 instructions in program order. We amalgamate
1047 "preserved program order") relation, which li
1048 instruction to the po-later instruction and i
1049 po.
1050
1051 The operational model already includes a desc
1052 situation: Fences are a source of ppo links.
1053 memory accesses with X ->po Y; then the CPU m
1054 any of the following hold:
1055
1056 A strong (smp_mb() or synchronize_rcu
1057 X and Y;
1058
1059 X and Y are both stores and an smp_wm
1060 them;
1061
1062 X and Y are both loads and an smp_rmb
1063 them;
1064
1065 X is also an acquire fence, such as s
1066
1067 Y is also a release fence, such as sm
1068
1069 Another possibility, not mentioned earlier bu
1070 section, is:
1071
1072 X and Y are both loads, X ->addr Y (i
1073 dependency from X to Y), and X is a R
1074 access.
1075
1076 Dependencies can also cause instructions to b
1077 order. This is uncontroversial when the seco
1078 store; either a data, address, or control dep
1079 a store W will force the CPU to execute R bef
1080 simply because the CPU cannot tell the memory
1081 store before it knows what value should be st
1082 data dependency), what location it should be
1083 of an address dependency), or whether the sto
1084 place (in the case of a control dependency).
1085
1086 Dependencies to load instructions are more pr
1087 there is no such thing as a data dependency t
1088 has no reason to respect a control dependency
1089 can always satisfy the second load speculativ
1090 then ignore the result if it turns out that t
1091 be executed after all. And lastly, the real
1092 we consider address dependencies to loads.
1093
1094 To be fair about it, all Linux-supported arch
1095 loads in program order if there is an address
1096 After all, a CPU cannot ask the memory subsys
1097 a particular location before it knows what th
1098 the split-cache design used by Alpha can caus
1099 that looks as if the loads were executed out
1100 section for more details). The kernel includ
1101 problem when the loads come from READ_ONCE(),
1102 includes address dependencies to loads in the
1103
1104 On the other hand, dependencies can indirectl
1105 two loads. This happens when there is a depe
1106 store and a second, po-later load reads from
1107
1108 R ->dep W ->rfi R',
1109
1110 where the dep link can be either an address o
1111 this situation we know it is possible for the
1112 W, because it can forward the value that W wi
1113 cannot execute R' before R, because it cannot
1114 it knows what that value is, or that W and R'
1115 location. However, if there is merely a cont
1116 and W then the CPU can speculatively forward
1117 R; if the speculation turns out to be wrong t
1118 restart or abandon R'.
1119
1120 (In theory, a CPU might forward a store to a
1121 an address dependency like this:
1122
1123 r1 = READ_ONCE(ptr);
1124 WRITE_ONCE(*r1, 17);
1125 r2 = READ_ONCE(*r1);
1126
1127 because it could tell that the store and the
1128 same location even before it knows what the l
1129 However, none of the architectures supported
1130 this.)
1131
1132 Two memory accesses of the same location must
1133 program order if the second access is a store
1134
1135 R ->po-loc W
1136
1137 (the po-loc link says that R comes before W i
1138 access the same location), the CPU is obliged
1139 If it executed W first then the memory subsys
1140 read request with the value stored by W (or a
1141 violation of the read-write coherence rule.
1142
1143 W ->po-loc W'
1144
1145 and the CPU executed W' before W, then the me
1146 W' before W in the coherence order. It would
1147 overwrite W', in violation of the write-write
1148 (Interestingly, an early ARMv8 memory model,
1149 allowing out-of-order writes like this to occ
1150 violating the write-write coherence rule by r
1151 send the W write to the memory subsystem at a
1152
1153
1154 AND THEN THERE WAS ALPHA
1155 ------------------------
1156
1157 As mentioned above, the Alpha architecture is
1158 not appear to respect address dependencies to
1159 code such as the following:
1160
1161 int x = 0;
1162 int y = -1;
1163 int *ptr = &y;
1164
1165 P0()
1166 {
1167 WRITE_ONCE(x, 1);
1168 smp_wmb();
1169 WRITE_ONCE(ptr, &x);
1170 }
1171
1172 P1()
1173 {
1174 int *r1;
1175 int r2;
1176
1177 r1 = ptr;
1178 r2 = READ_ONCE(*r1);
1179 }
1180
1181 can malfunction on Alpha systems (notice that
1182 to read ptr instead of READ_ONCE()). It is q
1183 and r2 = 0 at the end, in spite of the addres
1184
1185 At first glance this doesn't seem to make sen
1186 smp_wmb() forces P0's store to x to propagate
1187 to ptr does. And since P1 can't execute its
1188 until it knows what location to load from, i.
1189 first load, the value x = 1 must have propaga
1190 second load executed. So why doesn't r2 end
1191
1192 The answer lies in the Alpha's split local ca
1193 stores do reach P1's local cache in the prope
1194 that the first store is processed by a busy p
1195 the second store is processed by an idle part
1196 value may not become available for P1's CPU t
1197 ptr = &x value does, leading to the undesirab
1198 final effect is that even though the two load
1199 program order, it appears that they aren't.
1200
1201 This could not have happened if the local cac
1202 incoming stores in FIFO order. By contrast,
1203 maintain at least the appearance of FIFO orde
1204
1205 In practice, this difficulty is solved by ins
1206 between P1's two loads when the kernel is com
1207 architecture. In fact, as of version 4.15, t
1208 adds this fence after every READ_ONCE() and a
1209 effect of the fence is to cause the CPU not t
1210 instructions until after the local cache has
1211 the stores it has already received. Thus, if
1212
1213 P1()
1214 {
1215 int *r1;
1216 int r2;
1217
1218 r1 = READ_ONCE(ptr);
1219 r2 = READ_ONCE(*r1);
1220 }
1221
1222 then we would never get r1 = &x and r2 = 0.
1223 its second load, the x = 1 store would alread
1224 the local cache and available for satisfying
1225 we have yet another reason why shared data sh
1226 READ_ONCE() or another synchronization primit
1227 directly.
1228
1229 The LKMM requires that smp_rmb(), acquire fen
1230 share this property: They do not allow the CP
1231 instructions (or po-later loads in the case o
1232 outstanding stores have been processed by the
1233 case of a strong fence, the CPU first has to
1234 po-earlier stores to propagate to every other
1235 it has to wait for the local cache to process
1236 as of that time -- not just the stores receiv
1237 began.
1238
1239 And of course, none of this matters for any a
1240 Alpha.
1241
1242
1243 THE HAPPENS-BEFORE RELATION: hb
1244 -------------------------------
1245
1246 The happens-before relation (hb) links memory
1247 execute in a certain order. hb includes the
1248 others, one of which is rfe.
1249
1250 W ->rfe R implies that W and R are on differe
1251 that W's store must have propagated to R's CP
1252 otherwise R could not have read the value sto
1253 must have executed before R, and so we have W
1254
1255 The equivalent fact need not hold if W ->rfi
1256 the same CPU). As we have already seen, the
1257 W's value to be forwarded to R in such cases,
1258 execute before W does.
1259
1260 It's important to understand that neither coe
1261 hb, despite their similarities to rfe. For e
1262 W ->coe W'. This means that W and W' are sto
1263 they execute on different CPUs, and W comes b
1264 order (i.e., W' overwrites W). Nevertheless,
1265 execute before W, because the decision as to
1266 the other is made later by the memory subsyst
1267 nearly simultaneous, either one can come out
1268 R ->fre W means that W overwrites the value w
1269 doesn't mean that W has to execute after R.
1270 for the memory subsystem not to propagate W t
1271 has executed, which is possible if W executes
1272
1273 The third relation included in hb is like ppo
1274 events that are on the same CPU. However it
1275 explain, because it arises only indirectly fr
1276 cache coherence. The relation is called prop
1277 on CPU C in situations where a store from som
1278 the first event in the coherence order and pr
1279 second event executes.
1280
1281 This is best explained with some examples. T
1282 like this:
1283
1284 int x;
1285
1286 P0()
1287 {
1288 int r1;
1289
1290 WRITE_ONCE(x, 1);
1291 r1 = READ_ONCE(x);
1292 }
1293
1294 P1()
1295 {
1296 WRITE_ONCE(x, 8);
1297 }
1298
1299 If r1 = 8 at the end then P0's accesses must
1300 order. We can deduce this from the operation
1301 had executed before its store then the value
1302 been forwarded to the load, so r1 would have
1303 8. In this case there is a prop link from P0
1304 event, because P1's store came after P0's sto
1305 order, and P1's store propagated to P0 before
1306
1307 An equally simple case involves two loads of
1308 read from different stores:
1309
1310 int x = 0;
1311
1312 P0()
1313 {
1314 int r1, r2;
1315
1316 r1 = READ_ONCE(x);
1317 r2 = READ_ONCE(x);
1318 }
1319
1320 P1()
1321 {
1322 WRITE_ONCE(x, 9);
1323 }
1324
1325 If r1 = 0 and r2 = 9 at the end then P0's acc
1326 in program order. If the second load had exe
1327 then the x = 9 store must have been propagate
1328 load executed, and so r1 would have been 9 ra
1329 case there is a prop link from P0's first rea
1330 because P1's store overwrote the value read b
1331 P1's store propagated to P0 before P0's secon
1332
1333 Less trivial examples of prop all involve fen
1334 examples above, they can require that some in
1335 out of program order. This next one should l
1336
1337 int buf = 0, flag = 0;
1338
1339 P0()
1340 {
1341 WRITE_ONCE(buf, 1);
1342 smp_wmb();
1343 WRITE_ONCE(flag, 1);
1344 }
1345
1346 P1()
1347 {
1348 int r1;
1349 int r2;
1350
1351 r1 = READ_ONCE(flag);
1352 r2 = READ_ONCE(buf);
1353 }
1354
1355 This is the MP pattern again, with an smp_wmb
1356 stores. If r1 = 1 and r2 = 0 at the end then
1357 from P1's second load to its first (backwards
1358 similar to the previous examples: The value P
1359 overwritten by P0's store to buf, the fence g
1360 to buf will propagate to P1 before the store
1361 store to flag propagates to P1 before P1 read
1362
1363 The prop link says that in order to obtain th
1364 P1 must execute its second load before the fi
1365 from flag were executed first, then the buf =
1366 have propagated to P1 by the time P1's load f
1367 would have been 1 at the end, not 0. (The re
1368 Alpha, although the details are more complica
1369 into them.)
1370
1371 But what if we put an smp_rmb() fence between
1372 would force the two loads to be executed in p
1373 would generate a cycle in the hb relation: Th
1374 link (hence an hb link) from the first load t
1375 prop relation would give an hb link from the
1376 Since an instruction can't execute before its
1377 conclude that if an smp_rmb() fence is added,
1378 outcome is impossible -- as it should be.
1379
1380 The formal definition of the prop relation in
1381 followed by an arbitrary number of cumul-fenc
1382 rfe link. You can concoct more exotic exampl
1383 one fence, although this quickly leads to dim
1384 of complexity. For instance, here's an examp
1385 followed by two cumul-fences and an rfe link,
1386 release fences are A-cumulative:
1387
1388 int x, y, z;
1389
1390 P0()
1391 {
1392 int r0;
1393
1394 WRITE_ONCE(x, 1);
1395 r0 = READ_ONCE(z);
1396 }
1397
1398 P1()
1399 {
1400 WRITE_ONCE(x, 2);
1401 smp_wmb();
1402 WRITE_ONCE(y, 1);
1403 }
1404
1405 P2()
1406 {
1407 int r2;
1408
1409 r2 = READ_ONCE(y);
1410 smp_store_release(&z, 1);
1411 }
1412
1413 If x = 2, r0 = 1, and r2 = 1 after this code
1414 link from P0's store to its load. This is be
1415 overwritten by P1's store since x = 2 at the
1416 smp_wmb() ensures that P1's store to x propag
1417 store to y does (the first cumul-fence), the
1418 before P2's load and store execute, P2's smp_
1419 guarantees that the stores to x and y both pr
1420 store to z does (the second cumul-fence), and
1421 store to z has propagated to P0 (an rfe link)
1422
1423 In summary, the fact that the hb relation lin
1424 in the order they execute means that it must
1425 requirement is the content of the LKMM's "hap
1426
1427 The LKMM defines yet another relation connect
1428 instruction execution, but it is not included
1429 particular properties of strong fences, which
1430 section.
1431
1432
1433 THE PROPAGATES-BEFORE RELATION: pb
1434 ----------------------------------
1435
1436 The propagates-before (pb) relation capitaliz
1437 features of strong fences. It links two even
1438 store is coherence-later than E and propagate
1439 before F executes. The formal definition req
1440 F via a coe or fre link, an arbitrary number
1441 optional rfe link, a strong fence, and an arb
1442 links. Let's see how this definition works o
1443
1444 Consider first the case where E is a store (i
1445 of links begins with coe). Then there are ev
1446 that:
1447
1448 E ->coe W ->cumul-fence* X ->rfe? Y -
1449
1450 where the * suffix indicates an arbitrary num
1451 specified type, and the ? suffix indicates th
1452 be equal to X). Because of the cumul-fence l
1453 propagate to Y's CPU before X does, hence bef
1454 before the strong fence executes. Because th
1455 know that W will propagate to every CPU and t
1456 And because of the hb links, we know that Z w
1457 Thus W, which comes later than E in the coher
1458 propagate to every CPU and to RAM before F ex
1459
1460 The case where E is a load is exactly the sam
1461 link in the sequence is fre instead of coe.
1462
1463 The existence of a pb link from E to F implie
1464 before F. To see why, suppose that F execute
1465 have propagated to E's CPU before E executed.
1466 memory subsystem would then be forced to make
1467 coherence order, contradicting the fact that
1468 load, the memory subsystem would then be forc
1469 request with the value stored by W or an even
1470 contradicting the fact that E ->fre W.
1471
1472 A good example illustrating how pb works is t
1473 fences:
1474
1475 int x = 0, y = 0;
1476
1477 P0()
1478 {
1479 int r0;
1480
1481 WRITE_ONCE(x, 1);
1482 smp_mb();
1483 r0 = READ_ONCE(y);
1484 }
1485
1486 P1()
1487 {
1488 int r1;
1489
1490 WRITE_ONCE(y, 1);
1491 smp_mb();
1492 r1 = READ_ONCE(x);
1493 }
1494
1495 If r0 = 0 at the end then there is a pb link
1496 load: an fre link from P0's load to P1's stor
1497 value read by P0), and a strong fence between
1498 In this example, the sequences of cumul-fence
1499 Note that this pb link is not included in hb
1500 because it does not start and end on the same
1501
1502 Similarly, if r1 = 0 at the end then there is
1503 to P0's. This means that if both r1 and r2 w
1504 cycle in pb, which is not possible since an i
1505 before itself. Thus, adding smp_mb() fences
1506 prevents the r0 = 0, r1 = 0 outcome.
1507
1508 In summary, the fact that the pb relation lin
1509 they execute means that it cannot have cycles
1510 the content of the LKMM's "propagation" axiom
1511
1512
1513 RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, r
1514 ---------------------------------------------
1515
1516 RCU (Read-Copy-Update) is a powerful synchron
1517 rests on two concepts: grace periods and read
1518
1519 A grace period is the span of time occupied b
1520 synchronize_rcu(). A read-side critical sect
1521 section, for short) is a region of code delim
1522 at the start and rcu_read_unlock() at the end
1523 be nested, although we won't make use of this
1524
1525 As far as memory models are concerned, RCU's
1526 Grace-Period Guarantee, which states that a c
1527 span a full grace period. In more detail, th
1528
1529 For any critical section C and any gr
1530 one of the following statements must
1531
1532 (1) C ends before G does, and in addition
1533 propagates to C's CPU before the end
1534 every CPU before G ends.
1535
1536 (2) G starts before C does, and in additi
1537 propagates to G's CPU before the star
1538 to every CPU before C starts.
1539
1540 In particular, it is not possible for a criti
1541 before and end after a grace period.
1542
1543 Here is a simple example of RCU in action:
1544
1545 int x, y;
1546
1547 P0()
1548 {
1549 rcu_read_lock();
1550 WRITE_ONCE(x, 1);
1551 WRITE_ONCE(y, 1);
1552 rcu_read_unlock();
1553 }
1554
1555 P1()
1556 {
1557 int r1, r2;
1558
1559 r1 = READ_ONCE(x);
1560 synchronize_rcu();
1561 r2 = READ_ONCE(y);
1562 }
1563
1564 The Grace Period Guarantee tells us that when
1565 never end with r1 = 1 and r2 = 0. The reason
1566 means that P0's store to x propagated to P1 b
1567 synchronize_rcu(), so P0's critical section m
1568 P1's grace period, contrary to part (2) of th
1569 other hand, r2 = 0 means that P0's store to y
1570 end of the critical section, did not propagat
1571 the grace period, contrary to part (1). Toge
1572 the Guarantee.
1573
1574 In the kernel's implementations of RCU, the r
1575 to propagate to every CPU are fulfilled by pl
1576 suitable places in the RCU-related code. Thu
1577 starts before a grace period does then the cr
1578 execute an smp_mb() fence after the end of th
1579 some time before the grace period's synchroni
1580 And if a critical section ends after a grace
1581 synchronize_rcu() routine will execute an smp
1582 and some time before the critical section's o
1583 executes.
1584
1585 What exactly do we mean by saying that a crit
1586 before" or "ends after" a grace period? Some
1587 are pretty obvious, as in the example above,
1588 entirely clear. The LKMM formalizes this not
1589 rcu-link relation. rcu-link encompasses a ve
1590 "before": If E and F are RCU fence events (i.
1591 rcu_read_unlock(), or synchronize_rcu()) then
1592 E ->rcu-link F includes cases where E is po-b
1593 event X, F is po-after some memory-access eve
1594 X ->rfe Y, X ->co Y, or X ->fr Y.
1595
1596 The formal definition of the rcu-link relatio
1597 obscure, and we won't give it here. It is cl
1598 relation, and the details don't matter unless
1599 a somewhat lengthy formal proof. Pretty much
1600 about rcu-link is the information in the prec
1601
1602 The LKMM also defines the rcu-gp and rcu-rscs
1603 grace periods and read-side critical sections
1604 following way:
1605
1606 E ->rcu-gp F means that E and F are i
1607 and that event is a synchronize_rcu()
1608 period).
1609
1610 E ->rcu-rscsi F means that E and F ar
1611 and rcu_read_lock() fence events deli
1612 critical section. (The 'i' at the en
1613 that this relation is "inverted": It
1614 critical section to the start.)
1615
1616 If we think of the rcu-link relation as stand
1617 "before", then X ->rcu-gp Y ->rcu-link Z roug
1618 grace period which ends before Z begins. (In
1619 this, because it also includes cases where so
1620 Z's CPU before Z begins but doesn't propagate
1621 after X ends.) Similarly, X ->rcu-rscsi Y ->
1622 the end of a critical section which starts be
1623
1624 The LKMM goes on to define the rcu-order rela
1625 rcu-gp and rcu-rscsi links separated by rcu-l
1626 number of rcu-gp links is >= the number of rc
1627 example:
1628
1629 X ->rcu-gp Y ->rcu-link Z ->rcu-rscsi
1630
1631 would imply that X ->rcu-order V, because thi
1632 rcu-gp links and one rcu-rscsi link. (It als
1633 X ->rcu-order T and Z ->rcu-order V.) On the
1634
1635 X ->rcu-rscsi Y ->rcu-link Z ->rcu-rs
1636
1637 does not imply X ->rcu-order V, because the s
1638 one rcu-gp link but two rcu-rscsi links.
1639
1640 The rcu-order relation is important because t
1641 means that rcu-order links act kind of like s
1642 particular, E ->rcu-order F implies not only
1643 ends, but also that any write po-before E wil
1644 before any instruction po-after F can execute
1645 imply that E must execute before F; in fact,
1646 fence event is linked to itself by rcu-order
1647
1648 To prove this in full generality requires som
1649 We'll consider just a very simple case:
1650
1651 G ->rcu-gp W ->rcu-link Z ->rcu-rscsi
1652
1653 This formula means that G and W are the same
1654 and there are events X, Y and a read-side cri
1655
1656 1. G = W is po-before or equal to X;
1657
1658 2. X comes "before" Y in some sense (
1659
1660 3. Y is po-before Z;
1661
1662 4. Z is the rcu_read_unlock() event m
1663
1664 5. F is the rcu_read_lock() event mar
1665
1666 From 1 - 4 we deduce that the grace period G
1667 section C. Then part (2) of the Grace Period
1668 that G starts before C does, but also that an
1669 G's CPU before G starts must propagate to eve
1670 In particular, the write propagates to every
1671 executing and hence before any instruction po
1672 This sort of reasoning can be extended to han
1673 covered by rcu-order.
1674
1675 The rcu-fence relation is a simple extension
1676 rcu-order only links certain fence events (ca
1677 rcu_read_lock(), or rcu_read_unlock()), rcu-f
1678 that are separated by an rcu-order link. Thi
1679 the strong-fence relation links events that a
1680 smp_mb() fence event (as mentioned above, rcu
1681 like strong fences). Written symbolically, X
1682 there are fence events E and F such that:
1683
1684 X ->po E ->rcu-order F ->po Y.
1685
1686 From the discussion above, we see this implie
1687 executes before Y, but also (if X is a store)
1688 every CPU before Y executes. Thus rcu-fence
1689 "super-strong" fence: Unlike the original str
1690 synchronize_rcu()), rcu-fence is able to link
1691 CPUs. (Perhaps this fact should lead us to s
1692 really a fence at all!)
1693
1694 Finally, the LKMM defines the RCU-before (rb)
1695 rcu-fence. This is done in essentially the s
1696 relation was defined in terms of strong-fence
1697 details; the end result is that E ->rb F impl
1698 before F, just as E ->pb F does (and for much
1699
1700 Putting this all together, the LKMM expresses
1701 Guarantee by requiring that the rb relation d
1702 Equivalently, this "rcu" axiom requires that
1703 and F with E ->rcu-link F ->rcu-order E. Or
1704 the axiom requires that there are no cycles c
1705 rcu-rscsi alternating with rcu-link, where th
1706 is >= the number of rcu-rscsi links.
1707
1708 Justifying the axiom isn't easy, but it is in
1709 formalization of the Grace Period Guarantee.
1710 through the detailed argument, but the follow
1711 taste of what is involved. Suppose both part
1712 violated: A critical section starts before a
1713 store propagates to the critical section's CP
1714 critical section but doesn't propagate to som
1715 the end of the grace period.
1716
1717 Putting symbols to these ideas, let L and U b
1718 rcu_read_unlock() fence events delimiting the
1719 question, and let S be the synchronize_rcu()
1720 period. Saying that the critical section sta
1721 are events Q and R where Q is po-after L (whi
1722 critical section), Q is "before" R in the sen
1723 relation, and R is po-before the grace period
1724
1725 L ->rcu-link S.
1726
1727 Let W be the store mentioned above, let Y com
1728 critical section and witness that W propagate
1729 section's CPU by reading from W, and let Z on
1730 witness that W has not propagated to that CPU
1731 some event X which is po-after S. Symbolical
1732
1733 S ->po X ->hb* Z ->fr W ->rf Y ->po U
1734
1735 The fr link from Z to W indicates that W has
1736 at the time that Z executes. From this, it c
1737 discussion of the rcu-link relation earlier)
1738 by rcu-link:
1739
1740 S ->rcu-link U.
1741
1742 Since S is a grace period we have S ->rcu-gp
1743 the start and end of the critical section C w
1744 From this we obtain:
1745
1746 S ->rcu-gp S ->rcu-link U ->rcu-rscsi
1747
1748 a forbidden cycle. Thus the "rcu" axiom rule
1749 the Grace Period Guarantee.
1750
1751 For something a little more down-to-earth, le
1752 works out in practice. Consider the RCU code
1753 time with statement labels added:
1754
1755 int x, y;
1756
1757 P0()
1758 {
1759 L: rcu_read_lock();
1760 X: WRITE_ONCE(x, 1);
1761 Y: WRITE_ONCE(y, 1);
1762 U: rcu_read_unlock();
1763 }
1764
1765 P1()
1766 {
1767 int r1, r2;
1768
1769 Z: r1 = READ_ONCE(x);
1770 S: synchronize_rcu();
1771 W: r2 = READ_ONCE(y);
1772 }
1773
1774
1775 If r2 = 0 at the end then P0's store at Y ove
1776 P1's load at W reads from, so we have W ->fre
1777 also Y ->po U, we get S ->rcu-link U. In add
1778 because S is a grace period.
1779
1780 If r1 = 1 at the end then P1's load at Z read
1781 so we have X ->rfe Z. Together with L ->po X
1782 yields L ->rcu-link S. And since L and U are
1783 critical section, we have U ->rcu-rscsi L.
1784
1785 Then U ->rcu-rscsi L ->rcu-link S ->rcu-gp S
1786 forbidden cycle, violating the "rcu" axiom.
1787 allowed by the LKMM, as we would expect.
1788
1789 For contrast, let's see what can happen in a
1790
1791 int x, y, z;
1792
1793 P0()
1794 {
1795 int r0;
1796
1797 L0: rcu_read_lock();
1798 r0 = READ_ONCE(x);
1799 WRITE_ONCE(y, 1);
1800 U0: rcu_read_unlock();
1801 }
1802
1803 P1()
1804 {
1805 int r1;
1806
1807 r1 = READ_ONCE(y);
1808 S1: synchronize_rcu();
1809 WRITE_ONCE(z, 1);
1810 }
1811
1812 P2()
1813 {
1814 int r2;
1815
1816 L2: rcu_read_lock();
1817 r2 = READ_ONCE(z);
1818 WRITE_ONCE(x, 1);
1819 U2: rcu_read_unlock();
1820 }
1821
1822 If r0 = r1 = r2 = 1 at the end, then similar
1823 that U0 ->rcu-rscsi L0 ->rcu-link S1 ->rcu-gp
1824 L2 ->rcu-link U0. However this cycle is not
1825 sequence of relations contains fewer instance
1826 rcu-rscsi (two). Consequently the outcome is
1827 The following instruction timing diagram show
1828 occur:
1829
1830 P0 P1
1831 -------------------- --------------------
1832 rcu_read_lock()
1833 WRITE_ONCE(y, 1)
1834 r1 = READ_ONCE(y)
1835 synchronize_rcu() sta
1836 .
1837 .
1838 r0 = READ_ONCE(x) .
1839 rcu_read_unlock() .
1840 synchronize_rcu() end
1841 WRITE_ONCE(z, 1)
1842
1843
1844
1845 This requires P0 and P2 to execute their load
1846 program order, but of course they are allowed
1847 can see, the Grace Period Guarantee is not vi
1848 section in P0 both starts before P1's grace p
1849 before it does, and the critical section in P
1850 grace period does and ends after it does.
1851
1852 The LKMM supports SRCU (Sleepable Read-Copy-U
1853 normal RCU. The ideas involved are much the
1854 relations srcu-gp and srcu-rscsi added to rep
1855 and read-side critical sections. However, th
1856 differences between RCU read-side critical se
1857 counterparts, as described in the next sectio
1858
1859
1860 SRCU READ-SIDE CRITICAL SECTIONS
1861 --------------------------------
1862
1863 The LKMM uses the srcu-rscsi relation to mode
1864 sections. They differ from RCU read-side cri
1865 following respects:
1866
1867 1. Unlike the analogous RCU primitives,
1868 srcu_read_lock(), and srcu_read_unloc
1869 struct srcu_struct as an argument. T
1870 an SRCU domain, and calls linked by s
1871 same domain. Read-side critical sect
1872 associated with different domains are
1873 another; the SRCU version of the RCU
1874 to pairs of critical sections and gra
1875 same domain.
1876
1877 2. srcu_read_lock() returns a value, cal
1878 be passed to the matching srcu_read_u
1879 rcu_read_lock() and rcu_read_unlock()
1880 call does not always have to match th
1881 srcu_read_unlock(). In fact, it is p
1882 read-side critical sections to overla
1883 following example (where s is an srcu
1884 are integer variables):
1885
1886 idx1 = srcu_read_lock(&s);
1887 idx2 = srcu_read_lock(&s);
1888 srcu_read_unlock(&s, idx1);
1889 srcu_read_unlock(&s, idx2);
1890
1891 The matching is determined entirely b
1892 index value. By contrast, if the cal
1893 rcu_read_lock() and rcu_read_unlock()
1894 created two nested (fully overlapping
1895 sections: an inner one and an outer o
1896
1897 3. The srcu_down_read() and srcu_up_read
1898 exactly like srcu_read_lock() and src
1899 that matching calls don't have to exe
1900 (The names are meant to be suggestive
1901 semaphores.) Since the matching is d
1902 pointer and index value, these primit
1903 an SRCU read-side critical section to
1904 on another, so to speak.
1905
1906 In order to account for these properties of S
1907 srcu_read_lock() as a special type of load ev
1908 appropriate, since it takes a memory location
1909 a value, just as a load does) and srcu_read_u
1910 of store event (again appropriate, since it t
1911 memory location and a value). These loads an
1912 belonging to the "srcu-lock" and "srcu-unlock
1913 respectively.
1914
1915 This approach allows the LKMM to tell whether
1916 associated with the same SRCU domain, simply
1917 access the same memory location (i.e., they a
1918 relation). It also gives a way to tell which
1919 particular lock, by checking for the presence
1920 from the load (srcu-lock) to the store (srcu-
1921 given the situation outlined earlier (with st
1922
1923 A: idx1 = srcu_read_lock(&s);
1924 B: idx2 = srcu_read_lock(&s);
1925 C: srcu_read_unlock(&s, idx1);
1926 D: srcu_read_unlock(&s, idx2);
1927
1928 the LKMM will treat A and B as loads from s y
1929 idx1 and idx2 respectively. Similarly, it wi
1930 though they stored the values from idx1 and i
1931 is much as if we had written:
1932
1933 A: idx1 = READ_ONCE(s);
1934 B: idx2 = READ_ONCE(s);
1935 C: WRITE_ONCE(s, idx1);
1936 D: WRITE_ONCE(s, idx2);
1937
1938 except for the presence of the special srcu-l
1939 annotations. You can see at once that we hav
1940 B ->data D. These dependencies tell the LKMM
1941 srcu-unlock event matching srcu-lock event A,
1942 srcu-unlock event matching srcu-lock event B.
1943
1944 This approach is admittedly a hack, and it ha
1945 to problems. For example, in:
1946
1947 idx1 = srcu_read_lock(&s);
1948 srcu_read_unlock(&s, idx1);
1949 idx2 = srcu_read_lock(&s);
1950 srcu_read_unlock(&s, idx2);
1951
1952 the LKMM will believe that idx2 must have the
1953 since it reads from the immediately preceding
1954 Fortunately this won't matter, assuming that
1955 anything with SRCU index values other than pa
1956 srcu_read_unlock() or srcu_up_read() calls.
1957
1958 However, sometimes it is necessary to store a
1959 shared variable temporarily. In fact, this i
1960 srcu_down_read() to pass the index it gets to
1961 on a different CPU. In more detail, we might
1962
1963 struct srcu_struct s;
1964 int x;
1965
1966 P0()
1967 {
1968 int r0;
1969
1970 A: r0 = srcu_down_read(&s);
1971 B: WRITE_ONCE(x, r0);
1972 }
1973
1974 P1()
1975 {
1976 int r1;
1977
1978 C: r1 = READ_ONCE(x);
1979 D: srcu_up_read(&s, r1);
1980 }
1981
1982 Assuming that P1 executes after P0 and does r
1983 stored in x, we can write this (using bracket
1984 annotations) as:
1985
1986 A[srcu-lock] ->data B[once] ->rf C[on
1987
1988 The LKMM defines a carry-srcu-data relation t
1989 it permits an arbitrarily long sequence of
1990
1991 data ; rf
1992
1993 pairs (that is, a data link followed by an rf
1994 an srcu-lock event and the final data depende
1995 matching srcu-unlock event. carry-srcu-data
1996 need to ensure that none of the intermediate
1997 sequence are instances of srcu-unlock. This
1998 pattern like the one above:
1999
2000 A: idx1 = srcu_read_lock(&s);
2001 B: srcu_read_unlock(&s, idx1);
2002 C: idx2 = srcu_read_lock(&s);
2003 D: srcu_read_unlock(&s, idx2);
2004
2005 the LKMM treats B as a store to the variable
2006 that variable, creating an undesirable rf lin
2007
2008 A ->data B ->rf C ->data D.
2009
2010 This would cause carry-srcu-data to mistakenl
2011 dependency from A to D, giving the impression
2012 srcu-unlock event matching A's srcu-lock. To
2013 carry-srcu-data does not accept sequences in
2014 the intermediate ->data links (B above) is an
2015
2016
2017 LOCKING
2018 -------
2019
2020 The LKMM includes locking. In fact, there is
2021 in the formal model, added in order to make t
2022 However, this special code is intended to be
2023 to concepts we have already covered. A spinl
2024 the same as an int, and spin_lock(&s) is trea
2025
2026 while (cmpxchg_acquire(&s, 0, 1) != 0
2027 cpu_relax();
2028
2029 This waits until s is equal to 0 and then ato
2030 and the read part of the cmpxchg operation ac
2031 An alternate way to express the same thing wo
2032
2033 r = xchg_acquire(&s, 1);
2034
2035 along with a requirement that at the end, r =
2036 spin_trylock(&s) is treated almost the same a
2037
2038 return !cmpxchg_acquire(&s, 0, 1);
2039
2040 which atomically sets s to 1 if it is current
2041 true if it succeeds (the read part of the cmp
2042 acquire fence only if the operation is succes
2043 is treated almost the same as:
2044
2045 smp_store_release(&s, 0);
2046
2047 The "almost" qualifiers above need some expla
2048 store-release in a spin_unlock() and the load
2049 first half of the atomic rmw update in a spin
2050 spin_trylock() -- we can call these things lo
2051 lock-acquires -- have two properties beyond t
2052 and acquires.
2053
2054 First, when a lock-acquire reads from or is p
2055 the LKMM requires that every instruction po-b
2056 must execute before any instruction po-after
2057 would naturally hold if the release and acqui
2058 different CPUs and accessed the same lock var
2059 it also holds when they are on the same CPU,
2060 different lock variables. For example:
2061
2062 int x, y;
2063 spinlock_t s, t;
2064
2065 P0()
2066 {
2067 int r1, r2;
2068
2069 spin_lock(&s);
2070 r1 = READ_ONCE(x);
2071 spin_unlock(&s);
2072 spin_lock(&t);
2073 r2 = READ_ONCE(y);
2074 spin_unlock(&t);
2075 }
2076
2077 P1()
2078 {
2079 WRITE_ONCE(y, 1);
2080 smp_wmb();
2081 WRITE_ONCE(x, 1);
2082 }
2083
2084 Here the second spin_lock() is po-after the f
2085 therefore the load of x must execute before t
2086 the two locking operations use different lock
2087 r1 = 1 and r2 = 0 at the end (this is an inst
2088
2089 This requirement does not apply to ordinary r
2090 fences, only to lock-related operations. For
2091 in the example had been written as:
2092
2093 P0()
2094 {
2095 int r1, r2, r3;
2096
2097 r1 = READ_ONCE(x);
2098 smp_store_release(&s, 1);
2099 r3 = smp_load_acquire(&s);
2100 r2 = READ_ONCE(y);
2101 }
2102
2103 Then the CPU would be allowed to forward the
2104 smp_store_release() to the smp_load_acquire()
2105 instructions in the following order:
2106
2107 r3 = smp_load_acquire(&s);
2108 r2 = READ_ONCE(y);
2109 r1 = READ_ONCE(x);
2110 smp_store_release(&s, 1);
2111
2112 and thus it could load y before x, obtaining
2113
2114 Second, when a lock-acquire reads from or is
2115 and some other stores W and W' occur po-befor
2116 po-after the lock-acquire respectively, the L
2117 propagate to each CPU before W' does. For ex
2118
2119 int x, y;
2120 spinlock_t s;
2121
2122 P0()
2123 {
2124 spin_lock(&s);
2125 WRITE_ONCE(x, 1);
2126 spin_unlock(&s);
2127 }
2128
2129 P1()
2130 {
2131 int r1;
2132
2133 spin_lock(&s);
2134 r1 = READ_ONCE(x);
2135 WRITE_ONCE(y, 1);
2136 spin_unlock(&s);
2137 }
2138
2139 P2()
2140 {
2141 int r2, r3;
2142
2143 r2 = READ_ONCE(y);
2144 smp_rmb();
2145 r3 = READ_ONCE(x);
2146 }
2147
2148 If r1 = 1 at the end then the spin_lock() in
2149 the spin_unlock() in P0. Hence the store to
2150 before the store to y does, so we cannot have
2151 if P1 had used a lock variable different from
2152 propagated in either order. (On the other ha
2153 P1 had all executed on a single CPU, as in th
2154 one, then the writes would have propagated in
2155 critical sections used different lock variabl
2156
2157 These two special requirements for lock-relea
2158 not arise from the operational model. Nevert
2159 have come to expect and rely on them because
2160 architectures supported by the Linux kernel,
2161 differing reasons.
2162
2163
2164 PLAIN ACCESSES AND DATA RACES
2165 -----------------------------
2166
2167 In the LKMM, memory accesses such as READ_ONC
2168 smp_load_acquire(&z), and so on are collectiv
2169 "marked" accesses, because they are all annot
2170 operations of one kind or another. Ordinary
2171 accesses such as x or y = 0 are simply called
2172
2173 Early versions of the LKMM had nothing to say
2174 The C standard allows compilers to assume tha
2175 by plain accesses are not concurrently read o
2176 threads or CPUs. This leaves compilers free
2177 of transformations or optimizations of code c
2178 making such code very difficult for a memory
2179
2180 Here is just one example of a possible pitfal
2181
2182 int a = 6;
2183 int *x = &a;
2184
2185 P0()
2186 {
2187 int *r1;
2188 int r2 = 0;
2189
2190 r1 = x;
2191 if (r1 != NULL)
2192 r2 = READ_ONCE(*r1);
2193 }
2194
2195 P1()
2196 {
2197 WRITE_ONCE(x, NULL);
2198 }
2199
2200 On the face of it, one would expect that when
2201 possible final values for r2 are 6 and 0, dep
2202 P1's store to x propagates to P0 before P0's
2203 But since P0's load from x is a plain access,
2204 to carry out the load twice (for the comparis
2205 for the READ_ONCE()) and eliminate the tempor
2206 object code generated for P0 could therefore
2207 like this:
2208
2209 P0()
2210 {
2211 int r2 = 0;
2212
2213 if (x != NULL)
2214 r2 = READ_ONCE(*x);
2215 }
2216
2217 And now it is obvious that this code runs the
2218 NULL pointer, because P1's store to x might p
2219 test against NULL has been made but before th
2220 If the original code had said "r1 = READ_ONCE
2221 the compiler would not have performed this op
2222 would be no possibility of a NULL-pointer der
2223
2224 Given the possibility of transformations like
2225 doesn't try to predict all possible outcomes
2226 accesses. It is instead content to determine
2227 violates the compiler's assumptions, which wo
2228 outcome undefined.
2229
2230 In technical terms, the compiler is allowed t
2231 program executes, there will not be any data
2232 occurs when there are two memory accesses suc
2233
2234 1. they access the same location,
2235
2236 2. at least one of them is a store,
2237
2238 3. at least one of them is plain,
2239
2240 4. they occur on different CPUs (or in d
2241 same CPU), and
2242
2243 5. they execute concurrently.
2244
2245 In the literature, two accesses are said to "
2246 1 and 2 above. We'll go a little farther and
2247 are "race candidates" if they satisfy 1 - 4.
2248 race candidates actually do race in a given e
2249 whether they are concurrent.
2250
2251 The LKMM tries to determine whether a program
2252 which may execute concurrently; if it does th
2253 a potential data race and makes no prediction
2254 outcome.
2255
2256 Determining whether two accesses are race can
2257 see that all the concepts involved in the def
2258 part of the memory model. The hard part is t
2259 execute concurrently. The LKMM takes a conse
2260 assuming that accesses may be concurrent unle
2261 are not.
2262
2263 If two memory accesses aren't concurrent then
2264 the other. Therefore the LKMM decides two ac
2265 if they can be connected by a sequence of hb,
2266 (together referred to as xb, for "executes be
2267 are two complicating factors.
2268
2269 If X is a load and X executes before a store
2270 no danger of X and Y being concurrent. After
2271 effect on the value obtained by X until the m
2272 propagated Y from its own CPU to X's CPU, whi
2273 some time after Y executes and thus after X e
2274 store, then even if X executes before Y it is
2275 will propagate to Y's CPU just as Y is execut
2276 could very well interfere somehow with Y, and
2277 consider X and Y to be concurrent.
2278
2279 Therefore when X is a store, for X and Y to b
2280 requires not only that X must execute before
2281 propagate to Y's CPU before Y executes. (Or
2282 Y executes before X -- then Y must propagate
2283 executes if Y is a store.) This is expressed
2284 relation (vis), where X ->vis Y is defined to
2285 intermediate event Z such that:
2286
2287 X is connected to Z by a possibly emp
2288 cumul-fence links followed by an opti
2289 these links are present, X and Z are
2290
2291 and either:
2292
2293 Z is connected to Y by a strong-fence
2294 possibly empty sequence of xb links,
2295
2296 or:
2297
2298 Z is on the same CPU as Y and is conn
2299 empty sequence of xb links (again, if
2300 means Z and Y are the same event).
2301
2302 The motivations behind this definition are st
2303
2304 cumul-fence memory barriers force sto
2305 the barrier to propagate to other CPU
2306 po-after the barrier.
2307
2308 An rfe link from an event W to an eve
2309 from W, which certainly means that W
2310 R's CPU before R executed.
2311
2312 strong-fence memory barriers force st
2313 the barrier, or that propagate to the
2314 barrier executes, to propagate to all
2315 po-after the barrier can execute.
2316
2317 To see how this works out in practice, consid
2318 pattern (with fences and statement labels, bu
2319 test):
2320
2321 int buf = 0, flag = 0;
2322
2323 P0()
2324 {
2325 X: WRITE_ONCE(buf, 1);
2326 smp_wmb();
2327 W: WRITE_ONCE(flag, 1);
2328 }
2329
2330 P1()
2331 {
2332 int r1;
2333 int r2 = 0;
2334
2335 Z: r1 = READ_ONCE(flag);
2336 smp_rmb();
2337 Y: r2 = READ_ONCE(buf);
2338 }
2339
2340 The smp_wmb() memory barrier gives a cumul-fe
2341 assuming r1 = 1 at the end, there is an rfe l
2342 means that the store to buf must propagate fr
2343 executes. Next, Z and Y are on the same CPU
2344 provides an xb link from Z to Y (i.e., it for
2345 Y). Therefore we have X ->vis Y: X must prop
2346 executes.
2347
2348 The second complicating factor mentioned abov
2349 that when we are considering data races, some
2350 are plain. Now, although we have not said so
2351 point most of the relations defined by the LK
2352 cumul-fence, pb, and so on -- including vis)
2353 accesses.
2354
2355 There are good reasons for this restriction.
2356 allowed to apply fancy transformations to mar
2357 consequently each such access in the source c
2358 less directly to a single machine instruction
2359 plain accesses are a different story; the com
2360 split them up, duplicate them, eliminate them
2361 who knows what else. Seeing a plain access i
2362 you almost nothing about what machine instruc
2363 object code.
2364
2365 Fortunately, the compiler isn't completely fr
2366 limitations. For one, it is not allowed to i
2367 the object code if the source code does not a
2368 race (if it could, memory models would be use
2369 code would be safe!). For another, it cannot
2370 a compiler barrier.
2371
2372 A compiler barrier is a kind of fence, but as
2373 only affects the compiler; it does not necess
2374 how instructions are executed by the CPU. In
2375 code, the barrier() function is a compiler ba
2376 rise directly to any machine instructions in
2377 it affects how the compiler generates the res
2378 Given source code like this:
2379
2380 ... some memory accesses ...
2381 barrier();
2382 ... some other memory accesses ...
2383
2384 the barrier() function ensures that the machi
2385 corresponding to the first group of accesses
2386 any machine instructions corresponding to the
2387 -- even if some of the accesses are plain. (
2388 then execute some of those accesses out of pr
2389 already know how to deal with such issues.)
2390 there would be no such guarantee; the two gro
2391 intermingled or even reversed in the object c
2392
2393 The LKMM doesn't say much about the barrier()
2394 require that all fences are also compiler bar
2395 requires that the ordering properties of memo
2396 smp_rmb() or smp_store_release() apply to pla
2397 marked accesses.
2398
2399 This is the key to analyzing data races. Con
2400 again, now using plain accesses for buf:
2401
2402 int buf = 0, flag = 0;
2403
2404 P0()
2405 {
2406 U: buf = 1;
2407 smp_wmb();
2408 X: WRITE_ONCE(flag, 1);
2409 }
2410
2411 P1()
2412 {
2413 int r1;
2414 int r2 = 0;
2415
2416 Y: r1 = READ_ONCE(flag);
2417 if (r1) {
2418 smp_rmb();
2419 V: r2 = buf;
2420 }
2421 }
2422
2423 This program does not contain a data race. A
2424 accesses are race candidates, the LKMM can pr
2425 concurrent as follows:
2426
2427 The smp_wmb() fence in P0 is both a c
2428 cumul-fence. It guarantees that no m
2429 machine instructions the compiler gen
2430 access U, all those instructions will
2431 Consequently U's store to buf, no mat
2432 at the machine level, must propagate
2433 flag does.
2434
2435 X and Y are both marked accesses. He
2436 Y is a valid indicator that X propaga
2437 executed, i.e., X ->vis Y. (And if t
2438 r1 will be 0, so V will not be execut
2439 race with U.)
2440
2441 The smp_rmb() fence in P1 is a compil
2442 fence. It guarantees that all the ma
2443 corresponding to the access V will be
2444 therefore any loads among those instr
2445 after the fence does and hence after
2446
2447 Thus U's store to buf is forced to propagate
2448 executes (assuming V does execute), ruling ou
2449 data race between them.
2450
2451 This analysis illustrates how the LKMM deals
2452 general. Suppose R is a plain load and we wa
2453 executes before some marked access E. We can
2454 marked access X such that R and X are ordered
2455 X ->xb* E. If E was also a plain access, we
2456 marked access Y such that X ->xb* Y, and Y an
2457 fence. We describe this arrangement by sayin
2458 "post-bounded" by X and E is "pre-bounded" by
2459
2460 In fact, we go one step further: Since R is a
2461 "r-post-bounded" by X. Similarly, E would be
2462 "w-pre-bounded" by Y, depending on whether E
2463 This distinction is needed because some fence
2464 (i.e., smp_rmb()) and some affect only stores
2465 the two types of bounds are the same. And as
2466 say that a marked access pre-bounds and post-
2467 above were a marked load then X could simply
2468
2469 The need to distinguish between r- and w-boun
2470 issue. When the source code contains a plain
2471 allowed to put plain loads of the same locati
2472 For example, given the source code:
2473
2474 x = 1;
2475
2476 the compiler is theoretically allowed to gene
2477 looks like:
2478
2479 if (x != 1)
2480 x = 1;
2481
2482 thereby adding a load (and possibly replacing
2483 For this reason, whenever the LKMM requires a
2484 w-pre-bounded or w-post-bounded by a marked a
2485 the store to be r-pre-bounded or r-post-bound
2486 where the compiler adds a load.
2487
2488 (This may be overly cautious. We don't know
2489 compiler has augmented a store with a load in
2490 Linux kernel developers would probably fight
2491 compiler if it ever did this. Still, better
2492
2493 Incidentally, the other tranformation -- augm
2494 adding in a store to the same location -- is
2495 because the compiler cannot know whether any
2496 a concurrent load from that location. Two co
2497 constitute a race (they can't interfere with
2498 does race with a concurrent load. Thus addin
2499 data race where one was not already present i
2500 something the compiler is forbidden to do. A
2501 load, on the other hand, is acceptable becaus
2502 data race unless one already existed.
2503
2504 The LKMM includes a second way to pre-bound p
2505 addition to fences: an address dependency fro
2506 is, in the sequence:
2507
2508 p = READ_ONCE(ptr);
2509 r = *p;
2510
2511 the LKMM says that the marked load of ptr pre
2512 *p; the marked load must execute before any o
2513 instructions corresponding to the plain load.
2514 stipulation, since after all, the CPU can't p
2515 until it knows what value p will hold. Furth
2516 assumption like this one, some usages typical
2517 data races. For example:
2518
2519 int a = 1, b;
2520 int *ptr = &a;
2521
2522 P0()
2523 {
2524 b = 2;
2525 rcu_assign_pointer(ptr, &b);
2526 }
2527
2528 P1()
2529 {
2530 int *p;
2531 int r;
2532
2533 rcu_read_lock();
2534 p = rcu_dereference(ptr);
2535 r = *p;
2536 rcu_read_unlock();
2537 }
2538
2539 (In this example the rcu_read_lock() and rcu_
2540 really do anything, because there aren't any
2541 included merely for the sake of good form; ty
2542 synchronize_rcu() somewhere after the rcu_ass
2543
2544 rcu_assign_pointer() performs a store-release
2545 is definitely w-post-bounded before the store
2546 stores will propagate to P1 in that order. H
2547 is only equivalent to READ_ONCE(). While it
2548 not a fence or compiler barrier. Hence the o
2549 that the load of ptr in P1 is r-pre-bounded b
2550 (thus avoiding a race) is the assumption abou
2551
2552 This is a situation where the compiler can un
2553 and a certain amount of care is required when
2554 like this one. In particular, comparisons be
2555 other known addresses can cause trouble. If
2556
2557 p = rcu_dereference(ptr);
2558 if (p == &x)
2559 r = *p;
2560
2561 then the compiler just might generate object
2562
2563 p = rcu_dereference(ptr);
2564 if (p == &x)
2565 r = x;
2566
2567 or even:
2568
2569 rtemp = x;
2570 p = rcu_dereference(ptr);
2571 if (p == &x)
2572 r = rtemp;
2573
2574 which would invalidate the memory model's ass
2575 could now perform the load of x before the lo
2576 a control dependency but no address dependenc
2577
2578 Finally, it turns out there is a situation in
2579 not need to be w-post-bounded: when it is sep
2580 race-candidate access by a fence. At first g
2581 impossible. After all, to be race candidates
2582 be on different CPUs, and fences don't link e
2583 Well, normal fences don't -- but rcu-fence ca
2584
2585 int x, y;
2586
2587 P0()
2588 {
2589 WRITE_ONCE(x, 1);
2590 synchronize_rcu();
2591 y = 3;
2592 }
2593
2594 P1()
2595 {
2596 rcu_read_lock();
2597 if (READ_ONCE(x) == 0)
2598 y = 2;
2599 rcu_read_unlock();
2600 }
2601
2602 Do the plain stores to y race? Clearly not i
2603 value for x, so let's assume the READ_ONCE(x)
2604 means that the read-side critical section in
2605 before the grace period in P0 does, because R
2606 Guarantee says that otherwise P0's store to x
2607 P1 before the critical section started and so
2608 to the READ_ONCE(). (Another way of putting
2609 from the READ_ONCE() to the WRITE_ONCE() give
2610 between those two events.)
2611
2612 This means there is an rcu-fence link from P1
2613 "y = 3" store, and consequently the first mus
2614 before the second can execute. Therefore the
2615 concurrent and there is no race, even though
2616 isn't w-post-bounded by any marked accesses.
2617
2618 Putting all this material together yields the
2619 race-candidate stores W and W', where W ->co
2620 stores don't race if W can be linked to W' by
2621
2622 w-post-bounded ; vis ; w-pre-bounded
2623
2624 sequence. If W is plain then they also have
2625
2626 r-post-bounded ; xb* ; w-pre-bounded
2627
2628 sequence, and if W' is plain then they also h
2629
2630 w-post-bounded ; vis ; r-pre-bounded
2631
2632 sequence. For race-candidate load R and stor
2633 two accesses don't race if R can be linked to
2634
2635 r-post-bounded ; xb* ; w-pre-bounded
2636
2637 sequence or if W can be linked to R by a
2638
2639 w-post-bounded ; vis ; r-pre-bounded
2640
2641 sequence. For the cases involving a vis link
2642 sequences in which W is linked to W' or R by
2643
2644 strong-fence ; xb* ; {w and/or r}-pre
2645
2646 sequence with no post-bounding, and in every
2647 the link simply to be a fence with no boundin
2648 of the appropriate sort exists, the LKMM says
2649
2650 There is one more part of the LKMM related to
2651 not to data races) we should discuss. Recall
2652 as hb are limited to marked accesses only. A
2653 happens-before, propagates-before, and rcu ax
2654 various relation must not contain a cycle) do
2655 accesses. Nevertheless, we do want to rule o
2656 they don't make sense even for plain accesses
2657
2658 To this end, the LKMM imposes three extra res
2659 called the "plain-coherence" axiom because of
2660 rules used by the operational model to ensure
2661 is, the rules governing the memory subsystem'
2662 satisfy a load request and its determination
2663 fall in the coherence order):
2664
2665 If R and W are race candidates and it
2666 W by one of the xb* sequences listed
2667 not allowed (i.e., a load cannot read
2668 executes before, even if one or both
2669
2670 If W and R are race candidates and it
2671 R by one of the vis sequences listed
2672 not allowed (i.e., if a store is visi
2673 load must read from that store or one
2674
2675 If W and W' are race candidates and i
2676 to W' by one of the vis sequences lis
2677 is not allowed (i.e., if one store is
2678 the second must come after the first
2679
2680 This is the extent to which the LKMM deals wi
2681 Perhaps it could say more (for example, plain
2682 contribute to the ppo relation), but at the m
2683 minimal, conservative approach is good enough
2684
2685
2686 ODDS AND ENDS
2687 -------------
2688
2689 This section covers material that didn't quit
2690 earlier sections.
2691
2692 The descriptions in this document don't alway
2693 version of the LKMM exactly. For example, th
2694 definition of the prop relation makes the ini
2695 optional, and it doesn't require the events l
2696 be on the same CPU. These differences are ve
2697 instances where the coe/fre part of prop is m
2698 because all the other parts (fences and rfe)
2699 hb anyway, and where the formal model adds pr
2700 an explicit requirement that the events being
2701 CPU.
2702
2703 Another minor difference has to do with event
2704 accesses and fences, such as those correspond
2705 calls. In the formal model, these events are
2706 and fences; rather, they are read events with
2707 them as acquires. (Or write events annotated
2708 smp_store_release().) The final effect is th
2709
2710 Although we didn't mention it above, the inst
2711 ordering provided by the smp_rmb() fence does
2712 that are part of a non-value-returning atomic
2713 given:
2714
2715 atomic_inc(&x);
2716 smp_rmb();
2717 r1 = READ_ONCE(y);
2718
2719 it is not guaranteed that the load from y wil
2720 update to x. This is because the ARMv8 archi
2721 non-value-returning atomic operations effecti
2722 the CPU. Basically, the CPU tells the memory
2723 x, and then the increment is carried out by t
2724 no further involvement from the CPU. Since t
2725 the value of x, there is nothing for the smp_
2726
2727 The LKMM defines a few extra synchronization
2728 things we have already covered. In particula
2729 treated as READ_ONCE() and rcu_assign_pointer
2730 smp_store_release() -- which is basically how
2731 them.
2732
2733 Although we said that plain accesses are not
2734 relation, they do contribute to it indirectly
2735 an address dependency from a marked load R to
2736 followed by smp_wmb() and then a marked store
2737 ppo link from R to W'. The reasoning behind
2738 shaky, but essentially it says there is no wa
2739 for this source code in which W' could execut
2740 pre-bounding by address dependencies, it is p
2741 to undermine this relation if sufficient care
2742
2743 Secondly, plain accesses can carry dependenci
2744 links a marked load R to a store W, and the s
2745 from the same thread, then the data loaded by
2746 loaded originally by R. Thus, if R' is linked
2747 dependency, R is also linked to access X by t
2748 if W' or R' (or both!) are plain.
2749
2750 There are a few oddball fences which need spe
2751 smp_mb__before_atomic(), smp_mb__after_atomic
2752 smp_mb__after_spinlock(). The LKMM uses fenc
2753 annotations for them; they act as strong fenc
2754 except for the sets of events that they order
2755 all po-earlier events against all po-later ev
2756 they behave as follows:
2757
2758 smp_mb__before_atomic() orders all po
2759 po-later atomic updates and the event
2760
2761 smp_mb__after_atomic() orders po-earl
2762 the events preceding them against all
2763
2764 smp_mb__after_spinlock() orders po-ea
2765 events and the events preceding them
2766 events.
2767
2768 Interestingly, RCU and locking each introduce
2769 deadlock. When faced with code sequences suc
2770
2771 spin_lock(&s);
2772 spin_lock(&s);
2773 spin_unlock(&s);
2774 spin_unlock(&s);
2775
2776 or:
2777
2778 rcu_read_lock();
2779 synchronize_rcu();
2780 rcu_read_unlock();
2781
2782 what does the LKMM have to say? Answer: It s
2783 executions at all, which makes sense. But th
2784 misleading results, because if a piece of cod
2785 executions, some of which deadlock, the model
2786 non-deadlocking executions. For example:
2787
2788 int x, y;
2789
2790 P0()
2791 {
2792 int r0;
2793
2794 WRITE_ONCE(x, 1);
2795 r0 = READ_ONCE(y);
2796 }
2797
2798 P1()
2799 {
2800 rcu_read_lock();
2801 if (READ_ONCE(x) > 0) {
2802 WRITE_ONCE(y, 36);
2803 synchronize_rcu();
2804 }
2805 rcu_read_unlock();
2806 }
2807
2808 Is it possible to end up with r0 = 36 at the
2809 you it is not, but the model won't mention th
2810 will self-deadlock in the executions where it
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.