RE: JavaMemoryModel: Another litmus test for strong vs. weak volatiles

From: David Holmes (dholmes@dltech.com.au)
Date: Mon Mar 29 2004 - 19:30:45 EST


> On Mar 26, 2004, at 7:45 PM, David Holmes wrote:
> > "roach motel" rules are exact/complete. ie if my code contains no
> > thread-local volatiles or thread-local sync then I CAN explain the
> > behaviour in terms of the "barriers" (memory AND code-motion) inherent
in the
> > "roach motel" rules. Right?
> >
> >
>
> No.
>
> Consider:
>
> Initially, x = y = v = 0, v is volatile
>
> Thread 1:
> r3 = y
> v = 1
> r2 = v
> x = 1
>
> Thread 2:
> r1 = v
> v = r1+1
>
> Thread 3:
> r4 = x
> y = r4
>
> Execution in question:
> r1 = 1, r2 = 2, r3 == r4 == 1
>
> OK, so v is not thread local, and so it can't be removed.
> Roach motel order would prevent reordering the read of y or the write
> of x in thread 1.

That's fine. r3 is not guaranteed to read a particular value of y. The write
to x is not guaranteed to be visible to any other thread - but could be.

> But the ordering constraints on x and y are only visible to thread 2,
> not thread 3.

Yes. There is no synchronization in thread 3 with any other thread - so it
can see anything for x. This is not a correctly synchronized program.

> So it is possible for thread 3 to see the write to x by thread 1, and
> for thread 1 to see the write to y by thread 3.

Now you lost me again. If thread 3 sees the write to x by thread 1 then:

  t1: x = 1 hb t3: r4 = x

And if thread 1 sees the write to y by thread 3 then:

  t3: y = r4 hb t1: r3 = y

But t3: r4 = x hb t3: y = r4 because there is a data dependency, so
program order has to be obeyed.

And t1: r3 = y hb t1: x = 1 because of the volatile read and write of v

And that's a contradiction.

Is that you point? That the statements in thread 1 can be reordered? If so
what are the allowed reorderings?

David Holmes

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



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