Causality test case 5:
Initially, x = y = z = 0
Thread 1:
r1 = x
y = r1
Thread 2
r2 = y
x = r2
Thread 3
z = 1
Thread 4
r3 = z
x = r3
Behavior in question: r1 = r2 = 1, r3 = 0.
We start by executing
r2 = y (1)
This is a data race, so we need to show that r2 = y (1) is an
allowable discontinuity. Considering the following Esc:
r2 = y (1)
z = 1
r3 = z (1)
x = r3
r1 = x (1)
y = r1 // This is W; it writes 1 to y
x = r2
So this discontinuity is allowed, so long as W occurs in the
execution we are generating.
Here is the rest of the execution I wish to generate. Each data race read in
the remainder of the execution sees a previous write, so no
additional reasoning is required.
r2 = y (1)
x = r2
r1 = x (1)
y = r1 // This is W; it writes 1 to y
r3 = z (0)
x = r3
z = 1
Since W occurs in the executed we generated, our proof obligation is
satisfied, and the execution is allowed.
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:49 EDT