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 1–9 below, all initial quadword memory locations contain 1. In all these litmus tests, it is assumed that initializations are performed by a write or writes that are BEFORE all the explicitly listed accesses, that all relevant writes other than the initializations are explicitly shown, and that all accesses shown are to memory-like regions (so the definition of storage applies).

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 5–17

Page 229
Image 229
Compaq ECQD2KCTE manual Litmus Tests, Timeliness, Litmus Test 1 Impossible Sequence, PiPj