JavaMemoryModel: Another litmus test for strong vs. weak volatiles

From: Bill Pugh (pugh@cs.umd.edu)
Date: Thu Mar 18 2004 - 13:29:53 EST


For me, and perhaps others, litmus tests are a good way of understanding
the details of semantics.

So here is another litmus test for strong vs. weak semantics:

Initially, x = y = v = 0, v is volatile

Thread 1:
x = 1
v = 1

Thread 2:
y = 1
v = 2

Thread 3:
r1 = v
r2 = v

Thread 4:
r3 = v
r4 = x

Behavior in question: r1 = 1, r2 = 2, r3 = 2, r4 = 0

This behavior is legal under the weak interpretation, illegal under the
strong
interpretation for volatile.

Explanation: if we have r1 = 1 and r2 = 2, we know the write v = 1 was
ordered
before the write v = 2.

If we have r3 = 2, we know the write v = 2 comes before the read r3 = v.

So is there a happens-before edge from x = 1 to r4 = x? There is under
the strong semantics, but not under the weak semantics.

        Bill

-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:01:00 EDT