
5.6.1.9 Timeliness
Even in the absence of a barrier after the write, no write by a processor may be delayed indefi- nitely in the BEFORE ordering.
5.6.2 Litmus Tests
Many issues about writing and reading shared data can be cast into questions about whether a write is before or after a read. These questions can be answered by rigorously checking whether any ordering satisfies the rules in Sections 5.6.1.3 through 5.6.1.8.
In litmus tests
5.6.2.1 Litmus Test 1 (Impossible Sequence)
Initially, location x contains 1:
PiPj
[U1]Pi:W<8>(x,2)[V1]Pj:R<8>(x,2) [V2]Pj:R<8>(x,1)
Analysis:
<1> | By the definition of storage (Section 5.6.1.6), V1 reading 2 implies that U1 is visible |
| to V1. |
<2> | By the rules for visibility (Section 5.6.1.5), U1 being visible to V1, but being issued |
| by a different processor, implies that U1 ⇐ V1. |
<3> | By the processor issue constraints (Section 5.6.1.3), V1 ⇐ V2. |
<4> | By the transitivity of the partial order ⇐, it follows from <2> and <3> that U1 ⇐ |
| V2. |
<5> | By the rules for visibility, it follows from U1 ⇐ V2 that U1 is visible to V2. |
<6> | Since U1 is AFTER the initialization of x, U1 is the latest (in the ⇐ ordering) write |
| to x that is visible to V1. |
<7> | By the definition of storage, it follows that V2 should read the value written by U1, |
| in contradiction to the stated result. |
Thus, once a processor reads a new value from a location, it must never see an old value – time must not go backward. V2 must read 2.
System Architecture and Programming Implications