RE: JavaMemoryModel: Executions I find profoundly troubling

From: Bill Pugh (pugh@cs.umd.edu)
Date: Mon Jul 28 2003 - 16:26:54 EDT


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