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