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.
2560