memory-model/Documentation/explanation.txt

86 store instruction accessing the same location (we ignore complicating
169 store to buf but before the store to flag.  In this case, r1 and r2
191 store to the same memory location, from any CPU.
197 	Since r1 = 1, P0 must store 1 to flag before P1 loads 1 from
205 	store to the same address.
210 	Since an instruction (in this case, P0's store to flag) cannot
219 x86 and SPARC follow yet a different memory model: TSO (Total Store
222 Consistency.  One example is the Store Buffer (SB) pattern, in which
319 is concerned only with the store itself -- its value and its address
386 both branches of an "if" statement store the same value to the same
412 from x could be executed after the store to y.  Thus, the memory
481 a control dependency from the load to the store.
498 There appears to be a data dependency from the load of x to the store
547 write.  In colloquial terms, the load "reads from" the store.  We
548 write W ->rf R to indicate that the load R reads from the store W.  We
549 further distinguish the cases where the load and the store occur on
554 though it had been written there by an imaginary initial store that
558 read from a single store.  It doesn't apply properly in the presence
559 of load-tearing, where a load obtains some of its bits from one store
560 and some of them from another store.  Fortunately, use of READ_ONCE()
621 another.  The imaginary store which establishes x's initial value
622 comes first in the coherence order; the store which directly
623 overwrites the initial value comes second; the store which overwrites
640 	Write-read coherence: If W ->po-loc R, where W is a store and R
641 	is a load, then R must read from W or from some other store
645 	is a store, then the store which R reads from must come before
649 	loads, then either they read from the same store or else the
650 	store read by R comes before the store read by R' in the
658 requirement that every store eventually becomes visible to every CPU.)
675 write-write coherence rule: Since the store of 23 comes later in
677 thus must overwrite the store of 17.
690 rule: The READ_ONCE() load comes before the WRITE_ONCE() store in
691 program order, so it must not read from that store but rather from one
710 If r1 = 5 (reading from P0's store) and r2 = 0 (reading from the
711 imaginary store which establishes x's initial value) at the end, this
713 the r2 load in program order, so it must not read from a store that
724 possible for a store to directly or indirectly overwrite itself!  And
740 overwritten by a store.  In other words, we have R ->fr W when the
742 equivalently, when R reads from a store which comes earlier than W in
764 the load and the store are on the same CPU) and fre (when they are on
789 When CPU C executes a store instruction, it tells the memory subsystem
790 to store a certain value at a certain location.  The memory subsystem
791 propagates the store to all the other CPUs as well as to RAM.  (As a
792 special case, we say that the store propagates to its own CPU at the
794 store falls in the location's coherence order.  In particular, it must
795 arrange for the store to be co-later than (i.e., to overwrite) any
796 other store to the same location which has already propagated to CPU C.
799 whether there are any as-yet unexecuted store instructions, for the
801 uses the value of the po-latest such store as the value obtained by R,
802 and we say that the store's value is forwarded to R.  Otherwise, the
805 of the co-latest store to the location in question which has already
809 CPUs have local caches, and propagating a store to a CPU really means
811 time to process the stores that it receives, and a store can't be used
849 	execute all po-earlier instructions before the store
850 	associated with the fence (e.g., the store part of an
859 	For each other CPU C', any store which propagates to C before
862 	store associated with the release fence does.
864 	Any store which propagates to C before a strong fence is
951 each load between the store that it reads from and the following
952 store.  This leaves the relative positions of loads that read from the
953 same store unspecified; let's say they are inserted in program order,
994 occurs in between CPU 1's load and store.  To put it another way, the
995 problem is that the position of CPU 0's store in x's coherence order
996 is between the store that CPU 1 reads from and the store that CPU 1
1018 where Z0 is some store event and n can be any number (even 0, in the
1028 operational model, U ->cumul-fence X says that the store U propagates
1029 to each CPU before the store X does.  Then the fact that X and Y are
1078 store; either a data, address, or control dependency from a load R to
1079 a store W will force the CPU to execute R before W.  This is very
1081 store before it knows what value should be stored (in the case of a
1083 of an address dependency), or whether the store should actually take
1106 store and a second, po-later load reads from that store:
1112 W, because it can forward the value that W will store to R'.  But it
1120 (In theory, a CPU might forward a store to a load when it runs across
1127 because it could tell that the store and the second load access the
1133 program order if the second access is a store.  Thus, if we have
1140 read request with the value stored by W (or an even later store), in
1186 smp_wmb() forces P0's store to x to propagate to P1 before the store
1194 that the first store is processed by a busy part of the cache while
1195 the second store is processed by an idle part.  As a result, the x = 1
1223 its second load, the x = 1 store would already be fully processed by
1251 that W's store must have propagated to R's CPU before R executed;
1265 execute before W, because the decision as to which store overwrites
1277 on CPU C in situations where a store from some other CPU comes after
1301 had executed before its store then the value of the store would have
1304 event, because P1's store came after P0's store in x's coherence
1305 order, and P1's store propagated to P0 before P0's load executed.
1327 then the x = 9 store must have been propagated to P0 before the first
1330 because P1's store overwrote the value read by P0's first load, and
1331 P1's store propagated to P0 before P0's second load executed.
1359 overwritten by P0's store to buf, the fence guarantees that the store
1360 to buf will propagate to P1 before the store to flag does, and the
1361 store to flag propagates to P1 before P1 reads flag.
1365 from flag were executed first, then the buf = 1 store would already
1414 link from P0's store to its load.  This is because P0's store gets
1415 overwritten by P1's store since x = 2 at the end (a coe link), the
1416 smp_wmb() ensures that P1's store to x propagates to P2 before the
1417 store to y does (the first cumul-fence), the store to y propagates to P2
1418 before P2's load and store execute, P2's smp_store_release()
1420 store to z does (the second cumul-fence), and P0's load executes after the
1421 store to z has propagated to P0 (an rfe link).
1438 store is coherence-later than E and propagates to every CPU and to RAM
1444 Consider first the case where E is a store (implying that the sequence
1465 have propagated to E's CPU before E executed.  If E was a store, the
1469 request with the value stored by W or an even later store,
1496 load: an fre link from P0's load to P1's store (which overwrites the
1497 value read by P0), and a strong fence between P1's store and its load.
1532 (1)	C ends before G does, and in addition, every store that
1536 (2)	G starts before C does, and in addition, every store that
1566 means that P0's store to x propagated to P1 before P1 called
1569 other hand, r2 = 0 means that P0's store to y, which occurs before the
1619 this, because it also includes cases where some store propagates to
1687 executes before Y, but also (if X is a store) that X propagates to
1713 store propagates to the critical section's CPU before the end of the
1727 Let W be the store mentioned above, let Y come before the end of the
1775 If r2 = 0 at the end then P0's store at Y overwrites the value that
1780 If r1 = 1 at the end then P1's load at Z reads from P0's store at X,
1910 of store event (again appropriate, since it takes as arguments a
1920 from the load (srcu-lock) to the store (srcu-unlock).  For example,
1953 since it reads from the immediately preceding store of idx1 in s.
1958 However, sometimes it is necessary to store an index value in a
1996 need to ensure that none of the intermediate store events in this
2005 the LKMM treats B as a store to the variable s and C as a load from
2048 store-release in a spin_unlock() and the load-acquire which forms the
2149 the spin_unlock() in P0.  Hence the store to x must propagate to P2
2150 before the store to y does, so we cannot have r2 = 1 and r3 = 0.  But
2202 P1's store to x propagates to P0 before P0's load from x executes.
2218 NULL pointer, because P1's store to x might propagate to P0 after the
2236 2.	at least one of them is a store,
2269 If X is a load and X executes before a store Y, then indeed there is
2274 store, then even if X executes before Y it is still possible that X
2279 Therefore when X is a store, for X and Y to be non-concurrent the LKMM
2283 executes if Y is a store.)  This is expressed by the visibility
2342 means that the store to buf must propagate from P0 to P1 before Z
2431 	Consequently U's store to buf, no matter how it is carried out
2432 	at the machine level, must propagate to P1 before X's store to
2447 Thus U's store to buf is forced to propagate to P1 before V's load
2462 "w-pre-bounded" by Y, depending on whether E was a store or a load.
2470 issue.  When the source code contains a plain store, the compiler is
2482 thereby adding a load (and possibly replacing the store entirely).
2483 For this reason, whenever the LKMM requires a plain store to be
2485 the store to be r-pre-bounded or r-post-bounded, so as to handle cases
2489 compiler has augmented a store with a load in this fashion, and the
2494 adding in a store to the same location -- is not allowed.  This is
2497 constitute a race (they can't interfere with each other), but a store
2498 does race with a concurrent load.  Thus adding a store might create a
2500 something the compiler is forbidden to do.  Augmenting a store with a
2544 rcu_assign_pointer() performs a store-release, so the plain store to b
2545 is definitely w-post-bounded before the store to ptr, and the two
2606 Guarantee says that otherwise P0's store to x would have propagated to
2612 This means there is an rcu-fence link from P1's "y = 2" store to P0's
2613 "y = 3" store, and consequently the first must propagate from P1 to P0
2615 concurrent and there is no race, even though P1's plain store to y
2632 sequence.  For race-candidate load R and store W, the LKMM says the
2661 is, the rules governing the memory subsystem's choice of a store to
2662 satisfy a load request and its determination of where a store will
2667 	not allowed (i.e., a load cannot read from a store that it
2672 	not allowed (i.e., if a store is visible to a load then the
2673 	load must read from that store or one coherence-after it).
2677 	is not allowed (i.e., if one store is visible to a second then
2735 an address dependency from a marked load R to a plain store W,
2736 followed by smp_wmb() and then a marked store W', the LKMM creates a
2744 links a marked load R to a store W, and the store is read by a load R'