Compaq ECQD2KCTE Laptop User Manual


 
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.