linux/tools/memory-model/Documentation/explanation.txt
<<
>>
Prefs
   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