At 3:04 PM -0500 7/28/03, Sarita Adve wrote:
>SC-, as currently formalized, does not allow example 2 in Bill's message (I
>mistakenly convinced myself and Bill otherwise over the weekend).
>
>
OK, so Sarita's model will not allow r1 == r2 == r3 == 1
in the following code:
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
However, it will allow r1 == r2 == r3 == 1, r4 = 0
in the following code:
Example 2a:
Initially, X = 0, Y = 0, Z = 0, a[0] = 1, a[1] = 2
Thread 1 Thread 2 Thread 3 Thread 4
r1 = X r3 = Y Z = 1 r4 = Z
a[r1] = 0 X = r3 Y = r4
r2 = a[0]
Y = r2
This is the same as Example 2, except that it is possible that thread
3 and thread 4 could, together, write 1 to Y. However, since r4 = 0,
we know that in this execution they did not write 1 to Y.
So, to understand how an execution could have happened under Sarita's
model, you have to reason about another execution that could have
occurred but definitely did not.
So I still find the behavior of Example 2a profoundly troubling.
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:47 EDT