memory-model/Documentation/explanation.txt

207 	P0 stores 1 to buf before storing 1 to flag, since it executes
271 	W: P0 stores 1 to flag   executes before
272 	X: P1 loads 1 from flag  executes before
273 	Y: P1 loads 0 from buf   executes before
274 	Z: P0 stores 1 to buf    executes before
555 executes on a separate CPU before the main program runs.
789 When CPU C executes a store instruction, it tells the memory subsystem
798 When a CPU executes a load instruction R, it first checks to see
821 premature executions; we simply say that the load executes at the
1271 has executed, which is possible if W executes shortly before R.
1279 second event executes.
1420 store to z does (the second cumul-fence), and P0's load executes after the
1439 before F executes.  The formal definition requires that E be linked to
1453 propagate to Y's CPU before X does, hence before Y executes and hence
1454 before the strong fence executes.  Because this fence is strong, we
1455 know that W will propagate to every CPU and to RAM before Z executes.
1458 propagate to every CPU and to RAM before F executes.
1583 executes.
1668 that G starts before C does, but also that any write which executes on
1687 executes before Y, but also (if X is a store) that X propagates to
1688 every CPU before Y executes.  Thus rcu-fence is sort of a
1736 at the time that Z executes.  From this, it can be shown (see the
1982 Assuming that P1 executes after P0 and does read the index value
2202 P1's store to x propagates to P0 before P0's load from x executes.
2219 test against NULL has been made but before the READ_ONCE() executes.
2231 program executes, there will not be any data races.  A "data race"
2266 (together referred to as xb, for "executes before").  However, there
2269 If X is a load and X executes before a store Y, then indeed there is
2273 some time after Y executes and thus after X executes.  But if X is a
2274 store, then even if X executes before Y it is still possible that X
2281 propagate to Y's CPU before Y executes.  (Or vice versa, of course, if
2282 Y executes before X -- then Y must propagate to X's CPU before X
2283 executes if Y is a store.)  This is expressed by the visibility
2314 	barrier executes, to propagate to all CPUs before any events
2343 executes.  Next, Z and Y are on the same CPU and the smp_rmb() fence
2346 executes.
2448 executes (assuming V does execute), ruling out the possibility of a
2453 executes before some marked access E.  We can do this by finding a
2668 	executes before, even if one or both is plain).