Compaq ECQD2KCTE manual Litmus Test 7 Impossible Sequence, Litmus Test 8 Impossible Sequence

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:

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)

Analysis:

<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.

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:

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)

Analysis:

<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.

Both <1> and <5> cannot be true, so if U3 reads 1, then V3 must read 2, and vice versa.

5–20Alpha Architecture Handbook