Filter
Top Products
System Architecture and Programming Implications 5–19
5.6.2.4 Litmus Test 4 (Sequence Okay)
Initially, locations x and y contain 1:
Analysis:
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:
Analysis:
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:
Analysis:
Pi Pj
[U1]Pi:W<8>(x,2) [V1]Pj:R<8>(y,2)
[U2]Pi:W<8>(y,2) [V2]Pj:R<8>(x,1)
<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.
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)
<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.
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)
<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.