Compaq ECQD2KCTE Laptop User Manual


 
System Architecture and Programming Implications 5–21
5.6.2.9 Litmus Test 9 (Impossible Sequence)
Initially, location x contains 1:
Analysis:
Both <1> and <2> cannot be true. Time cannot go backwards. If V3 reads 2, then U3 must read
2. Alternatively, if U3 reads 3, then V3 must read 3.
5.6.2.10 Litmus Test 10 (Sequence Okay)
For an aligned quadword location, x, initially 100000001
16
:
Analysis:
There is no ordering cycle, so the sequence is permitted.
5.6.2.11 Litmus Test 11 (Impossible Sequence)
For an aligned quadword location, x, initially 100000001
16
:
Analysis:
Both <1> and <2> cannot be true.
Pi Pj
[U1]Pi:W<8>(x,2) [V1]Pj:W<8>(x,3)
[U2]Pi:R<8>(x,2) [V2]Pj:R<8>(x,3)
[U3]Pi:R<8>(x,3) [V3]Pj:R<8>(x,2)
<1> V3 reading 2 implies U1 is the latest write to x visible to V3, therefore V1 U1.
<2> U3 reading 3 implies V1 is the latest write to x visible to U3, therefore U1 V1.
Pi Pj
[U1]Pi:W<4>(x,2) [V1]Pj:W<4>(x+4,2)
[U2]Pi:R<8>(x,100000002
16
) [V2]Pj:R<8>(x,200000001
16
)
<1> Since U2 reads 1 from x+4, V1 is not visible to U2. Thus U2 V1.
<2> Similarly, V2 U1.
<3> U1 is visible to U2, but since they are issued by the same processor, it is not neces-
sarily the case that U1 U2.
<4> Similarly, it is not necessarily the case that V1 V2.
Pi Pj
[U1]Pi:W<4>(x,2) [V1]Pj:R<8>(x,200000001
16
)
[U2]Pi:MB or WMB
[U3]Pi:W<4>(x+4,2)
<1> V1 reading 200000001
16
implies U3 V1 U1 by storage and visibility.
<2> U1 U2 U3, by processor issue constraints.