[Sorry for the long delays in replies, this week was a rather busy one
for me before I started trying to catch up on the JMM debate. Sarita,
in particular, sent mail off-list two days ago. I hope the reply here
will answer her concerns.]
Bill writes:
> We have a general rule that:
> * correctly synchronized programs exhibit only SC behaviors
>
> Now, I think we need to classify any program using only volatile variables
> as correctly synchronized.
>
> Which means that programs that use only volatile variables exhibit
> only SC behaviors.
Thank you for clarifying this. From my reading of the models circa
Wednesday, I'd concluded that:
* In Sarita's models they appeared to be SC by fiat---because
synchronization accesses were considered race-free.
* Volatiles weren't obviously SC in the CnC model.
* I was fuzzy on the desired interaction between regular and volatile
reads/writes.
* I wanted to be clear on the relationship between synchronization and
program order.
Subsequent postings managed to convince Victor Luchangco (and through
him, me) that synchronization wasn't supposed to be SC at all. You've
thankfully disabused me of that notion. Synchronization is SC.
> I think, as Jan-Willem suggestions, that the way to solve this is to
> say that there is a total order over all synchronization actions that
> is consistent with program order. This total order is used to
> determine when there is an inter-thread hb edge induced from
> synchronization actions and which value is seen by volatile reads.
> The synchronization order will be consistent with hb order, but need
> not be consistent with the causal order.
OK. So there's a total order on *all* synchronization, and it must be
consistent with program order. But only the transitive edges from
synchronization writes to corresponding synchronization reads end up
in the resulting hb relation. This gives the "roach motel" semantics
wrt regular memory operations.
This matches my assumed understanding of the world.
There are a lot of orderings kicking around in both formalisms:
* Program order
* Synchronization order
* Execution order
* Happens before
The recent one-page formalisms from both Sarita and from Jeremy and
Bill have made it much easier for me to determine the relationships
among all of these. I think the relationship between synchronization
order, program order, and happens before could be more clearly stated
in both semantics. Something like Bill's paragraph above would be
just the thing.
That said, there's been dramatic improvement over the course of the
week. I'm frankly amazed.
I meanwhile remain disturbed by some of what we can do under the
rubric of causality (the examples with conditionals uniformly make me
twitch). But I understand the reasons for these decisions, and have
found myself arguing both sides over the past few days. In the end, I
agree with Victor that we have to try for the weakest possible
semantics we can.
-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