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