
5.6.2.4 Litmus Test 4 (Sequence Okay)
Initially, locations x and y contain 1:
PiPj
| [U1]Pi:W<8>(x,2) | [V1]Pj:R<8>(y,2) | |
| [U2]Pi:W<8>(y,2) | [V2]Pj:R<8>(x,1) | |
| 
 | 
 | |
| Analysis: | 
 | |
| <1> | V1 reading 2 implies U2 ⇐ V1, by storage and visibility. | |
| <2> | Since V2 does not read 2, there cannot be U1 ⇐ V2. | |
| <3> | By the access order constraints, it follows from <2> that V2 ⇐ U1. | |
There are no conflicts in the sequence. There are no violations of the definition of BEFORE.
5.6.2.5 Litmus Test 5 (Sequence Okay)
Initially, locations x and y contain 1:
| Pi | Pj | 
| 
 | 
 | 
| [U1]Pi:W<8>(x,2) | [V1]Pj:R<8>(y,2) | 
| 
 | [V2]Pj:MB | 
| [U2]Pi:W<8>(y,2) | [V3]Pj:R<8>(x,1) | 
| 
 | 
 | 
Analysis:
| <1> | V1 reading 2 implies U2 ⇐ V1, by storage and visibility. | 
| <2> | V1 ⇐ V2 ⇐ V3, by processor issue constraints. | 
| <3> | V3 reading 1 implies V3 ⇐ U1, by storage and visibility. | 
There is U2 ⇐ V1 ⇐ V2 ⇐ V3 ⇐ U1. There are no conflicts in this sequence. There are no violations of the definition of BEFORE.
5.6.2.6 Litmus Test 6 (Sequence Okay)
Initially, locations x and y contain 1:
| Pi | Pj | 
[U1]Pi:W<8>(x,2)[V1]Pj:R<8>(y,2)
[U2]Pi:MB
[U3]Pi:W<8>(y,2)[V2]Pj:R<8>(x,1)
Analysis:
| <1> | U1 ⇐ U2 ⇐ U3, by processor issue constraints. | 
| <2> | V1 reading 2 implies U3 ⇐ V1, by storage and visibility. | 
| <3> | V2 reading 1 implies V2 ⇐ U1, by storage and visibility. | 
System Architecture and Programming Implications 
