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