memory-model/Documentation/explanation.txt

331 The most important relation between events is program order (po).  You
339 This is inherently a single-CPU relation; two instructions executing
343 po-loc is a sub-relation of po.  It links two memory accesses when the
422 memory model cannot assume there is a fixed program order relation
430 We say that two events are linked by a dependency relation when the
545 The reads-from relation (rf) links a write event to a read event when
557 Usage of the rf relation implicitly assumes that loads will always
723 Just like the po relation, co is inherently an ordering -- it is not
725 just like with the rf relation, we distinguish between stores that
738 The from-reads relation (fr) can be a little difficult for people to
763 As with rf, rfi, and rfe, we subdivide the fr relation into fri (when
767 Note that the fr relation is determined entirely by the rf and co
887 though smp_wmb() isn't A-cumulative.  The cumul-fence relation is
1008 where the rmw relation links the read and write events making up each
1019 degenerate case).  We write this relation as: Z0 ->rmw-sequence Zn.
1023 cumul-fence relation.  That is, if we have:
1032 the w-post-bounded relation defined below in the PLAIN ACCESSES AND
1047 "preserved program order") relation, which links the po-earlier
1048 instruction to the po-later instruction and is thus a sub-relation of
1102 includes address dependencies to loads in the ppo relation.
1246 The happens-before relation (hb) links memory accesses that have to
1247 execute in a certain order.  hb includes the ppo relation and two
1273 The third relation included in hb is like ppo, in that it only links
1276 cache coherence.  The relation is called prop, and it links two events
1373 would generate a cycle in the hb relation: The fence would create a ppo
1375 prop relation would give an hb link from the second load to the first.
1380 The formal definition of the prop relation involves a coe or fre link,
1423 In summary, the fact that the hb relation links memory access events
1427 The LKMM defines yet another relation connected to times of
1436 The propagates-before (pb) relation capitalizes on the special
1508 In summary, the fact that the pb relation links events in the order
1589 rcu-link relation.  rcu-link encompasses a very general notion of
1596 The formal definition of the rcu-link relation is more than a little
1598 relation, and the details don't matter unless you want to comb through
1613 	that this relation is "inverted": It links the end of the
1616 If we think of the rcu-link relation as standing for an extended
1624 The LKMM goes on to define the rcu-order relation as a sequence of
1640 The rcu-order relation is important because the Grace Period Guarantee
1675 The rcu-fence relation is a simple extension of rcu-order.  While
1679 the strong-fence relation links events that are separated by an
1694 Finally, the LKMM defines the RCU-before (rb) relation in terms of
1696 relation was defined in terms of strong-fence.  We will omit the
1701 Guarantee by requiring that the rb relation does not contain a cycle.
1723 relation, and R is po-before the grace period S.  Thus we have:
1737 discussion of the rcu-link relation earlier) that S and U are related
1863 The LKMM uses the srcu-rscsi relation to model SRCU read-side critical
1918 relation).  It also gives a way to tell which unlock matches a
1988 The LKMM defines a carry-srcu-data relation to express this pattern;
2284 relation (vis), where X ->vis Y is defined to hold if there is an
2654 various relation must not contain a cycle) doesn't apply to plain
2682 contribute to the ppo relation), but at the moment it seems that this
2694 definition of the prop relation makes the initial coe or fre part
2695 optional, and it doesn't require the events linked by the relation to
2734 relation, they do contribute to it indirectly.  Firstly, when there is
2741 to undermine this relation if sufficient care is not taken.