I want to enumerate several of the executions allowed by Sarita's
model that I find profoundly troubling.
Example 1:
Initially, x = y = z = 0
Thread 1:
x = 1
Thread 2:
r1 = x
y = r1
Thread 3:
r2 = y
z = r2
Thread 4:
r3 = z
y = r3
Troubling execution: r1 == 0, r2 == r3 == 1.
This execution is troubling because, given that r1 = 0, the only way
r2 could be 1 is if thread 4 wrote 1 to y. And the only way that
could be true is if r3 is one, which could only be true if r2 is one.
So in this example, there is no causal way to explain how r2 and r3
became one.
Example 2:
Initially, x = 0, y = 0, a[0] = 1, a[1] = 2
Thread 1 Thread 2
r1 = X r3 = Y
a[r1] = 0 X = r3
r2 = a[0]
Y = r2
Troubling execution r1 == r2 == r3 == 1
This execution is troubling because in order for r2 to be 1, r1 must
have been 1. But r1 could be one only if thread 2 wrote 1 to X. Which
could only be true if thread 2 read 1 from Y. Which could only be
true if r2 is 1.
Example 3 (I haven't had a chance to run this one by Sarita yet):
Initially, x = 1, y = 0
Thread 1:
r1 = x
y = r1+1
x = r1
Thread 2:
r2 = y
x = r2+2
Troubling execution r1 = 4 and r2 = 5
How could this happen in Sarita's model? Basically, the read of x in
thread 1 has to see the later write to x in thread 1. Which both
involves seeing a read in violation of the happens-before ordering
and is a causality violation.
There is a race D1 between the read of x in thread 1 and the write of
x in thread 2. There is a SC execution in which r1 = x comes first,
the race occurs, and thread 2 writes 4 to x. Thus, Prefix:1 is empty,
and P|D1 will be a program that just sets r1 = 4. Which allows r1 = 4
and r2 = 5.
Bill
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:46 EDT