Re: JavaMemoryModel: New Causality Test

From: William Pugh (pugh@cs.umd.edu)
Date: Sun Feb 15 2004 - 10:53:57 EST


As Hans stated, I think it is pretty clear that we can't allow the
behavior r = 1 in the example Jerry provided.

If a loop never terminates, the code that occurs after the loop does
not effectively exist, and must not be visible.

For a slightly more interesting example, consider:

Initially, x = y = 0

Thread 1:
do {
   r1 = x;
   } while (r1 == 0);
y = 1

Thread 2:
r2 = y
if (r2 == 1)
   x = 1

This is also a correctly synchronized program, so the only legal
behavior is to have r2 = 0 and thread 1 never terminating.

If you change the example to:

Initially, x = y = 0

Thread 1:
do {
   r1 = x;
   } while (r1 == 0);
y = 1

Thread 2:
r2 = y
x = r2

then the program is no longer correctly synchronized, but I believe
that the acceptable behaviors should not change (and does not change
in our model).

        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:57 EDT