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
r3=w
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
jmaessen@alum.mit.edu
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:49 EDT