TEXT   54


Guest on 23rd August 2022 12:34:17 PM

  1. Explanation of the Linux-Kernel Memory Consistency Model
  2. ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  4. :Author: Alan Stern <stern@rowland.harvard.edu>
  5. :Created: October
  7. .. Contents
  10.   2. BACKGROUND
  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
  20.   12. THE FROM-READS RELATION: fr, fri, and fre
  22.   14. PROPAGATION ORDER RELATION: cumul-fence
  25.   17. ATOMIC UPDATES: rmw
  30.   22. RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb
  31.   23. LOCKING
  33.   25. ODDS AND ENDS
  38. ------------
  40. The Linux-kernel memory consistency model (LKMM) is rather complex and
  41. obscure.  This is particularly evident if you read through the
  42. linux-kernel.bell and linux-kernel.cat files that make up the formal
  43. version of the model; they are extremely terse and their meanings are
  44. far from clear.
  46. This document describes the ideas underlying the LKMM.  It is meant
  47. for people who want to understand how the model was designed.  It does
  48. not go into the details of the code in the .bell and .cat files;
  49. rather, it explains in English what the code expresses symbolically.
  51. Sections 2 (BACKGROUND) through 5 (ORDERING AND CYCLES) are aimed
  52. toward beginners; they explain what memory consistency models are and
  53. the basic notions shared by all such models.  People already familiar
  54. with these concepts can skim or skip over them.  Sections 6 (EVENTS)
  55. through 12 (THE FROM_READS RELATION) describe the fundamental
  56. relations used in many models.  Starting in Section 13 (AN OPERATIONAL
  57. MODEL), the workings of the LKMM itself are covered.
  59. Warning: The code examples in this document are not written in the
  60. proper format for litmus tests.  They don't include a header line, the
  61. initializations are not enclosed in braces, the global variables are
  62. not passed by pointers, and they don't have an "exists" clause at the
  63. end.  Converting them to the right format is left as an exercise for
  64. the reader.
  68. ----------
  70. A memory consistency model (or just memory model, for short) is
  71. something which predicts, given a piece of computer code running on a
  72. particular kind of system, what values may be obtained by the code's
  73. load instructions.  The LKMM makes these predictions for code running
  74. as part of the Linux kernel.
  76. In practice, people tend to use memory models the other way around.
  77. That is, given a piece of code and a collection of values specified
  78. for the loads, the model will predict whether it is possible for the
  79. code to run in such a way that the loads will indeed obtain the
  80. specified values.  Of course, this is just another way of expressing
  81. the same idea.
  83. For code running on a uniprocessor system, the predictions are easy:
  84. Each load instruction must obtain the value written by the most recent
  85. store instruction accessing the same location (we ignore complicating
  86. factors such as DMA and mixed-size accesses.)  But on multiprocessor
  87. systems, with multiple CPUs making concurrent accesses to shared
  88. memory locations, things aren't so simple.
  90. Different architectures have differing memory models, and the Linux
  91. kernel supports a variety of architectures.  The LKMM has to be fairly
  92. permissive, in the sense that any behavior allowed by one of these
  93. architectures also has to be allowed by the LKMM.
  97. ----------------
  99. Here is a simple example to illustrate the basic concepts.  Consider
  100. some code running as part of a device driver for an input device.  The
  101. driver might contain an interrupt handler which collects data from the
  102. device, stores it in a buffer, and sets a flag to indicate the buffer
  103. is full.  Running concurrently on a different CPU might be a part of
  104. the driver code being executed by a process in the midst of a read(2)
  105. system call.  This code tests the flag to see whether the buffer is
  106. ready, and if it is, copies the data back to userspace.  The buffer
  107. and the flag are memory locations shared between the two CPUs.
  109. We can abstract out the important pieces of the driver code as follows
  110. (the reason for using WRITE_ONCE() and READ_ONCE() instead of simple
  111. assignment statements is discussed later):
  113.         int buf = 0, flag = 0;
  115.         P0()
  116.         {
  117.                 WRITE_ONCE(buf, 1);
  118.                 WRITE_ONCE(flag, 1);
  119.         }
  121.         P1()
  122.         {
  123.                 int r1;
  124.                 int r2 = 0;
  126.                 r1 = READ_ONCE(flag);
  127.                 if (r1)
  128.                         r2 = READ_ONCE(buf);
  129.         }
  131. Here the P0() function represents the interrupt handler running on one
  132. CPU and P1() represents the read() routine running on another.  The
  133. value 1 stored in buf represents input data collected from the device.
  134. Thus, P0 stores the data in buf and then sets flag.  Meanwhile, P1
  135. reads flag into the private variable r1, and if it is set, reads the
  136. data from buf into a second private variable r2 for copying to
  137. userspace.  (Presumably if flag is not set then the driver will wait a
  138. while and try again.)
  140. This pattern of memory accesses, where one CPU stores values to two
  141. shared memory locations and another CPU loads from those locations in
  142. the opposite order, is widely known as the "Message Passing" or MP
  143. pattern.  It is typical of memory access patterns in the kernel.
  145. Please note that this example code is a simplified abstraction.  Real
  146. buffers are usually larger than a single integer, real device drivers
  147. usually use sleep and wakeup mechanisms rather than polling for I/O
  148. completion, and real code generally doesn't bother to copy values into
  149. private variables before using them.  All that is beside the point;
  150. the idea here is simply to illustrate the overall pattern of memory
  151. accesses by the CPUs.
  153. A memory model will predict what values P1 might obtain for its loads
  154. from flag and buf, or equivalently, what values r1 and r2 might end up
  155. with after the code has finished running.
  157. Some predictions are trivial.  For instance, no sane memory model would
  158. predict that r1 = 42 or r2 = -7, because neither of those values ever
  159. gets stored in flag or buf.
  161. Some nontrivial predictions are nonetheless quite simple.  For
  162. instance, P1 might run entirely before P0 begins, in which case r1 and
  163. r2 will both be 0 at the end.  Or P0 might run entirely before P1
  164. begins, in which case r1 and r2 will both be 1.
  166. The interesting predictions concern what might happen when the two
  167. routines run concurrently.  One possibility is that P1 runs after P0's
  168. store to buf but before the store to flag.  In this case, r1 and r2
  169. will again both be 0.  (If P1 had been designed to read buf
  170. unconditionally then we would instead have r1 = 0 and r2 = 1.)
  172. However, the most interesting possibility is where r1 = 1 and r2 = 0.
  173. If this were to occur it would mean the driver contains a bug, because
  174. incorrect data would get sent to the user: 0 instead of 1.  As it
  175. happens, the LKMM does predict this outcome can occur, and the example
  176. driver code shown above is indeed buggy.
  180. ----------------------------
  182. The first widely cited memory model, and the simplest to understand,
  183. is Sequential Consistency.  According to this model, systems behave as
  184. if each CPU executed its instructions in order but with unspecified
  185. timing.  In other words, the instructions from the various CPUs get
  186. interleaved in a nondeterministic way, always according to some single
  187. global order that agrees with the order of the instructions in the
  188. program source for each CPU.  The model says that the value obtained
  189. by each load is simply the value written by the most recently executed
  190. store to the same memory location, from any CPU.
  192. For the MP example code shown above, Sequential Consistency predicts
  193. that the undesired result r1 = 1, r2 = 0 cannot occur.  The reasoning
  194. goes like this:
  196.         Since r1 = 1, P0 must store 1 to flag before P1 loads 1 from
  197.         it, as loads can obtain values only from earlier stores.
  199.         P1 loads from flag before loading from buf, since CPUs execute
  200.         their instructions in order.
  202.         P1 must load 0 from buf before P0 stores 1 to it; otherwise r2
  203.         would be 1 since a load obtains its value from the most recent
  204.         store to the same address.
  206.         P0 stores 1 to buf before storing 1 to flag, since it executes
  207.         its instructions in order.
  209.         Since an instruction (in this case, P0's store to flag) cannot
  210.         execute before itself, the specified outcome is impossible.
  212. However, real computer hardware almost never follows the Sequential
  213. Consistency memory model; doing so would rule out too many valuable
  214. performance optimizations.  On ARM and PowerPC architectures, for
  215. instance, the MP example code really does sometimes yield r1 = 1 and
  216. r2 = 0.
  218. x86 and SPARC follow yet a different memory model: TSO (Total Store
  219. Ordering).  This model predicts that the undesired outcome for the MP
  220. pattern cannot occur, but in other respects it differs from Sequential
  221. Consistency.  One example is the Store Buffer (SB) pattern, in which
  222. each CPU stores to its own shared location and then loads from the
  223. other CPU's location:
  225.         int x = 0, y = 0;
  227.         P0()
  228.         {
  229.                 int r0;
  231.                 WRITE_ONCE(x, 1);
  232.                 r0 = READ_ONCE(y);
  233.         }
  235.         P1()
  236.         {
  237.                 int r1;
  239.                 WRITE_ONCE(y, 1);
  240.                 r1 = READ_ONCE(x);
  241.         }
  243. Sequential Consistency predicts that the outcome r0 = 0, r1 = 0 is
  244. impossible.  (Exercise: Figure out the reasoning.)  But TSO allows
  245. this outcome to occur, and in fact it does sometimes occur on x86 and
  246. SPARC systems.
  248. The LKMM was inspired by the memory models followed by PowerPC, ARM,
  249. x86, Alpha, and other architectures.  However, it is different in
  250. detail from each of them.
  254. -------------------
  256. Memory models are all about ordering.  Often this is temporal ordering
  257. (i.e., the order in which certain events occur) but it doesn't have to
  258. be; consider for example the order of instructions in a program's
  259. source code.  We saw above that Sequential Consistency makes an
  260. important assumption that CPUs execute instructions in the same order
  261. as those instructions occur in the code, and there are many other
  262. instances of ordering playing central roles in memory models.
  264. The counterpart to ordering is a cycle.  Ordering rules out cycles:
  265. It's not possible to have X ordered before Y, Y ordered before Z, and
  266. Z ordered before X, because this would mean that X is ordered before
  267. itself.  The analysis of the MP example under Sequential Consistency
  268. involved just such an impossible cycle:
  270.         W: P0 stores 1 to flag   executes before
  271.         X: P1 loads 1 from flag  executes before
  272.         Y: P1 loads 0 from buf   executes before
  273.         Z: P0 stores 1 to buf    executes before
  274.         W: P0 stores 1 to flag.
  276. In short, if a memory model requires certain accesses to be ordered,
  277. and a certain outcome for the loads in a piece of code can happen only
  278. if those accesses would form a cycle, then the memory model predicts
  279. that outcome cannot occur.
  281. The LKMM is defined largely in terms of cycles, as we will see.
  284. EVENTS
  285. ------
  287. The LKMM does not work directly with the C statements that make up
  288. kernel source code.  Instead it considers the effects of those
  289. statements in a more abstract form, namely, events.  The model
  290. includes three types of events:
  292.         Read events correspond to loads from shared memory, such as
  293.         calls to READ_ONCE(), smp_load_acquire(), or
  294.         rcu_dereference().
  296.         Write events correspond to stores to shared memory, such as
  297.         calls to WRITE_ONCE(), smp_store_release(), or atomic_set().
  299.         Fence events correspond to memory barriers (also known as
  300.         fences), such as calls to smp_rmb() or rcu_read_lock().
  302. These categories are not exclusive; a read or write event can also be
  303. a fence.  This happens with functions like smp_load_acquire() or
  304. spin_lock().  However, no single event can be both a read and a write.
  305. Atomic read-modify-write accesses, such as atomic_inc() or xchg(),
  306. correspond to a pair of events: a read followed by a write.  (The
  307. write event is omitted for executions where it doesn't occur, such as
  308. a cmpxchg() where the comparison fails.)
  310. Other parts of the code, those which do not involve interaction with
  311. shared memory, do not give rise to events.  Thus, arithmetic and
  312. logical computations, control-flow instructions, or accesses to
  313. private memory or CPU registers are not of central interest to the
  314. memory model.  They only affect the model's predictions indirectly.
  315. For example, an arithmetic computation might determine the value that
  316. gets stored to a shared memory location (or in the case of an array
  317. index, the address where the value gets stored), but the memory model
  318. is concerned only with the store itself -- its value and its address
  319. -- not the computation leading up to it.
  321. Events in the LKMM can be linked by various relations, which we will
  322. describe in the following sections.  The memory model requires certain
  323. of these relations to be orderings, that is, it requires them not to
  324. have any cycles.
  328. -----------------------------------------
  330. The most important relation between events is program order (po).  You
  331. can think of it as the order in which statements occur in the source
  332. code after branches are taken into account and loops have been
  333. unrolled.  A better description might be the order in which
  334. instructions are presented to a CPU's execution unit.  Thus, we say
  335. that X is po-before Y (written as "X ->po Y" in formulas) if X occurs
  336. before Y in the instruction stream.
  338. This is inherently a single-CPU relation; two instructions executing
  339. on different CPUs are never linked by po.  Also, it is by definition
  340. an ordering so it cannot have any cycles.
  342. po-loc is a sub-relation of po.  It links two memory accesses when the
  343. first comes before the second in program order and they access the
  344. same memory location (the "-loc" suffix).
  346. Although this may seem straightforward, there is one subtle aspect to
  347. program order we need to explain.  The LKMM was inspired by low-level
  348. architectural memory models which describe the behavior of machine
  349. code, and it retains their outlook to a considerable extent.  The
  350. read, write, and fence events used by the model are close in spirit to
  351. individual machine instructions.  Nevertheless, the LKMM describes
  352. kernel code written in C, and the mapping from C to machine code can
  353. be extremely complex.
  355. Optimizing compilers have great freedom in the way they translate
  356. source code to object code.  They are allowed to apply transformations
  357. that add memory accesses, eliminate accesses, combine them, split them
  358. into pieces, or move them around.  The use of READ_ONCE(), WRITE_ONCE(),
  359. or one of the other atomic or synchronization primitives prevents a
  360. large number of compiler optimizations.  In particular, it is guaranteed
  361. that the compiler will not remove such accesses from the generated code
  362. (unless it can prove the accesses will never be executed), it will not
  363. change the order in which they occur in the code (within limits imposed
  364. by the C standard), and it will not introduce extraneous accesses.
  366. The MP and SB examples above used READ_ONCE() and WRITE_ONCE() rather
  367. than ordinary memory accesses.  Thanks to this usage, we can be certain
  368. that in the MP example, the compiler won't reorder P0's write event to
  369. buf and P0's write event to flag, and similarly for the other shared
  370. memory accesses in the examples.
  372. Since private variables are not shared between CPUs, they can be
  373. accessed normally without READ_ONCE() or WRITE_ONCE().  In fact, they
  374. need not even be stored in normal memory at all -- in principle a
  375. private variable could be stored in a CPU register (hence the convention
  376. that these variables have names starting with the letter 'r').
  379. A WARNING
  380. ---------
  382. The protections provided by READ_ONCE(), WRITE_ONCE(), and others are
  383. not perfect; and under some circumstances it is possible for the
  384. compiler to undermine the memory model.  Here is an example.  Suppose
  385. both branches of an "if" statement store the same value to the same
  386. location:
  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.         }
  397. For this code, the LKMM predicts that the load from x will always be
  398. executed before either of the stores to y.  However, a compiler could
  399. lift the stores out of the conditional, transforming the code into
  400. something resembling:
  402.         r1 = READ_ONCE(x);
  403.         WRITE_ONCE(y, 2);
  404.         if (r1) {
  405.                 ...  /* do something */
  406.         } else {
  407.                 ...  /* do something else */
  408.         }
  410. Given this version of the code, the LKMM would predict that the load
  411. from x could be executed after the store to y.  Thus, the memory
  412. model's original prediction could be invalidated by the compiler.
  414. Another issue arises from the fact that in C, arguments to many
  415. operators and function calls can be evaluated in any order.  For
  416. example:
  418.         r1 = f(5) + g(6);
  420. The object code might call f(5) either before or after g(6); the
  421. memory model cannot assume there is a fixed program order relation
  422. between them.  (In fact, if the function calls are inlined then the
  423. compiler might even interleave their object code.)
  426. DEPENDENCY RELATIONS: data, addr, and ctrl
  427. ------------------------------------------
  429. We say that two events are linked by a dependency relation when the
  430. execution of the second event depends in some way on a value obtained
  431. from memory by the first.  The first event must be a read, and the
  432. value it obtains must somehow affect what the second event does.
  433. There are three kinds of dependencies: data, address (addr), and
  434. control (ctrl).
  436. A read and a write event are linked by a data dependency if the value
  437. obtained by the read affects the value stored by the write.  As a very
  438. simple example:
  440.         int x, y;
  442.         r1 = READ_ONCE(x);
  443.         WRITE_ONCE(y, r1 + 5);
  445. The value stored by the WRITE_ONCE obviously depends on the value
  446. loaded by the READ_ONCE.  Such dependencies can wind through
  447. arbitrarily complicated computations, and a write can depend on the
  448. values of multiple reads.
  450. A read event and another memory access event are linked by an address
  451. dependency if the value obtained by the read affects the location
  452. accessed by the other event.  The second event can be either a read or
  453. a write.  Here's another simple example:
  455.         int a[20];
  456.         int i;
  458.         r1 = READ_ONCE(i);
  459.         r2 = READ_ONCE(a[r1]);
  461. Here the location accessed by the second READ_ONCE() depends on the
  462. index value loaded by the first.  Pointer indirection also gives rise
  463. to address dependencies, since the address of a location accessed
  464. through a pointer will depend on the value read earlier from that
  465. pointer.
  467. Finally, a read event and another memory access event are linked by a
  468. control dependency if the value obtained by the read affects whether
  469. the second event is executed at all.  Simple example:
  471.         int x, y;
  473.         r1 = READ_ONCE(x);
  474.         if (r1)
  475.                 WRITE_ONCE(y, 1984);
  477. Execution of the WRITE_ONCE() is controlled by a conditional expression
  478. which depends on the value obtained by the READ_ONCE(); hence there is
  479. a control dependency from the load to the store.
  481. It should be pretty obvious that events can only depend on reads that
  482. come earlier in program order.  Symbolically, if we have R ->data X,
  483. R ->addr X, or R ->ctrl X (where R is a read event), then we must also
  484. have R ->po X.  It wouldn't make sense for a computation to depend
  485. somehow on a value that doesn't get loaded from shared memory until
  486. later in the code!
  489. THE READS-FROM RELATION: rf, rfi, and rfe
  490. -----------------------------------------
  492. The reads-from relation (rf) links a write event to a read event when
  493. the value loaded by the read is the value that was stored by the
  494. write.  In colloquial terms, the load "reads from" the store.  We
  495. write W ->rf R to indicate that the load R reads from the store W.  We
  496. further distinguish the cases where the load and the store occur on
  497. the same CPU (internal reads-from, or rfi) and where they occur on
  498. different CPUs (external reads-from, or rfe).
  500. For our purposes, a memory location's initial value is treated as
  501. though it had been written there by an imaginary initial store that
  502. executes on a separate CPU before the main program runs.
  504. Usage of the rf relation implicitly assumes that loads will always
  505. read from a single store.  It doesn't apply properly in the presence
  506. of load-tearing, where a load obtains some of its bits from one store
  507. and some of them from another store.  Fortunately, use of READ_ONCE()
  508. and WRITE_ONCE() will prevent load-tearing; it's not possible to have:
  510.         int x = 0;
  512.         P0()
  513.         {
  514.                 WRITE_ONCE(x, 0x1234);
  515.         }
  517.         P1()
  518.         {
  519.                 int r1;
  521.                 r1 = READ_ONCE(x);
  522.         }
  524. and end up with r1 = 0x1200 (partly from x's initial value and partly
  525. from the value stored by P0).
  527. On the other hand, load-tearing is unavoidable when mixed-size
  528. accesses are used.  Consider this example:
  530.         union {
  531.                 u32     w;
  532.                 u16     h[2];
  533.         } x;
  535.         P0()
  536.         {
  537.                 WRITE_ONCE(x.h[0], 0x1234);
  538.                 WRITE_ONCE(x.h[1], 0x5678);
  539.         }
  541.         P1()
  542.         {
  543.                 int r1;
  545.                 r1 = READ_ONCE(x.w);
  546.         }
  548. If r1 = 0x56781234 (little-endian!) at the end, then P1 must have read
  549. from both of P0's stores.  It is possible to handle mixed-size and
  550. unaligned accesses in a memory model, but the LKMM currently does not
  551. attempt to do so.  It requires all accesses to be properly aligned and
  552. of the location's actual size.
  556. ------------------------------------------------------------------
  558. Cache coherence is a general principle requiring that in a
  559. multi-processor system, the CPUs must share a consistent view of the
  560. memory contents.  Specifically, it requires that for each location in
  561. shared memory, the stores to that location must form a single global
  562. ordering which all the CPUs agree on (the coherence order), and this
  563. ordering must be consistent with the program order for accesses to
  564. that location.
  566. To put it another way, for any variable x, the coherence order (co) of
  567. the stores to x is simply the order in which the stores overwrite one
  568. another.  The imaginary store which establishes x's initial value
  569. comes first in the coherence order; the store which directly
  570. overwrites the initial value comes second; the store which overwrites
  571. that value comes third, and so on.
  573. You can think of the coherence order as being the order in which the
  574. stores reach x's location in memory (or if you prefer a more
  575. hardware-centric view, the order in which the stores get written to
  576. x's cache line).  We write W ->co W' if W comes before W' in the
  577. coherence order, that is, if the value stored by W gets overwritten,
  578. directly or indirectly, by the value stored by W'.
  580. Coherence order is required to be consistent with program order.  This
  581. requirement takes the form of four coherency rules:
  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'.
  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.
  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.
  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.
  600. This is sometimes referred to as sequential consistency per variable,
  601. because it means that the accesses to any single memory location obey
  602. the rules of the Sequential Consistency memory model.  (According to
  603. Wikipedia, sequential consistency per variable and cache coherence
  604. mean the same thing except that cache coherence includes an extra
  605. requirement that every store eventually becomes visible to every CPU.)
  607. Any reasonable memory model will include cache coherence.  Indeed, our
  608. expectation of cache coherence is so deeply ingrained that violations
  609. of its requirements look more like hardware bugs than programming
  610. errors:
  612.         int x;
  614.         P0()
  615.         {
  616.                 WRITE_ONCE(x, 17);
  617.                 WRITE_ONCE(x, 23);
  618.         }
  620. If the final value stored in x after this code ran was 17, you would
  621. think your computer was broken.  It would be a violation of the
  622. write-write coherence rule: Since the store of 23 comes later in
  623. program order, it must also come later in x's coherence order and
  624. thus must overwrite the store of 17.
  626.         int x = 0;
  628.         P0()
  629.         {
  630.                 int r1;
  632.                 r1 = READ_ONCE(x);
  633.                 WRITE_ONCE(x, 666);
  634.         }
  636. If r1 = 666 at the end, this would violate the read-write coherence
  637. rule: The READ_ONCE() load comes before the WRITE_ONCE() store in
  638. program order, so it must not read from that store but rather from one
  639. coming earlier in the coherence order (in this case, x's initial
  640. value).
  642.         int x = 0;
  644.         P0()
  645.         {
  646.                 WRITE_ONCE(x, 5);
  647.         }
  649.         P1()
  650.         {
  651.                 int r1, r2;
  653.                 r1 = READ_ONCE(x);
  654.                 r2 = READ_ONCE(x);
  655.         }
  657. If r1 = 5 (reading from P0's store) and r2 = 0 (reading from the
  658. imaginary store which establishes x's initial value) at the end, this
  659. would violate the read-read coherence rule: The r1 load comes before
  660. the r2 load in program order, so it must not read from a store that
  661. comes later in the coherence order.
  663. (As a minor curiosity, if this code had used normal loads instead of
  664. READ_ONCE() in P1, on Itanium it sometimes could end up with r1 = 5
  665. and r2 = 0!  This results from parallel execution of the operations
  666. encoded in Itanium's Very-Long-Instruction-Word format, and it is yet
  667. another motivation for using READ_ONCE() when accessing shared memory
  668. locations.)
  670. Just like the po relation, co is inherently an ordering -- it is not
  671. possible for a store to directly or indirectly overwrite itself!  And
  672. just like with the rf relation, we distinguish between stores that
  673. occur on the same CPU (internal coherence order, or coi) and stores
  674. that occur on different CPUs (external coherence order, or coe).
  676. On the other hand, stores to different memory locations are never
  677. related by co, just as instructions on different CPUs are never
  678. related by po.  Coherence order is strictly per-location, or if you
  679. prefer, each location has its own independent coherence order.
  682. THE FROM-READS RELATION: fr, fri, and fre
  683. -----------------------------------------
  685. The from-reads relation (fr) can be a little difficult for people to
  686. grok.  It describes the situation where a load reads a value that gets
  687. overwritten by a store.  In other words, we have R ->fr W when the
  688. value that R reads is overwritten (directly or indirectly) by W, or
  689. equivalently, when R reads from a store which comes earlier than W in
  690. the coherence order.
  692. For example:
  694.         int x = 0;
  696.         P0()
  697.         {
  698.                 int r1;
  700.                 r1 = READ_ONCE(x);
  701.                 WRITE_ONCE(x, 2);
  702.         }
  704. The value loaded from x will be 0 (assuming cache coherence!), and it
  705. gets overwritten by the value 2.  Thus there is an fr link from the
  706. READ_ONCE() to the WRITE_ONCE().  If the code contained any later
  707. stores to x, there would also be fr links from the READ_ONCE() to
  708. them.
  710. As with rf, rfi, and rfe, we subdivide the fr relation into fri (when
  711. the load and the store are on the same CPU) and fre (when they are on
  712. different CPUs).
  714. Note that the fr relation is determined entirely by the rf and co
  715. relations; it is not independent.  Given a read event R and a write
  716. event W for the same location, we will have R ->fr W if and only if
  717. the write which R reads from is co-before W.  In symbols,
  719.         (R ->fr W) := (there exists W' with W' ->rf R and W' ->co W).
  723. --------------------
  725. The LKMM is based on various operational memory models, meaning that
  726. the models arise from an abstract view of how a computer system
  727. operates.  Here are the main ideas, as incorporated into the LKMM.
  729. The system as a whole is divided into the CPUs and a memory subsystem.
  730. The CPUs are responsible for executing instructions (not necessarily
  731. in program order), and they communicate with the memory subsystem.
  732. For the most part, executing an instruction requires a CPU to perform
  733. only internal operations.  However, loads, stores, and fences involve
  734. more.
  736. When CPU C executes a store instruction, it tells the memory subsystem
  737. to store a certain value at a certain location.  The memory subsystem
  738. propagates the store to all the other CPUs as well as to RAM.  (As a
  739. special case, we say that the store propagates to its own CPU at the
  740. time it is executed.)  The memory subsystem also determines where the
  741. store falls in the location's coherence order.  In particular, it must
  742. arrange for the store to be co-later than (i.e., to overwrite) any
  743. other store to the same location which has already propagated to CPU C.
  745. When a CPU executes a load instruction R, it first checks to see
  746. whether there are any as-yet unexecuted store instructions, for the
  747. same location, that come before R in program order.  If there are, it
  748. uses the value of the po-latest such store as the value obtained by R,
  749. and we say that the store's value is forwarded to R.  Otherwise, the
  750. CPU asks the memory subsystem for the value to load and we say that R
  751. is satisfied from memory.  The memory subsystem hands back the value
  752. of the co-latest store to the location in question which has already
  753. propagated to that CPU.
  755. (In fact, the picture needs to be a little more complicated than this.
  756. CPUs have local caches, and propagating a store to a CPU really means
  757. propagating it to the CPU's local cache.  A local cache can take some
  758. time to process the stores that it receives, and a store can't be used
  759. to satisfy one of the CPU's loads until it has been processed.  On
  760. most architectures, the local caches process stores in
  761. First-In-First-Out order, and consequently the processing delay
  762. doesn't matter for the memory model.  But on Alpha, the local caches
  763. have a partitioned design that results in non-FIFO behavior.  We will
  764. discuss this in more detail later.)
  766. Note that load instructions may be executed speculatively and may be
  767. restarted under certain circumstances.  The memory model ignores these
  768. premature executions; we simply say that the load executes at the
  769. final time it is forwarded or satisfied.
  771. Executing a fence (or memory barrier) instruction doesn't require a
  772. CPU to do anything special other than informing the memory subsystem
  773. about the fence.  However, fences do constrain the way CPUs and the
  774. memory subsystem handle other instructions, in two respects.
  776. First, a fence forces the CPU to execute various instructions in
  777. program order.  Exactly which instructions are ordered depends on the
  778. type of fence:
  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;
  784.         smp_rmb() forces the CPU to execute all po-earlier loads
  785.         before any po-later loads;
  787.         smp_wmb() forces the CPU to execute all po-earlier stores
  788.         before any po-later stores;
  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;
  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()).
  800. Second, some types of fence affect the way the memory subsystem
  801. propagates stores.  When a fence instruction is executed on CPU C:
  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.
  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.
  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.
  816. The propagation ordering enforced by release fences and strong fences
  817. affects stores from other CPUs that propagate to CPU C before the
  818. fence is executed, as well as stores that are executed on C before the
  819. fence.  We describe this property by saying that release fences and
  820. strong fences are A-cumulative.  By contrast, smp_wmb() fences are not
  821. A-cumulative; they only affect the propagation of stores that are
  822. executed on C before the fence (i.e., those which precede the fence in
  823. program order).
  825. rcu_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
  826. other properties which we discuss later.
  830. ---------------------------------------
  832. The fences which affect propagation order (i.e., strong, release, and
  833. smp_wmb() fences) are collectively referred to as cumul-fences, even
  834. though smp_wmb() isn't A-cumulative.  The cumul-fence relation is
  835. defined to link memory access events E and F whenever:
  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
  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
  843.         A strong fence event occurs between some X and F in program
  844.         order, where either X = E or else E ->rf X.
  846. The operational model requires that whenever W and W' are both stores
  847. and W ->cumul-fence W', then W must propagate to any given CPU
  848. before W' does.  However, for different CPUs C and C', it does not
  849. require W to propagate to C before W' propagates to C'.
  853. -------------------------------------------------
  855. The LKMM is derived from the restrictions imposed by the design
  856. outlined above.  These restrictions involve the necessity of
  857. maintaining cache coherence and the fact that a CPU can't operate on a
  858. value before it knows what that value is, among other things.
  860. The formal version of the LKMM is defined by six requirements, or
  861. axioms:
  863.         Sequential consistency per variable: This requires that the
  864.         system obey the four coherency rules.
  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.
  870.         Happens-before: This requires that certain instructions are
  871.         executed in a specific order.
  873.         Propagation: This requires that certain stores propagate to
  874.         CPUs and to RAM in a specific order.
  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.
  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.
  884. The first and second are quite common; they can be found in many
  885. memory 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.
  889. Each of these axioms is discussed below.
  893. -----------------------------------
  895. According to the principle of cache coherence, the stores to any fixed
  896. shared location in memory form a global ordering.  We can imagine
  897. inserting the loads from that location into this ordering, by placing
  898. each load between the store that it reads from and the following
  899. store.  This leaves the relative positions of loads that read from the
  900. same store unspecified; let's say they are inserted in program order,
  901. first for CPU 0, then CPU 1, etc.
  903. You can check that the four coherency rules imply that the rf, co, fr,
  904. and po-loc relations agree with this global ordering; in other words,
  905. whenever we have X ->rf Y or X ->co Y or X ->fr Y or X ->po-loc Y, the
  906. X event comes before the Y event in the global ordering.  The LKMM's
  907. "coherence" axiom expresses this by requiring the union of these
  908. relations not to have any cycles.  This means it must not be possible
  909. to find events
  911.         X0 -> X1 -> X2 -> ... -> Xn -> X0,
  913. where each of the links is either rf, co, fr, or po-loc.  This has to
  914. hold if the accesses to the fixed memory location can be ordered as
  915. cache coherence demands.
  917. Although it is not obvious, it can be shown that the converse is also
  918. true: This LKMM axiom implies that the four coherency rules are
  919. obeyed.
  922. ATOMIC UPDATES: rmw
  923. -------------------
  925. What does it mean to say that a read-modify-write (rmw) update, such
  926. as atomic_inc(&x), is atomic?  It means that the memory location (x in
  927. this case) does not get altered between the read and the write events
  928. making up the atomic operation.  In particular, if two CPUs perform
  929. atomic_inc(&x) concurrently, it must be guaranteed that the final
  930. value of x will be the initial value plus two.  We should never have
  931. the following sequence of events:
  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;
  938. where the final value of x is wrong (14 rather than 15).
  940. In this example, CPU 0's increment effectively gets lost because it
  941. occurs in between CPU 1's load and store.  To put it another way, the
  942. problem is that the position of CPU 0's store in x's coherence order
  943. is between the store that CPU 1 reads from and the store that CPU 1
  944. performs.
  946. The same analysis applies to all atomic update operations.  Therefore,
  947. to enforce atomicity the LKMM requires that atomic updates follow this
  948. rule: Whenever R and W are the read and write events composing an
  949. atomic read-modify-write and W' is the write event which R reads from,
  950. there must not be any stores coming between W' and W in the coherence
  951. order.  Equivalently,
  953.         (R ->rmw W) implies (there is no X with R ->fr X and X ->co W),
  955. where the rmw relation links the read and write events making up each
  956. atomic update.  This is what the LKMM's "atomic" axiom says.
  960. -----------------------------------------
  962. There are many situations where a CPU is obliged to execute two
  963. instructions in program order.  We amalgamate them into the ppo (for
  964. "preserved program order") relation, which links the po-earlier
  965. instruction to the po-later instruction and is thus a sub-relation of
  966. po.
  968. The operational model already includes a description of one such
  969. situation: Fences are a source of ppo links.  Suppose X and Y are
  970. memory accesses with X ->po Y; then the CPU must execute X before Y if
  971. any of the following hold:
  973.         A strong (smp_mb() or synchronize_rcu()) fence occurs between
  974.         X and Y;
  976.         X and Y are both stores and an smp_wmb() fence occurs between
  977.         them;
  979.         X and Y are both loads and an smp_rmb() fence occurs between
  980.         them;
  982.         X is also an acquire fence, such as smp_load_acquire();
  984.         Y is also a release fence, such as smp_store_release().
  986. Another possibility, not mentioned earlier but discussed in the next
  987. section, is:
  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.
  993. Dependencies can also cause instructions to be executed in program
  994. order.  This is uncontroversial when the second instruction is a
  995. store; either a data, address, or control dependency from a load R to
  996. a store W will force the CPU to execute R before W.  This is very
  997. simply because the CPU cannot tell the memory subsystem about W's
  998. store before it knows what value should be stored (in the case of a
  999. data dependency), what location it should be stored into (in the case
  1000. of an address dependency), or whether the store should actually take
  1001. place (in the case of a control dependency).
  1003. Dependencies to load instructions are more problematic.  To begin with,
  1004. there is no such thing as a data dependency to a load.  Next, a CPU
  1005. has no reason to respect a control dependency to a load, because it
  1006. can always satisfy the second load speculatively before the first, and
  1007. then ignore the result if it turns out that the second load shouldn't
  1008. be executed after all.  And lastly, the real difficulties begin when
  1009. we consider address dependencies to loads.
  1011. To be fair about it, all Linux-supported architectures do execute
  1012. loads in program order if there is an address dependency between them.
  1013. After all, a CPU cannot ask the memory subsystem to load a value from
  1014. a particular location before it knows what that location is.  However,
  1015. the split-cache design used by Alpha can cause it to behave in a way
  1016. that looks as if the loads were executed out of order (see the next
  1017. section for more details).  The kernel includes a workaround for this
  1018. problem when the loads come from READ_ONCE(), and therefore the LKMM
  1019. includes address dependencies to loads in the ppo relation.
  1021. On the other hand, dependencies can indirectly affect the ordering of
  1022. two loads.  This happens when there is a dependency from a load to a
  1023. store and a second, po-later load reads from that store:
  1025.         R ->dep W ->rfi R',
  1027. where the dep link can be either an address or a data dependency.  In
  1028. this situation we know it is possible for the CPU to execute R' before
  1029. W, because it can forward the value that W will store to R'.  But it
  1030. cannot execute R' before R, because it cannot forward the value before
  1031. it knows what that value is, or that W and R' do access the same
  1032. location.  However, if there is merely a control dependency between R
  1033. and W then the CPU can speculatively forward W to R' before executing
  1034. R; if the speculation turns out to be wrong then the CPU merely has to
  1035. restart or abandon R'.
  1037. (In theory, a CPU might forward a store to a load when it runs across
  1038. an address dependency like this:
  1040.         r1 = READ_ONCE(ptr);
  1041.         WRITE_ONCE(*r1, 17);
  1042.         r2 = READ_ONCE(*r1);
  1044. because it could tell that the store and the second load access the
  1045. same location even before it knows what the location's address is.
  1046. However, none of the architectures supported by the Linux kernel do
  1047. this.)
  1049. Two memory accesses of the same location must always be executed in
  1050. program order if the second access is a store.  Thus, if we have
  1052.         R ->po-loc W
  1054. (the po-loc link says that R comes before W in program order and they
  1055. access the same location), the CPU is obliged to execute W after R.
  1056. If it executed W first then the memory subsystem would respond to R's
  1057. read request with the value stored by W (or an even later store), in
  1058. violation of the read-write coherence rule.  Similarly, if we had
  1060.         W ->po-loc W'
  1062. and the CPU executed W' before W, then the memory subsystem would put
  1063. W' before W in the coherence order.  It would effectively cause W to
  1064. overwrite W', in violation of the write-write coherence rule.
  1065. (Interestingly, an early ARMv8 memory model, now obsolete, proposed
  1066. allowing out-of-order writes like this to occur.  The model avoided
  1067. violating the write-write coherence rule by requiring the CPU not to
  1068. send the W write to the memory subsystem at all!)
  1072. ------------------------
  1074. As mentioned above, the Alpha architecture is unique in that it does
  1075. not appear to respect address dependencies to loads.  This means that
  1076. code such as the following:
  1078.         int x = 0;
  1079.         int y = -1;
  1080.         int *ptr = &y;
  1082.         P0()
  1083.         {
  1084.                 WRITE_ONCE(x, 1);
  1085.                 smp_wmb();
  1086.                 WRITE_ONCE(ptr, &x);
  1087.         }
  1089.         P1()
  1090.         {
  1091.                 int *r1;
  1092.                 int r2;
  1094.                 r1 = ptr;
  1095.                 r2 = READ_ONCE(*r1);
  1096.         }
  1098. can malfunction on Alpha systems (notice that P1 uses an ordinary load
  1099. to read ptr instead of READ_ONCE()).  It is quite possible that r1 = &x
  1100. and r2 = 0 at the end, in spite of the address dependency.
  1102. At first glance this doesn't seem to make sense.  We know that the
  1103. smp_wmb() forces P0's store to x to propagate to P1 before the store
  1104. to ptr does.  And since P1 can't execute its second load
  1105. until it knows what location to load from, i.e., after executing its
  1106. first load, the value x = 1 must have propagated to P1 before the
  1107. second load executed.  So why doesn't r2 end up equal to 1?
  1109. The answer lies in the Alpha's split local caches.  Although the two
  1110. stores do reach P1's local cache in the proper order, it can happen
  1111. that the first store is processed by a busy part of the cache while
  1112. the second store is processed by an idle part.  As a result, the x = 1
  1113. value may not become available for P1's CPU to read until after the
  1114. ptr = &x value does, leading to the undesirable result above.  The
  1115. final effect is that even though the two loads really are executed in
  1116. program order, it appears that they aren't.
  1118. This could not have happened if the local cache had processed the
  1119. incoming stores in FIFO order.  By contrast, other architectures
  1120. maintain at least the appearance of FIFO order.
  1122. In practice, this difficulty is solved by inserting a special fence
  1123. between P1's two loads when the kernel is compiled for the Alpha
  1124. architecture.  In fact, as of version 4.15, the kernel automatically
  1125. adds this fence after every READ_ONCE() and atomic load on Alpha.  The
  1126. effect of the fence is to cause the CPU not to execute any po-later
  1127. instructions until after the local cache has finished processing all
  1128. the stores it has already received.  Thus, if the code was changed to:
  1130.         P1()
  1131.         {
  1132.                 int *r1;
  1133.                 int r2;
  1135.                 r1 = READ_ONCE(ptr);
  1136.                 r2 = READ_ONCE(*r1);
  1137.         }
  1139. then we would never get r1 = &x and r2 = 0.  By the time P1 executed
  1140. its second load, the x = 1 store would already be fully processed by
  1141. the local cache and available for satisfying the read request.  Thus
  1142. we have yet another reason why shared data should always be read with
  1143. READ_ONCE() or another synchronization primitive rather than accessed
  1144. directly.
  1146. The LKMM requires that smp_rmb(), acquire fences, and strong fences
  1147. share this property: They do not allow the CPU to execute any po-later
  1148. instructions (or po-later loads in the case of smp_rmb()) until all
  1149. outstanding stores have been processed by the local cache.  In the
  1150. case of a strong fence, the CPU first has to wait for all of its
  1151. po-earlier stores to propagate to every other CPU in the system; then
  1152. it has to wait for the local cache to process all the stores received
  1153. as of that time -- not just the stores received when the strong fence
  1154. began.
  1156. And of course, none of this matters for any architecture other than
  1157. Alpha.
  1161. -------------------------------
  1163. The happens-before relation (hb) links memory accesses that have to
  1164. execute in a certain order.  hb includes the ppo relation and two
  1165. others, one of which is rfe.
  1167. W ->rfe R implies that W and R are on different CPUs.  It also means
  1168. that W's store must have propagated to R's CPU before R executed;
  1169. otherwise R could not have read the value stored by W.  Therefore W
  1170. must have executed before R, and so we have W ->hb R.
  1172. The equivalent fact need not hold if W ->rfi R (i.e., W and R are on
  1173. the same CPU).  As we have already seen, the operational model allows
  1174. W's value to be forwarded to R in such cases, meaning that R may well
  1175. execute before W does.
  1177. It's important to understand that neither coe nor fre is included in
  1178. hb, despite their similarities to rfe.  For example, suppose we have
  1179. W ->coe W'.  This means that W and W' are stores to the same location,
  1180. they execute on different CPUs, and W comes before W' in the coherence
  1181. order (i.e., W' overwrites W).  Nevertheless, it is possible for W' to
  1182. execute before W, because the decision as to which store overwrites
  1183. the other is made later by the memory subsystem.  When the stores are
  1184. nearly simultaneous, either one can come out on top.  Similarly,
  1185. R ->fre W means that W overwrites the value which R reads, but it
  1186. doesn't mean that W has to execute after R.  All that's necessary is
  1187. for the memory subsystem not to propagate W to R's CPU until after R
  1188. has executed, which is possible if W executes shortly before R.
  1190. The third relation included in hb is like ppo, in that it only links
  1191. events that are on the same CPU.  However it is more difficult to
  1192. explain, because it arises only indirectly from the requirement of
  1193. cache coherence.  The relation is called prop, and it links two events
  1194. on CPU C in situations where a store from some other CPU comes after
  1195. the first event in the coherence order and propagates to C before the
  1196. second event executes.
  1198. This is best explained with some examples.  The simplest case looks
  1199. like this:
  1201.         int x;
  1203.         P0()
  1204.         {
  1205.                 int r1;
  1207.                 WRITE_ONCE(x, 1);
  1208.                 r1 = READ_ONCE(x);
  1209.         }
  1211.         P1()
  1212.         {
  1213.                 WRITE_ONCE(x, 8);
  1214.         }
  1216. If r1 = 8 at the end then P0's accesses must have executed in program
  1217. order.  We can deduce this from the operational model; if P0's load
  1218. had executed before its store then the value of the store would have
  1219. been forwarded to the load, so r1 would have ended up equal to 1, not
  1220. 8.  In this case there is a prop link from P0's write event to its read
  1221. event, because P1's store came after P0's store in x's coherence
  1222. order, and P1's store propagated to P0 before P0's load executed.
  1224. An equally simple case involves two loads of the same location that
  1225. read from different stores:
  1227.         int x = 0;
  1229.         P0()
  1230.         {
  1231.                 int r1, r2;
  1233.                 r1 = READ_ONCE(x);
  1234.                 r2 = READ_ONCE(x);
  1235.         }
  1237.         P1()
  1238.         {
  1239.                 WRITE_ONCE(x, 9);
  1240.         }
  1242. If r1 = 0 and r2 = 9 at the end then P0's accesses must have executed
  1243. in program order.  If the second load had executed before the first
  1244. then the x = 9 store must have been propagated to P0 before the first
  1245. load executed, and so r1 would have been 9 rather than 0.  In this
  1246. case there is a prop link from P0's first read event to its second,
  1247. because P1's store overwrote the value read by P0's first load, and
  1248. P1's store propagated to P0 before P0's second load executed.
  1250. Less trivial examples of prop all involve fences.  Unlike the simple
  1251. examples above, they can require that some instructions are executed
  1252. out of program order.  This next one should look familiar:
  1254.         int buf = 0, flag = 0;
  1256.         P0()
  1257.         {
  1258.                 WRITE_ONCE(buf, 1);
  1259.                 smp_wmb();
  1260.                 WRITE_ONCE(flag, 1);
  1261.         }
  1263.         P1()
  1264.         {
  1265.                 int r1;
  1266.                 int r2;
  1268.                 r1 = READ_ONCE(flag);
  1269.                 r2 = READ_ONCE(buf);
  1270.         }
  1272. This is the MP pattern again, with an smp_wmb() fence between the two
  1273. stores.  If r1 = 1 and r2 = 0 at the end then there is a prop link
  1274. from P1's second load to its first (backwards!).  The reason is
  1275. similar to the previous examples: The value P1 loads from buf gets
  1276. overwritten by P0's store to buf, the fence guarantees that the store
  1277. to buf will propagate to P1 before the store to flag does, and the
  1278. store to flag propagates to P1 before P1 reads flag.
  1280. The prop link says that in order to obtain the r1 = 1, r2 = 0 result,
  1281. P1 must execute its second load before the first.  Indeed, if the load
  1282. from flag were executed first, then the buf = 1 store would already
  1283. have propagated to P1 by the time P1's load from buf executed, so r2
  1284. would have been 1 at the end, not 0.  (The reasoning holds even for
  1285. Alpha, although the details are more complicated and we will not go
  1286. into them.)
  1288. But what if we put an smp_rmb() fence between P1's loads?  The fence
  1289. would force the two loads to be executed in program order, and it
  1290. would generate a cycle in the hb relation: The fence would create a ppo
  1291. link (hence an hb link) from the first load to the second, and the
  1292. prop relation would give an hb link from the second load to the first.
  1293. Since an instruction can't execute before itself, we are forced to
  1294. conclude that if an smp_rmb() fence is added, the r1 = 1, r2 = 0
  1295. outcome is impossible -- as it should be.
  1297. The formal definition of the prop relation involves a coe or fre link,
  1298. followed by an arbitrary number of cumul-fence links, ending with an
  1299. rfe link.  You can concoct more exotic examples, containing more than
  1300. one fence, although this quickly leads to diminishing returns in terms
  1301. of complexity.  For instance, here's an example containing a coe link
  1302. followed by two cumul-fences and an rfe link, utilizing the fact that
  1303. release fences are A-cumulative:
  1305.         int x, y, z;
  1307.         P0()
  1308.         {
  1309.                 int r0;
  1311.                 WRITE_ONCE(x, 1);
  1312.                 r0 = READ_ONCE(z);
  1313.         }
  1315.         P1()
  1316.         {
  1317.                 WRITE_ONCE(x, 2);
  1318.                 smp_wmb();
  1319.                 WRITE_ONCE(y, 1);
  1320.         }
  1322.         P2()
  1323.         {
  1324.                 int r2;
  1326.                 r2 = READ_ONCE(y);
  1327.                 smp_store_release(&z, 1);
  1328.         }
  1330. If x = 2, r0 = 1, and r2 = 1 after this code runs then there is a prop
  1331. link from P0's store to its load.  This is because P0's store gets
  1332. overwritten by P1's store since x = 2 at the end (a coe link), the
  1333. smp_wmb() ensures that P1's store to x propagates to P2 before the
  1334. store to y does (the first cumul-fence), the store to y propagates to P2
  1335. before P2's load and store execute, P2's smp_store_release()
  1336. guarantees that the stores to x and y both propagate to P0 before the
  1337. store to z does (the second cumul-fence), and P0's load executes after the
  1338. store to z has propagated to P0 (an rfe link).
  1340. In summary, the fact that the hb relation links memory access events
  1341. in the order they execute means that it must not have cycles.  This
  1342. requirement is the content of the LKMM's "happens-before" axiom.
  1344. The LKMM defines yet another relation connected to times of
  1345. instruction execution, but it is not included in hb.  It relies on the
  1346. particular properties of strong fences, which we cover in the next
  1347. section.
  1351. ----------------------------------
  1353. The propagates-before (pb) relation capitalizes on the special
  1354. features of strong fences.  It links two events E and F whenever some
  1355. store is coherence-later than E and propagates to every CPU and to RAM
  1356. before F executes.  The formal definition requires that E be linked to
  1357. F via a coe or fre link, an arbitrary number of cumul-fences, an
  1358. optional rfe link, a strong fence, and an arbitrary number of hb
  1359. links.  Let's see how this definition works out.
  1361. Consider first the case where E is a store (implying that the sequence
  1362. of links begins with coe).  Then there are events W, X, Y, and Z such
  1363. that:
  1365.         E ->coe W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F,
  1367. where the * suffix indicates an arbitrary number of links of the
  1368. specified type, and the ? suffix indicates the link is optional (Y may
  1369. be equal to X).  Because of the cumul-fence links, we know that W will
  1370. propagate to Y's CPU before X does, hence before Y executes and hence
  1371. before the strong fence executes.  Because this fence is strong, we
  1372. know that W will propagate to every CPU and to RAM before Z executes.
  1373. And because of the hb links, we know that Z will execute before F.
  1374. Thus W, which comes later than E in the coherence order, will
  1375. propagate to every CPU and to RAM before F executes.
  1377. The case where E is a load is exactly the same, except that the first
  1378. link in the sequence is fre instead of coe.
  1380. The existence of a pb link from E to F implies that E must execute
  1381. before F.  To see why, suppose that F executed first.  Then W would
  1382. have propagated to E's CPU before E executed.  If E was a store, the
  1383. memory subsystem would then be forced to make E come after W in the
  1384. coherence order, contradicting the fact that E ->coe W.  If E was a
  1385. load, the memory subsystem would then be forced to satisfy E's read
  1386. request with the value stored by W or an even later store,
  1387. contradicting the fact that E ->fre W.
  1389. A good example illustrating how pb works is the SB pattern with strong
  1390. fences:
  1392.         int x = 0, y = 0;
  1394.         P0()
  1395.         {
  1396.                 int r0;
  1398.                 WRITE_ONCE(x, 1);
  1399.                 smp_mb();
  1400.                 r0 = READ_ONCE(y);
  1401.         }
  1403.         P1()
  1404.         {
  1405.                 int r1;
  1407.                 WRITE_ONCE(y, 1);
  1408.                 smp_mb();
  1409.                 r1 = READ_ONCE(x);
  1410.         }
  1412. If r0 = 0 at the end then there is a pb link from P0's load to P1's
  1413. load: an fre link from P0's load to P1's store (which overwrites the
  1414. value read by P0), and a strong fence between P1's store and its load.
  1415. In this example, the sequences of cumul-fence and hb links are empty.
  1416. Note that this pb link is not included in hb as an instance of prop,
  1417. because it does not start and end on the same CPU.
  1419. Similarly, if r1 = 0 at the end then there is a pb link from P1's load
  1420. to P0's.  This means that if both r1 and r2 were 0 there would be a
  1421. cycle in pb, which is not possible since an instruction cannot execute
  1422. before itself.  Thus, adding smp_mb() fences to the SB pattern
  1423. prevents the r0 = 0, r1 = 0 outcome.
  1425. In summary, the fact that the pb relation links events in the order
  1426. they execute means that it cannot have cycles.  This requirement is
  1427. the content of the LKMM's "propagation" axiom.
  1430. RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb
  1431. ------------------------------------------------------------------------
  1433. RCU (Read-Copy-Update) is a powerful synchronization mechanism.  It
  1434. rests on two concepts: grace periods and read-side critical sections.
  1436. A grace period is the span of time occupied by a call to
  1437. synchronize_rcu().  A read-side critical section (or just critical
  1438. section, for short) is a region of code delimited by rcu_read_lock()
  1439. at the start and rcu_read_unlock() at the end.  Critical sections can
  1440. be nested, although we won't make use of this fact.
  1442. As far as memory models are concerned, RCU's main feature is its
  1443. Grace-Period Guarantee, which states that a critical section can never
  1444. span a full grace period.  In more detail, the Guarantee says:
  1446.         For any critical section C and any grace period G, at least
  1447.         one of the following statements must hold:
  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.
  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.
  1457. In particular, it is not possible for a critical section to both start
  1458. before and end after a grace period.
  1460. Here is a simple example of RCU in action:
  1462.         int x, y;
  1464.         P0()
  1465.         {
  1466.                 rcu_read_lock();
  1467.                 WRITE_ONCE(x, 1);
  1468.                 WRITE_ONCE(y, 1);
  1469.                 rcu_read_unlock();
  1470.         }
  1472.         P1()
  1473.         {
  1474.                 int r1, r2;
  1476.                 r1 = READ_ONCE(x);
  1477.                 synchronize_rcu();
  1478.                 r2 = READ_ONCE(y);
  1479.         }
  1481. The Grace Period Guarantee tells us that when this code runs, it will
  1482. never end with r1 = 1 and r2 = 0.  The reasoning is as follows.  r1 = 1
  1483. means that P0's store to x propagated to P1 before P1 called
  1484. synchronize_rcu(), so P0's critical section must have started before
  1485. P1's grace period, contrary to part (2) of the Guarantee.  On the
  1486. other hand, r2 = 0 means that P0's store to y, which occurs before the
  1487. end of the critical section, did not propagate to P1 before the end of
  1488. the grace period, contrary to part (1).  Together the results violate
  1489. the Guarantee.
  1491. In the kernel's implementations of RCU, the requirements for stores
  1492. to propagate to every CPU are fulfilled by placing strong fences at
  1493. suitable places in the RCU-related code.  Thus, if a critical section
  1494. starts before a grace period does then the critical section's CPU will
  1495. execute an smp_mb() fence after the end of the critical section and
  1496. some time before the grace period's synchronize_rcu() call returns.
  1497. And if a critical section ends after a grace period does then the
  1498. synchronize_rcu() routine will execute an smp_mb() fence at its start
  1499. and some time before the critical section's opening rcu_read_lock()
  1500. executes.
  1502. What exactly do we mean by saying that a critical section "starts
  1503. before" or "ends after" a grace period?  Some aspects of the meaning
  1504. are pretty obvious, as in the example above, but the details aren't
  1505. entirely clear.  The LKMM formalizes this notion by means of the
  1506. rcu-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(),
  1508. rcu_read_unlock(), or synchronize_rcu()) then among other things,
  1509. E ->rcu-link F includes cases where E is po-before some memory-access
  1510. event X, F is po-after some memory-access event Y, and we have any of
  1511. X ->rfe Y, X ->co Y, or X ->fr Y.
  1513. The formal definition of the rcu-link relation is more than a little
  1514. obscure, and we won't give it here.  It is closely related to the pb
  1515. relation, and the details don't matter unless you want to comb through
  1516. a somewhat lengthy formal proof.  Pretty much all you need to know
  1517. about rcu-link is the information in the preceding paragraph.
  1519. The LKMM also defines the rcu-gp and rcu-rscsi relations.  They bring
  1520. grace periods and read-side critical sections into the picture, in the
  1521. following way:
  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).
  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.)
  1533. If 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
  1535. grace period which ends before Z begins.  (In fact it covers more than
  1536. this, because it also includes cases where some store propagates to
  1537. Z's CPU before Z begins but doesn't propagate to some other CPU until
  1538. after X ends.)  Similarly, X ->rcu-rscsi Y ->rcu-link Z says that X is
  1539. the end of a critical section which starts before Z begins.
  1541. The LKMM goes on to define the rcu-order relation as a sequence of
  1542. rcu-gp and rcu-rscsi links separated by rcu-link links, in which the
  1543. number of rcu-gp links is >= the number of rcu-rscsi links.  For
  1544. example:
  1546.         X ->rcu-gp Y ->rcu-link Z ->rcu-rscsi T ->rcu-link U ->rcu-gp V
  1548. would imply that X ->rcu-order V, because this sequence contains two
  1549. rcu-gp links and one rcu-rscsi link.  (It also implies that
  1550. X ->rcu-order T and Z ->rcu-order V.)  On the other hand:
  1552.         X ->rcu-rscsi Y ->rcu-link Z ->rcu-rscsi T ->rcu-link U ->rcu-gp V
  1554. does not imply X ->rcu-order V, because the sequence contains only
  1555. one rcu-gp link but two rcu-rscsi links.
  1557. The rcu-order relation is important because the Grace Period Guarantee
  1558. means that rcu-order links act kind of like strong fences.  In
  1559. particular, E ->rcu-order F implies not only that E begins before F
  1560. ends, but also that any write po-before E will propagate to every CPU
  1561. before any instruction po-after F can execute.  (However, it does not
  1562. imply that E must execute before F; in fact, each synchronize_rcu()
  1563. fence event is linked to itself by rcu-order as a degenerate case.)
  1565. To prove this in full generality requires some intellectual effort.
  1566. We'll consider just a very simple case:
  1568.         G ->rcu-gp W ->rcu-link Z ->rcu-rscsi F.
  1570. This formula means that G and W are the same event (a grace period),
  1571. and there are events X, Y and a read-side critical section C such that:
  1573.         1. G = W is po-before or equal to X;
  1575.         2. X comes "before" Y in some sense (including rfe, co and fr);
  1577.         3. Y is po-before Z;
  1579.         4. Z is the rcu_read_unlock() event marking the end of C;
  1581.         5. F is the rcu_read_lock() event marking the start of C.
  1583. From 1 - 4 we deduce that the grace period G ends before the critical
  1584. section C.  Then part (2) of the Grace Period Guarantee says not only
  1585. that G starts before C does, but also that any write which executes on
  1586. G's CPU before G starts must propagate to every CPU before C starts.
  1587. In particular, the write propagates to every CPU before F finishes
  1588. executing and hence before any instruction po-after F can execute.
  1589. This sort of reasoning can be extended to handle all the situations
  1590. covered by rcu-order.
  1592. The rcu-fence relation is a simple extension of rcu-order.  While
  1593. rcu-order only links certain fence events (calls to synchronize_rcu(),
  1594. rcu_read_lock(), or rcu_read_unlock()), rcu-fence links any events
  1595. that are separated by an rcu-order link.  This is analogous to the way
  1596. the strong-fence relation links events that are separated by an
  1597. smp_mb() fence event (as mentioned above, rcu-order links act kind of
  1598. like strong fences).  Written symbolically, X ->rcu-fence Y means
  1599. there are fence events E and F such that:
  1601.         X ->po E ->rcu-order F ->po Y.
  1603. From the discussion above, we see this implies not only that X
  1604. executes before Y, but also (if X is a store) that X propagates to
  1605. every CPU before Y executes.  Thus rcu-fence is sort of a
  1606. "super-strong" fence: Unlike the original strong fences (smp_mb() and
  1607. synchronize_rcu()), rcu-fence is able to link events on different
  1608. CPUs.  (Perhaps this fact should lead us to say that rcu-fence isn't
  1609. really a fence at all!)
  1611. Finally, the LKMM defines the RCU-before (rb) relation in terms of
  1612. rcu-fence.  This is done in essentially the same way as the pb
  1613. relation was defined in terms of strong-fence.  We will omit the
  1614. details; the end result is that E ->rb F implies E must execute
  1615. before F, just as E ->pb F does (and for much the same reasons).
  1617. Putting this all together, the LKMM expresses the Grace Period
  1618. Guarantee by requiring that the rb relation does not contain a cycle.
  1619. Equivalently, this "rcu" axiom requires that there are no events E
  1620. and F with E ->rcu-link F ->rcu-order E.  Or to put it a third way,
  1621. the axiom requires that there are no cycles consisting of rcu-gp and
  1622. rcu-rscsi alternating with rcu-link, where the number of rcu-gp links
  1623. is >= the number of rcu-rscsi links.
  1625. Justifying the axiom isn't easy, but it is in fact a valid
  1626. formalization of the Grace Period Guarantee.  We won't attempt to go
  1627. through the detailed argument, but the following analysis gives a
  1628. taste of what is involved.  Suppose both parts of the Guarantee are
  1629. violated: A critical section starts before a grace period, and some
  1630. store propagates to the critical section's CPU before the end of the
  1631. critical section but doesn't propagate to some other CPU until after
  1632. the end of the grace period.
  1634. Putting symbols to these ideas, let L and U be the rcu_read_lock() and
  1635. rcu_read_unlock() fence events delimiting the critical section in
  1636. question, and let S be the synchronize_rcu() fence event for the grace
  1637. period.  Saying that the critical section starts before S means there
  1638. are events Q and R where Q is po-after L (which marks the start of the
  1639. critical section), Q is "before" R in the sense used by the rcu-link
  1640. relation, and R is po-before the grace period S.  Thus we have:
  1642.         L ->rcu-link S.
  1644. Let W be the store mentioned above, let Y come before the end of the
  1645. critical section and witness that W propagates to the critical
  1646. section's CPU by reading from W, and let Z on some arbitrary CPU be a
  1647. witness that W has not propagated to that CPU, where Z happens after
  1648. some event X which is po-after S.  Symbolically, this amounts to:
  1650.         S ->po X ->hb* Z ->fr W ->rf Y ->po U.
  1652. The fr link from Z to W indicates that W has not propagated to Z's CPU
  1653. at the time that Z executes.  From this, it can be shown (see the
  1654. discussion of the rcu-link relation earlier) that S and U are related
  1655. by rcu-link:
  1657.         S ->rcu-link U.
  1659. Since S is a grace period we have S ->rcu-gp S, and since L and U are
  1660. the start and end of the critical section C we have U ->rcu-rscsi L.
  1661. From this we obtain:
  1663.         S ->rcu-gp S ->rcu-link U ->rcu-rscsi L ->rcu-link S,
  1665. a forbidden cycle.  Thus the "rcu" axiom rules out this violation of
  1666. the Grace Period Guarantee.
  1668. For something a little more down-to-earth, let's see how the axiom
  1669. works out in practice.  Consider the RCU code example from above, this
  1670. time with statement labels added:
  1672.         int x, y;
  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.         }
  1682.         P1()
  1683.         {
  1684.                 int r1, r2;
  1686.                 Z: r1 = READ_ONCE(x);
  1687.                 S: synchronize_rcu();
  1688.                 W: r2 = READ_ONCE(y);
  1689.         }
  1692. If r2 = 0 at the end then P0's store at Y overwrites the value that
  1693. P1's load at W reads from, so we have W ->fre Y.  Since S ->po W and
  1694. also Y ->po U, we get S ->rcu-link U.  In addition, S ->rcu-gp S
  1695. because S is a grace period.
  1697. If r1 = 1 at the end then P1's load at Z reads from P0's store at X,
  1698. so we have X ->rfe Z.  Together with L ->po X and Z ->po S, this
  1699. yields L ->rcu-link S.  And since L and U are the start and end of a
  1700. critical section, we have U ->rcu-rscsi L.
  1702. Then U ->rcu-rscsi L ->rcu-link S ->rcu-gp S ->rcu-link U is a
  1703. forbidden cycle, violating the "rcu" axiom.  Hence the outcome is not
  1704. allowed by the LKMM, as we would expect.
  1706. For contrast, let's see what can happen in a more complicated example:
  1708.         int x, y, z;
  1710.         P0()
  1711.         {
  1712.                 int r0;
  1714.                 L0: rcu_read_lock();
  1715.                     r0 = READ_ONCE(x);
  1716.                     WRITE_ONCE(y, 1);
  1717.                 U0: rcu_read_unlock();
  1718.         }
  1720.         P1()
  1721.         {
  1722.                 int r1;
  1724.                     r1 = READ_ONCE(y);
  1725.                 S1: synchronize_rcu();
  1726.                     WRITE_ONCE(z, 1);
  1727.         }
  1729.         P2()
  1730.         {
  1731.                 int r2;
  1733.                 L2: rcu_read_lock();
  1734.                     r2 = READ_ONCE(z);
  1735.                     WRITE_ONCE(x, 1);
  1736.                 U2: rcu_read_unlock();
  1737.         }
  1739. If r0 = r1 = r2 = 1 at the end, then similar reasoning to before shows
  1740. that U0 ->rcu-rscsi L0 ->rcu-link S1 ->rcu-gp S1 ->rcu-link U2 ->rcu-rscsi
  1741. L2 ->rcu-link U0.  However this cycle is not forbidden, because the
  1742. sequence of relations contains fewer instances of rcu-gp (one) than of
  1743. rcu-rscsi (two).  Consequently the outcome is allowed by the LKMM.
  1744. The following instruction timing diagram shows how it might actually
  1745. occur:
  1747. P0                      P1                      P2
  1748. --------------------    --------------------    --------------------
  1749. rcu_read_lock()
  1750. WRITE_ONCE(y, 1)
  1751.                         r1 = READ_ONCE(y)
  1752.                         synchronize_rcu() starts
  1753.                         .                       rcu_read_lock()
  1754.                         .                       WRITE_ONCE(x, 1)
  1755. r0 = READ_ONCE(x)       .
  1756. rcu_read_unlock()       .
  1757.                         synchronize_rcu() ends
  1758.                         WRITE_ONCE(z, 1)
  1759.                                                 r2 = READ_ONCE(z)
  1760.                                                 rcu_read_unlock()
  1762. This requires P0 and P2 to execute their loads and stores out of
  1763. program order, but of course they are allowed to do so.  And as you
  1764. can see, the Grace Period Guarantee is not violated: The critical
  1765. section in P0 both starts before P1's grace period does and ends
  1766. before it does, and the critical section in P2 both starts after P1's
  1767. grace period does and ends after it does.
  1769. Addendum: The LKMM now supports SRCU (Sleepable Read-Copy-Update) in
  1770. addition to normal RCU.  The ideas involved are much the same as
  1771. above, with new relations srcu-gp and srcu-rscsi added to represent
  1772. SRCU grace periods and read-side critical sections.  There is a
  1773. restriction on the srcu-gp and srcu-rscsi links that can appear in an
  1774. rcu-order sequence (the srcu-rscsi links must be paired with srcu-gp
  1775. links having the same SRCU domain with proper nesting); the details
  1776. are relatively unimportant.
  1779. LOCKING
  1780. -------
  1782. The LKMM includes locking.  In fact, there is special code for locking
  1783. in the formal model, added in order to make tools run faster.
  1784. However, this special code is intended to be more or less equivalent
  1785. to concepts we have already covered.  A spinlock_t variable is treated
  1786. the same as an int, and spin_lock(&s) is treated almost the same as:
  1788.         while (cmpxchg_acquire(&s, 0, 1) != 0)
  1789.                 cpu_relax();
  1791. This waits until s is equal to 0 and then atomically sets it to 1,
  1792. and the read part of the cmpxchg operation acts as an acquire fence.
  1793. An alternate way to express the same thing would be:
  1795.         r = xchg_acquire(&s, 1);
  1797. along with a requirement that at the end, r = 0.  Similarly,
  1798. spin_trylock(&s) is treated almost the same as:
  1800.         return !cmpxchg_acquire(&s, 0, 1);
  1802. which atomically sets s to 1 if it is currently equal to 0 and returns
  1803. true if it succeeds (the read part of the cmpxchg operation acts as an
  1804. acquire fence only if the operation is successful).  spin_unlock(&s)
  1805. is treated almost the same as:
  1807.         smp_store_release(&s, 0);
  1809. The "almost" qualifiers above need some explanation.  In the LKMM, the
  1810. store-release in a spin_unlock() and the load-acquire which forms the
  1811. first half of the atomic rmw update in a spin_lock() or a successful
  1812. spin_trylock() -- we can call these things lock-releases and
  1813. lock-acquires -- have two properties beyond those of ordinary releases
  1814. and acquires.
  1816. First, when a lock-acquire reads from a lock-release, the LKMM
  1817. requires that every instruction po-before the lock-release must
  1818. execute before any instruction po-after the lock-acquire.  This would
  1819. naturally hold if the release and acquire operations were on different
  1820. CPUs, but the LKMM says it holds even when they are on the same CPU.
  1821. For example:
  1823.         int x, y;
  1824.         spinlock_t s;
  1826.         P0()
  1827.         {
  1828.                 int r1, r2;
  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.         }
  1838.         P1()
  1839.         {
  1840.                 WRITE_ONCE(y, 1);
  1841.                 smp_wmb();
  1842.                 WRITE_ONCE(x, 1);
  1843.         }
  1845. Here the second spin_lock() reads from the first spin_unlock(), and
  1846. therefore the load of x must execute before the load of y.  Thus we
  1847. cannot have r1 = 1 and r2 = 0 at the end (this is an instance of the
  1848. MP pattern).
  1850. This requirement does not apply to ordinary release and acquire
  1851. fences, only to lock-related operations.  For instance, suppose P0()
  1852. in the example had been written as:
  1854.         P0()
  1855.         {
  1856.                 int r1, r2, r3;
  1858.                 r1 = READ_ONCE(x);
  1859.                 smp_store_release(&s, 1);
  1860.                 r3 = smp_load_acquire(&s);
  1861.                 r2 = READ_ONCE(y);
  1862.         }
  1864. Then the CPU would be allowed to forward the s = 1 value from the
  1865. smp_store_release() to the smp_load_acquire(), executing the
  1866. instructions in the following order:
  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
  1873. and thus it could load y before x, obtaining r2 = 0 and r1 = 1.
  1875. Second, when a lock-acquire reads from a lock-release, and some other
  1876. stores W and W' occur po-before the lock-release and po-after the
  1877. lock-acquire respectively, the LKMM requires that W must propagate to
  1878. each CPU before W' does.  For example, consider:
  1880.         int x, y;
  1881.         spinlock_t x;
  1883.         P0()
  1884.         {
  1885.                 spin_lock(&s);
  1886.                 WRITE_ONCE(x, 1);
  1887.                 spin_unlock(&s);
  1888.         }
  1890.         P1()
  1891.         {
  1892.                 int r1;
  1894.                 spin_lock(&s);
  1895.                 r1 = READ_ONCE(x);
  1896.                 WRITE_ONCE(y, 1);
  1897.                 spin_unlock(&s);
  1898.         }
  1900.         P2()
  1901.         {
  1902.                 int r2, r3;
  1904.                 r2 = READ_ONCE(y);
  1905.                 smp_rmb();
  1906.                 r3 = READ_ONCE(x);
  1907.         }
  1909. If r1 = 1 at the end then the spin_lock() in P1 must have read from
  1910. the spin_unlock() in P0.  Hence the store to x must propagate to P2
  1911. before the store to y does, so we cannot have r2 = 1 and r3 = 0.
  1913. These two special requirements for lock-release and lock-acquire do
  1914. not arise from the operational model.  Nevertheless, kernel developers
  1915. have come to expect and rely on them because they do hold on all
  1916. architectures supported by the Linux kernel, albeit for various
  1917. differing reasons.
  1921. -----------------------------
  1923. In the LKMM, memory accesses such as READ_ONCE(x), atomic_inc(&y),
  1924. smp_load_acquire(&z), and so on are collectively referred to as
  1925. "marked" accesses, because they are all annotated with special
  1926. operations of one kind or another.  Ordinary C-language memory
  1927. accesses such as x or y = 0 are simply called "plain" accesses.
  1929. Early versions of the LKMM had nothing to say about plain accesses.
  1930. The C standard allows compilers to assume that the variables affected
  1931. by plain accesses are not concurrently read or written by any other
  1932. threads or CPUs.  This leaves compilers free to implement all manner
  1933. of transformations or optimizations of code containing plain accesses,
  1934. making such code very difficult for a memory model to handle.
  1936. Here is just one example of a possible pitfall:
  1938.         int a = 6;
  1939.         int *x = &a;
  1941.         P0()
  1942.         {
  1943.                 int *r1;
  1944.                 int r2 = 0;
  1946.                 r1 = x;
  1947.                 if (r1 != NULL)
  1948.                         r2 = READ_ONCE(*r1);
  1949.         }
  1951.         P1()
  1952.         {
  1953.                 WRITE_ONCE(x, NULL);
  1954.         }
  1956. On the face of it, one would expect that when this code runs, the only
  1957. possible final values for r2 are 6 and 0, depending on whether or not
  1958. P1's store to x propagates to P0 before P0's load from x executes.
  1959. But since P0's load from x is a plain access, the compiler may decide
  1960. to carry out the load twice (for the comparison against NULL, then again
  1961. for the READ_ONCE()) and eliminate the temporary variable r1.  The
  1962. object code generated for P0 could therefore end up looking rather
  1963. like this:
  1965.         P0()
  1966.         {
  1967.                 int r2 = 0;
  1969.                 if (x != NULL)
  1970.                         r2 = READ_ONCE(*x);
  1971.         }
  1973. And now it is obvious that this code runs the risk of dereferencing a
  1974. NULL pointer, because P1's store to x might propagate to P0 after the
  1975. test against NULL has been made but before the READ_ONCE() executes.
  1976. If the original code had said "r1 = READ_ONCE(x)" instead of "r1 = x",
  1977. the compiler would not have performed this optimization and there
  1978. would be no possibility of a NULL-pointer dereference.
  1980. Given the possibility of transformations like this one, the LKMM
  1981. doesn't try to predict all possible outcomes of code containing plain
  1982. accesses.  It is instead content to determine whether the code
  1983. violates the compiler's assumptions, which would render the ultimate
  1984. outcome undefined.
  1986. In technical terms, the compiler is allowed to assume that when the
  1987. program executes, there will not be any data races.  A "data race"
  1988. occurs when there are two memory accesses such that:
  1990. 1.      they access the same location,
  1992. 2.      at least one of them is a store,
  1994. 3.      at least one of them is plain,
  1996. 4.      they occur on different CPUs (or in different threads on the
  1997.         same CPU), and
  1999. 5.      they execute concurrently.
  2001. In the literature, two accesses are said to "conflict" if they satisfy
  2002. 1 and 2 above.  We'll go a little farther and say that two accesses
  2003. are "race candidates" if they satisfy 1 - 4.  Thus, whether or not two
  2004. race candidates actually do race in a given execution depends on
  2005. whether they are concurrent.
  2007. The LKMM tries to determine whether a program contains race candidates
  2008. which may execute concurrently; if it does then the LKMM says there is
  2009. a potential data race and makes no predictions about the program's
  2010. outcome.
  2012. Determining whether two accesses are race candidates is easy; you can
  2013. see that all the concepts involved in the definition above are already
  2014. part of the memory model.  The hard part is telling whether they may
  2015. execute concurrently.  The LKMM takes a conservative attitude,
  2016. assuming that accesses may be concurrent unless it can prove they
  2017. are not.
  2019. If two memory accesses aren't concurrent then one must execute before
  2020. the other.  Therefore the LKMM decides two accesses aren't concurrent
  2021. if they can be connected by a sequence of hb, pb, and rb links
  2022. (together referred to as xb, for "executes before").  However, there
  2023. are two complicating factors.
  2025. If X is a load and X executes before a store Y, then indeed there is
  2026. no danger of X and Y being concurrent.  After all, Y can't have any
  2027. effect on the value obtained by X until the memory subsystem has
  2028. propagated Y from its own CPU to X's CPU, which won't happen until
  2029. some time after Y executes and thus after X executes.  But if X is a
  2030. store, then even if X executes before Y it is still possible that X
  2031. will propagate to Y's CPU just as Y is executing.  In such a case X
  2032. could very well interfere somehow with Y, and we would have to
  2033. consider X and Y to be concurrent.
  2035. Therefore when X is a store, for X and Y to be non-concurrent the LKMM
  2036. requires not only that X must execute before Y but also that X must
  2037. propagate to Y's CPU before Y executes.  (Or vice versa, of course, if
  2038. Y executes before X -- then Y must propagate to X's CPU before X
  2039. executes if Y is a store.)  This is expressed by the visibility
  2040. relation (vis), where X ->vis Y is defined to hold if there is an
  2041. intermediate event Z such that:
  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),
  2047. and either:
  2049.         Z is connected to Y by a strong-fence link followed by a
  2050.         possibly empty sequence of xb links,
  2052. or:
  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).
  2058. The motivations behind this definition are straightforward:
  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.
  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.
  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.
  2073. To see how this works out in practice, consider our old friend, the MP
  2074. pattern (with fences and statement labels, but without the conditional
  2075. test):
  2077.         int buf = 0, flag = 0;
  2079.         P0()
  2080.         {
  2081.                 X: WRITE_ONCE(buf, 1);
  2082.                    smp_wmb();
  2083.                 W: WRITE_ONCE(flag, 1);
  2084.         }
  2086.         P1()
  2087.         {
  2088.                 int r1;
  2089.                 int r2 = 0;
  2091.                 Z: r1 = READ_ONCE(flag);
  2092.                    smp_rmb();
  2093.                 Y: r2 = READ_ONCE(buf);
  2094.         }
  2096. The smp_wmb() memory barrier gives a cumul-fence link from X to W, and
  2097. assuming r1 = 1 at the end, there is an rfe link from W to Z.  This
  2098. means that the store to buf must propagate from P0 to P1 before Z
  2099. executes.  Next, Z and Y are on the same CPU and the smp_rmb() fence
  2100. provides an xb link from Z to Y (i.e., it forces Z to execute before
  2101. Y).  Therefore we have X ->vis Y: X must propagate to Y's CPU before Y
  2102. executes.
  2104. The second complicating factor mentioned above arises from the fact
  2105. that when we are considering data races, some of the memory accesses
  2106. are plain.  Now, although we have not said so explicitly, up to this
  2107. point most of the relations defined by the LKMM (ppo, hb, prop,
  2108. cumul-fence, pb, and so on -- including vis) apply only to marked
  2109. accesses.
  2111. There are good reasons for this restriction.  The compiler is not
  2112. allowed to apply fancy transformations to marked accesses, and
  2113. consequently each such access in the source code corresponds more or
  2114. less directly to a single machine instruction in the object code.  But
  2115. plain accesses are a different story; the compiler may combine them,
  2116. split them up, duplicate them, eliminate them, invent new ones, and
  2117. who knows what else.  Seeing a plain access in the source code tells
  2118. you almost nothing about what machine instructions will end up in the
  2119. object code.
  2121. Fortunately, the compiler isn't completely free; it is subject to some
  2122. limitations.  For one, it is not allowed to introduce a data race into
  2123. the object code if the source code does not already contain a data
  2124. race (if it could, memory models would be useless and no multithreaded
  2125. code would be safe!).  For another, it cannot move a plain access past
  2126. a compiler barrier.
  2128. A compiler barrier is a kind of fence, but as the name implies, it
  2129. only affects the compiler; it does not necessarily have any effect on
  2130. how instructions are executed by the CPU.  In Linux kernel source
  2131. code, the barrier() function is a compiler barrier.  It doesn't give
  2132. rise directly to any machine instructions in the object code; rather,
  2133. it affects how the compiler generates the rest of the object code.
  2134. Given source code like this:
  2136.         ... some memory accesses ...
  2137.         barrier();
  2138.         ... some other memory accesses ...
  2140. the barrier() function ensures that the machine instructions
  2141. corresponding to the first group of accesses will all end po-before
  2142. any machine instructions corresponding to the second group of accesses
  2143. -- even if some of the accesses are plain.  (Of course, the CPU may
  2144. then execute some of those accesses out of program order, but we
  2145. already know how to deal with such issues.)  Without the barrier()
  2146. there would be no such guarantee; the two groups of accesses could be
  2147. intermingled or even reversed in the object code.
  2149. The LKMM doesn't say much about the barrier() function, but it does
  2150. require that all fences are also compiler barriers.  In addition, it
  2151. requires that the ordering properties of memory barriers such as
  2152. smp_rmb() or smp_store_release() apply to plain accesses as well as to
  2153. marked accesses.
  2155. This is the key to analyzing data races.  Consider the MP pattern
  2156. again, now using plain accesses for buf:
  2158.         int buf = 0, flag = 0;
  2160.         P0()
  2161.         {
  2162.                 U: buf = 1;
  2163.                    smp_wmb();
  2164.                 X: WRITE_ONCE(flag, 1);
  2165.         }
  2167.         P1()
  2168.         {
  2169.                 int r1;
  2170.                 int r2 = 0;
  2172.                 Y: r1 = READ_ONCE(flag);
  2173.                    if (r1) {
  2174.                            smp_rmb();
  2175.                         V: r2 = buf;
  2176.                    }
  2177.         }
  2179. This program does not contain a data race.  Although the U and V
  2180. accesses are race candidates, the LKMM can prove they are not
  2181. concurrent as follows:
  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.
  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.)
  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.
  2203. Thus U's store to buf is forced to propagate to P1 before V's load
  2204. executes (assuming V does execute), ruling out the possibility of a
  2205. data race between them.
  2207. This analysis illustrates how the LKMM deals with plain accesses in
  2208. general.  Suppose R is a plain load and we want to show that R
  2209. executes before some marked access E.  We can do this by finding a
  2210. marked access X such that R and X are ordered by a suitable fence and
  2211. X ->xb* E.  If E was also a plain access, we would also look for a
  2212. marked access Y such that X ->xb* Y, and Y and E are ordered by a
  2213. fence.  We describe this arrangement by saying that R is
  2214. "post-bounded" by X and E is "pre-bounded" by Y.
  2216. In 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.
  2219. This distinction is needed because some fences affect only loads
  2220. (i.e., smp_rmb()) and some affect only stores (smp_wmb()); otherwise
  2221. the two types of bounds are the same.  And as a degenerate case, we
  2222. say that a marked access pre-bounds and post-bounds itself (e.g., if R
  2223. above were a marked load then X could simply be taken to be R itself.)
  2225. The need to distinguish between r- and w-bounding raises yet another
  2226. issue.  When the source code contains a plain store, the compiler is
  2227. allowed to put plain loads of the same location into the object code.
  2228. For example, given the source code:
  2230.         x = 1;
  2232. the compiler is theoretically allowed to generate object code that
  2233. looks like:
  2235.         if (x != 1)
  2236.                 x = 1;
  2238. thereby adding a load (and possibly replacing the store entirely).
  2239. For this reason, whenever the LKMM requires a plain store to be
  2240. w-pre-bounded or w-post-bounded by a marked access, it also requires
  2241. the store to be r-pre-bounded or r-post-bounded, so as to handle cases
  2242. where the compiler adds a load.
  2244. (This may be overly cautious.  We don't know of any examples where a
  2245. compiler has augmented a store with a load in this fashion, and the
  2246. Linux kernel developers would probably fight pretty hard to change a
  2247. compiler if it ever did this.  Still, better safe than sorry.)
  2249. Incidentally, the other tranformation -- augmenting a plain load by
  2250. adding in a store to the same location -- is not allowed.  This is
  2251. because the compiler cannot know whether any other CPUs might perform
  2252. a concurrent load from that location.  Two concurrent loads don't
  2253. constitute a race (they can't interfere with each other), but a store
  2254. does race with a concurrent load.  Thus adding a store might create a
  2255. data race where one was not already present in the source code,
  2256. something the compiler is forbidden to do.  Augmenting a store with a
  2257. load, on the other hand, is acceptable because doing so won't create a
  2258. data race unless one already existed.
  2260. The LKMM includes a second way to pre-bound plain accesses, in
  2261. addition to fences: an address dependency from a marked load.  That
  2262. is, in the sequence:
  2264.         p = READ_ONCE(ptr);
  2265.         r = *p;
  2267. the 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
  2269. instructions corresponding to the plain load.  This is a reasonable
  2270. stipulation, since after all, the CPU can't perform the load of *p
  2271. until it knows what value p will hold.  Furthermore, without some
  2272. assumption like this one, some usages typical of RCU would count as
  2273. data races.  For example:
  2275.         int a = 1, b;
  2276.         int *ptr = &a;
  2278.         P0()
  2279.         {
  2280.                 b = 2;
  2281.                 rcu_assign_pointer(ptr, &b);
  2282.         }
  2284.         P1()
  2285.         {
  2286.                 int *p;
  2287.                 int r;
  2289.                 rcu_read_lock();
  2290.                 p = rcu_dereference(ptr);
  2291.                 r = *p;
  2292.                 rcu_read_unlock();
  2293.         }
  2295. (In this example the rcu_read_lock() and rcu_read_unlock() calls don't
  2296. really do anything, because there aren't any grace periods.  They are
  2297. included merely for the sake of good form; typically P0 would call
  2298. synchronize_rcu() somewhere after the rcu_assign_pointer().)
  2300. rcu_assign_pointer() performs a store-release, so the plain store to b
  2301. is definitely w-post-bounded before the store to ptr, and the two
  2302. stores will propagate to P1 in that order.  However, rcu_dereference()
  2303. is only equivalent to READ_ONCE().  While it is a marked access, it is
  2304. not a fence or compiler barrier.  Hence the only guarantee we have
  2305. that 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.
  2308. This is a situation where the compiler can undermine the memory model,
  2309. and a certain amount of care is required when programming constructs
  2310. like this one.  In particular, comparisons between the pointer and
  2311. other known addresses can cause trouble.  If you have something like:
  2313.         p = rcu_dereference(ptr);
  2314.         if (p == &x)
  2315.                 r = *p;
  2317. then the compiler just might generate object code resembling:
  2319.         p = rcu_dereference(ptr);
  2320.         if (p == &x)
  2321.                 r = x;
  2323. or even:
  2325.         rtemp = x;
  2326.         p = rcu_dereference(ptr);
  2327.         if (p == &x)
  2328.                 r = rtemp;
  2330. which would invalidate the memory model's assumption, since the CPU
  2331. could now perform the load of x before the load of ptr (there might be
  2332. a control dependency but no address dependency at the machine level).
  2334. Finally, it turns out there is a situation in which a plain write does
  2335. not need to be w-post-bounded: when it is separated from the other
  2336. race-candidate access by a fence.  At first glance this may seem
  2337. impossible.  After all, to be race candidates the two accesses must
  2338. be on different CPUs, and fences don't link events on different CPUs.
  2339. Well, normal fences don't -- but rcu-fence can!  Here's an example:
  2341.         int x, y;
  2343.         P0()
  2344.         {
  2345.                 WRITE_ONCE(x, 1);
  2346.                 synchronize_rcu();
  2347.                 y = 3;
  2348.         }
  2350.         P1()
  2351.         {
  2352.                 rcu_read_lock();
  2353.                 if (READ_ONCE(x) == 0)
  2354.                         y = 2;
  2355.                 rcu_read_unlock();
  2356.         }
  2358. Do the plain stores to y race?  Clearly not if P1 reads a non-zero
  2359. value for x, so let's assume the READ_ONCE(x) does obtain 0.  This
  2360. means that the read-side critical section in P1 must finish executing
  2361. before the grace period in P0 does, because RCU's Grace-Period
  2362. Guarantee says that otherwise P0's store to x would have propagated to
  2363. P1 before the critical section started and so would have been visible
  2364. to the READ_ONCE().  (Another way of putting it is that the fre link
  2365. from the READ_ONCE() to the WRITE_ONCE() gives rise to an rcu-link
  2366. between those two events.)
  2368. This 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
  2370. before the second can execute.  Therefore the two stores cannot be
  2371. concurrent and there is no race, even though P1's plain store to y
  2372. isn't w-post-bounded by any marked accesses.
  2374. Putting all this material together yields the following picture.  For
  2375. race-candidate stores W and W', where W ->co W', the LKMM says the
  2376. stores don't race if W can be linked to W' by a
  2378.         w-post-bounded ; vis ; w-pre-bounded
  2380. sequence.  If W is plain then they also have to be linked by an
  2382.         r-post-bounded ; xb* ; w-pre-bounded
  2384. sequence, and if W' is plain then they also have to be linked by a
  2386.         w-post-bounded ; vis ; r-pre-bounded
  2388. sequence.  For race-candidate load R and store W, the LKMM says the
  2389. two accesses don't race if R can be linked to W by an
  2391.         r-post-bounded ; xb* ; w-pre-bounded
  2393. sequence or if W can be linked to R by a
  2395.         w-post-bounded ; vis ; r-pre-bounded
  2397. sequence.  For the cases involving a vis link, the LKMM also accepts
  2398. sequences in which W is linked to W' or R by a
  2400.         strong-fence ; xb* ; {w and/or r}-pre-bounded
  2402. sequence with no post-bounding, and in every case the LKMM also allows
  2403. the link simply to be a fence with no bounding at all.  If no sequence
  2404. of the appropriate sort exists, the LKMM says that the accesses race.
  2406. There is one more part of the LKMM related to plain accesses (although
  2407. not to data races) we should discuss.  Recall that many relations such
  2408. as hb are limited to marked accesses only.  As a result, the
  2409. happens-before, propagates-before, and rcu axioms (which state that
  2410. various relation must not contain a cycle) doesn't apply to plain
  2411. accesses.  Nevertheless, we do want to rule out such cycles, because
  2412. they don't make sense even for plain accesses.
  2414. To this end, the LKMM imposes three extra restrictions, together
  2415. called the "plain-coherence" axiom because of their resemblance to the
  2416. rules used by the operational model to ensure cache coherence (that
  2417. is, the rules governing the memory subsystem's choice of a store to
  2418. satisfy a load request and its determination of where a store will
  2419. fall in the coherence order):
  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).
  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).
  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).
  2436. This is the extent to which the LKMM deals with plain accesses.
  2437. Perhaps it could say more (for example, plain accesses might
  2438. contribute to the ppo relation), but at the moment it seems that this
  2439. minimal, conservative approach is good enough.
  2443. -------------
  2445. This section covers material that didn't quite fit anywhere in the
  2446. earlier sections.
  2448. The descriptions in this document don't always match the formal
  2449. version of the LKMM exactly.  For example, the actual formal
  2450. definition of the prop relation makes the initial coe or fre part
  2451. optional, and it doesn't require the events linked by the relation to
  2452. be on the same CPU.  These differences are very unimportant; indeed,
  2453. instances where the coe/fre part of prop is missing are of no interest
  2454. because all the other parts (fences and rfe) are already included in
  2455. hb anyway, and where the formal model adds prop into hb, it includes
  2456. an explicit requirement that the events being linked are on the same
  2457. CPU.
  2459. Another minor difference has to do with events that are both memory
  2460. accesses and fences, such as those corresponding to smp_load_acquire()
  2461. calls.  In the formal model, these events aren't actually both reads
  2462. and fences; rather, they are read events with an annotation marking
  2463. them as acquires.  (Or write events annotated as releases, in the case
  2464. smp_store_release().)  The final effect is the same.
  2466. Although we didn't mention it above, the instruction execution
  2467. ordering provided by the smp_rmb() fence doesn't apply to read events
  2468. that are part of a non-value-returning atomic update.  For instance,
  2469. given:
  2471.         atomic_inc(&x);
  2472.         smp_rmb();
  2473.         r1 = READ_ONCE(y);
  2475. it is not guaranteed that the load from y will execute after the
  2476. update to x.  This is because the ARMv8 architecture allows
  2477. non-value-returning atomic operations effectively to be executed off
  2478. the CPU.  Basically, the CPU tells the memory subsystem to increment
  2479. x, and then the increment is carried out by the memory hardware with
  2480. no further involvement from the CPU.  Since the CPU doesn't ever read
  2481. the value of x, there is nothing for the smp_rmb() fence to act on.
  2483. The LKMM defines a few extra synchronization operations in terms of
  2484. things we have already covered.  In particular, rcu_dereference() is
  2485. treated as READ_ONCE() and rcu_assign_pointer() is treated as
  2486. smp_store_release() -- which is basically how the Linux kernel treats
  2487. them.
  2489. Although we said that plain accesses are not linked by the ppo
  2490. relation, they do contribute to it indirectly.  Namely, when there is
  2491. an address dependency from a marked load R to a plain store W,
  2492. followed by smp_wmb() and then a marked store W', the LKMM creates a
  2493. ppo link from R to W'.  The reasoning behind this is perhaps a little
  2494. shaky, but essentially it says there is no way to generate object code
  2495. for this source code in which W' could execute before R.  Just as with
  2496. pre-bounding by address dependencies, it is possible for the compiler
  2497. to undermine this relation if sufficient care is not taken.
  2499. There are a few oddball fences which need special treatment:
  2500. smp_mb__before_atomic(), smp_mb__after_atomic(), and
  2501. smp_mb__after_spinlock().  The LKMM uses fence events with special
  2502. annotations for them; they act as strong fences just like smp_mb()
  2503. except for the sets of events that they order.  Instead of ordering
  2504. all po-earlier events against all po-later events, as smp_mb() does,
  2505. they behave as follows:
  2507.         smp_mb__before_atomic() orders all po-earlier events against
  2508.         po-later atomic updates and the events following them;
  2510.         smp_mb__after_atomic() orders po-earlier atomic updates and
  2511.         the events preceding them against all po-later events;
  2513.         smp_mb_after_spinlock() orders po-earlier lock acquisition
  2514.         events and the events preceding them against all po-later
  2515.         events.
  2517. Interestingly, RCU and locking each introduce the possibility of
  2518. deadlock.  When faced with code sequences such as:
  2520.         spin_lock(&s);
  2521.         spin_lock(&s);
  2522.         spin_unlock(&s);
  2523.         spin_unlock(&s);
  2525. or:
  2527.         rcu_read_lock();
  2528.         synchronize_rcu();
  2529.         rcu_read_unlock();
  2531. what does the LKMM have to say?  Answer: It says there are no allowed
  2532. executions at all, which makes sense.  But this can also lead to
  2533. misleading results, because if a piece of code has multiple possible
  2534. executions, some of which deadlock, the model will report only on the
  2535. non-deadlocking executions.  For example:
  2537.         int x, y;
  2539.         P0()
  2540.         {
  2541.                 int r0;
  2543.                 WRITE_ONCE(x, 1);
  2544.                 r0 = READ_ONCE(y);
  2545.         }
  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.         }
  2557. Is it possible to end up with r0 = 36 at the end?  The LKMM will tell
  2558. you it is not, but the model won't mention that this is because P1
  2559. will self-deadlock in the executions where it stores 36 in y.

Raw Paste

Login or Register to edit or fork this paste. It's free.