JavaMemoryModel: Re: Are the volatile semantics strong enough?

From: Jan-Willem Maessen (jmaessen@MIT.EDU)
Date: Wed Jul 30 2003 - 17:37:15 EDT

Alex Garthwaite points out that I messed up not one, but both of my
examples in a rush to get my mail out:
> Assume v and w are volatile locations, x is a regular location.
> v=1 w=1 r1=v r3=w
> r2=w r4=v
> Can r1 == r3 == 1, but r2 == r4 == 1?

This ought to read r2 == r4 == 0.

> Clearly not, if we believe that volatiles are SC. But this is not
> captured by happens before, and it's unclear to me where in Bill &
> Jeremy's semantics this behavior is prohibited. Bill, Jeremy, can one
> of you enlighten me?

In this case:
> x=8 v=2 r1=v
> v=1 x=9 r2=x
> r3=v
> Can r1==r3==1 but r2==9?

Should have read:
x=8 w=2 r1=v
v=1 x=9 r2=x

Can r1==1, r3==0 but r2==9?

> I remember arguments that this would be a
> bad thing, and therefore we don't want r3=v hb v=2, preventing us from
> totally ordering actions to a volatile location v in hb. I cannot
> recall why.
> ------------------------------------------------------------
> One thing has become clear to me is that the total ordering we obtain
> on locks and volatiles is entirely separate from the notion of happens
> before. The existence of a separate ordering is only mentioned in
> passing in both semantics (under the rubric of SC in Sarita's). And
> it's not clear to me where it fits in to Bill and Jeremy's semantics
> at all. I'd love to see it formalized as well, if only to say
> "There's a total ordering on synchronization operations which must be
> consistent with program order. It's otherwise not the same as any of
> the other orderings (hb, co, etc.) we're talking about here."
> -Jan-Willem Maessen

Let this be a lesson to anyone attempting to simplify their examples
as they copy them off their white board.

-Jan-Willem Maessen
JavaMemoryModel mailing list -

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