Vol. 3 8-15
MULTIPLE-PROCESSOR MANAGEMENT
8.2.3.6 Stores Are Transitively Visible
The memory-ordering model ensures transitive visibility of stores; stores that are
causally related appear to all processors to occur in an order consistent with the
causality relation. This is illustrated by the following example:
Assume that r1 == 1 and r2 == 1.
• Because r1 == 1, processor 0’s store occurs before processor 1’s load.
• Because the memory-ordering model prevents a store from being reordered with
an earlier load (see Section 8.2.3.3), processor 1’s load occurs before its store.
Thus, processor 0’s store causally precedes processor 1’s store.
• Because processor 0’s store causally precedes processor 1’s store, the memory-
ordering model ensures that processor
0’s store appears to occur before
processor 1’s store from the point of view of all processors.
• Because r2 == 1, processor 1’s store occurs before processor 2’s load.
• Because the Intel-64 memory-ordering model prevents loads from being
reordered (see Section 8.2.3.2), processor 2’s load occur in order.
• The above items imply that processor 0’s store to x occurs before processor 2’s
load from x. This implies that r3
== 1.
8.2.3.7 Stores Are Seen in a Consistent Order by Other Processors
As noted in Section 8.2.3.5, the memory-ordering model allows stores by two
processors to be seen in different orders by those two processors. However, any two
stores must appear to execute in the same order to all processors other than those
performing the stores. This is illustrated by the following example:
Example 8-6. Stores Are Transitively Visible
Processor 0 Processor 1 Processor 2
mov [ _x], 1 mov r1, [ _x]
mov [ _y], 1 mov r2, [ _y]
mov r3, [_x]
Initially x == y == 0
r1 == 1, r2 == 1, r3 == 0 is not allowed
Example 8-7. Stores Are Seen in a Consistent Order by Other Processors
Processor 0 Processor 1 Processor 2 Processor 3
mov [ _x], 1 mov [ _y], 1 mov r1, [ _x] mov r3, [_y]
mov r2, [ _y] mov r4, [_x]
Initially x == y ==0
r1 == 1, r2 == 0, r3 == 1, r4 == 0is not allowed