5–20 Alpha Architecture Handbook
There is V2 ⇐ U1 ⇐ U2 ⇐ U3 ⇐ V1. There are no conflicts in this sequence. There are no
violations of the definition of BEFORE.
In litmus tests 4, 5, and 6, writes to two different locations x and y are observed (by another
processor) to occur in the opposite order than that in which they were performed. An update to
y propagates quickly to Pj, but the update to x is delayed, and Pi and Pj do not both have MBs.
5.6.2.7 Litmus Test 7 (Impossible Sequence)
Initially, locations x and y contain 1:
Analysis:
Both <1> and <5> cannot be true, so if V1 reads 2, then V3 must also read 2.
If both x and y are in memory-like regions, the sequence remains impossible if U2 is changed
to a WMB. Similarly, if both x and y are in non-memory-like regions, the sequence remains
impossible if U2 is changed to a WMB.
5.6.2.8 Litmus Test 8 (Impossible Sequence)
Initially, locations x and y contain 1:
Analysis:
Both <1> and <5> cannot be true, so if U3 reads 1, then V3 must read 2, and vice versa.
Pi Pj
[U1]Pi:W<8>(x,2) [V1]Pj:R<8>(y,2)
[U2]Pi:MB [V2]Pj:MB
[U3]Pi:W<8>(y,2) [V3]Pj:R<8>(x,1)
<1> V3 reading 1 implies V3 ⇐ U1, by storage and visibility.
<2> V1 reading 2 implies U3 ⇐ V1, by storage and visibility.
<3> U1 ⇐ U2 ⇐ U3, by processor issue constraints.
<4> V1 ⇐ V2 ⇐ V3, by processor issue constraints.
<5> By <2>, <3>, and <4>, U1 ⇐ U2 ⇐ U3 ⇐ V1 ⇐ V2 ⇐ V3.
Pi Pj
[U1]Pi:W<8>(x,2) [V1]Pj:W<8>(y,2)
[U2]Pi:MB [V2]Pj:MB
[U3]Pi:R<8>(y,1) [V3]Pj:R<8>(x,1)
<1> V3 reading 1 implies V3 ⇐ U1, by storage and visibility.
<2> U3 reading 1 implies U3 ⇐ V1, by storage and visibility.
<3> U1 ⇐ U2 ⇐ U3, by processor issue constraints.
<4> V1 ⇐ V2 ⇐ V3, by processor issue constraints.
<5> By <2>, <3>, and <4>, U1 ⇐ U2 ⇐ U3 ⇐ V1 ⇐ V2 ⇐ V3.