5.6.2.2 Litmus Test 2 (Impossible Sequence)
Initially, location x contains 1:
Pi |
| Pj |
|
| |
[U1]Pi:W<8>(x,2) | [V1]Pj:W<8>(x,3) | |
|
| [V2]Pj:R<8>(x,2) |
|
| [V3]Pj:R<8>(x,3) |
|
| |
Analysis: |
| |
<1> | Since V1 precedes V2 in processor issue sequence, V1 is visible to V2. | |
<2> | V2 reading 2 implies U1 is the latest (in ⇐ order) write to x visible to V2. | |
<3> | From <1> and <2>, V1 ⇐ U1. | |
<4> | Since U1 is visible to V2, and they are issued by different processors, U1 ⇐ V2. | |
<5> | By the processor issue constraints, V2 ⇐ V3. | |
<6> | From <4> and <5>, U1 ⇐ V3. | |
<7> | From <6> and the visibility rules, U1 is visible to V3. | |
<8> | Since both V1 and the initialization of x are BEFORE U1, U1 is the latest write to x | |
| that is visible to V3. |
|
<9> | By the definition of storage, it follows that V3 should read the value written by U1, | |
| in contradiction to the stated result. | |
Thus, once processor Pj reads a new value written by U1, any other writes that must precede the read must also precede U1. V3 must read 2.
5.6.2.3 Litmus Test 3 (Impossible Sequence)
Initially, location x contains 1:
Pi | Pj | Pk |
|
|
|
[U1]Pi:W<8>(x,2) | [V1]Pj:W<8>(x,3) | [W1]Pk:R<8>(x,3) |
[U2]Pi:R<8>(x,3) |
| [W2]Pk:R<8>(x,2) |
|
|
|
Analysis:
<1> | U2 reading 3 implies V1 is the latest write to x visible to U2, therefore U1 ⇐ V1. |
<2> | W1 reading 3 implies V1 is visible to W1, so V1 ⇐ W1 ⇐ W, therefore V1 is also |
| visible to W2. |
<3> | W2 reading 2 implies U1 is the latest write to x visible to W2, therefore V1 ⇐ U1. |
<4> | From <1> and <3>, U1 ⇐ V1 ⇐ U1. |
Again, time cannot go backwards. If V1 is ordered before U1, then processor Pk cannot read first the later value 3 and then the earlier value 2. Alternatively, if V1 is ordered before U1, U2 must read 2.
