JavaMemoryModel: Are the volatile semantics strong enough?

From: Jan-Willem Maessen (jmaessen@alum.mit.edu)
Date: Wed Jul 30 2003 - 17:06:51 EDT


A number of us here at Sun have frantically been reading in order to
catch up with the ongoing debate.

I'm a little uncomfortable with the encoding of volatiles in the
happens-before relation (in both models---they seem to do basically
the same thing once we've transitively closed hb). Quoting Sarita's
latest draft:

"I hb J if ... (2) I is a synchronization write and J is a
synchronization read that returns the value written by I..."

This guarantees that a volatile read J will see all writes (even
non-volatile ones) performed in the thread which performed the write
I. But I'm wondering if this is enough.

Hopefully a couple of examples will clarify my confusion:

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?
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?

x=8 v=2 r1=v
v=1 x=9 r2=x
                r3=v

Can r1==r3==1 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
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



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