JavaMemoryModel: missing ingredient of volatile semantic

From: Thomas Wang (wang@cup.hp.com)
Date: Thu Mar 25 2004 - 18:13:27 EST


> Strong interpretation:
> There is a happens-before (or release/acquire) relationship from
> each write to each latter read of that volatile.
>
> Weak interpretation:
> There is a happens-before (or release/acquire) relationship from
> each write to each latter read of that volatile that sees that write.

I examined the requirement of the strong interpretation. It seems the strong
interpretation could be too strict. It almost required volatile writes
to be made visible immediately, with infinite speed.

Where as the weak interpretation is just stating the obvious:
if a volatile write was observed by a read, then the volatile write must
have happened prior to the read.

I wonder could the missing ingredient be the requirement that
if a volatile write becomes visible to a read, then the volatile write
is visible to all threads. With this property you can derive behaviors
that is similar to the strong interpretation.

> 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

Before "v=1" can be made visible to any thread, "x=1" must be made visible
to all threads.
Thread 3 observes value of r1 is 1. This means "x=1" is visible to
all threads at this point. Thread 3 subsequently observes value of r2 is 2.
By the rule that if a volatile write becomes visible to a read then the
volatile write is visible to all threads, we know all threads must observe
"v=2" after "v=1".
Thread 4 observes "v=2". Since we know "v=1" is visible prior to "v=2",
and we know "x=1" is visible prior to "v=1", then we know "x=1" is
visible at this point.

QED.

Thomas Wang

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



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