I'll try to respond in detail to Sarita's comments and those of others shortly.
But let me just provide a high-level summary of our approach.
Initially, we worked our way through various operational models and
other specialized definitions. Part of the problem is that there is
no pre-existing set of complete requirements for the memory model,
which spells out all the behaviors that must be prohibited and all
the behaviors that must be allowed.
Several times, we thought we had a workable semantics, and then came
up with a example that couldn't be handled by that semantics.
We have now moved to a very simple semantics: consistency and causality.
1) Consistency requires that behavior is consistent with both intra-thread
semantics and the write visibility enforced by the happens-before ordering.
2) Causality means that an action cannot cause itself to happen. In other
words, it must be possible to explain how a execution occurred, without
there existing an action x requiring that x be assumed to occur in order to
show that x did occur.
That's it for the core model (excluding stuff like final fields, etc).
Now it turns out that formalizing causality is not easy, and there
are some tricky corner cases (such as what happens when redundant
read eliminations allows that guarantee that two reads always see the
same value).
Now, it turns out that consistency and causality give all sorts of
properties we need, such as:
* Correctly synchronized programs have SC behavior
* No values can appear out of thin air
Sartia argues that both consistency and causality are too strong, and
that incorrectly synchronized programs should be allowed to violate
both. Instead, she has tried to come up with a weaker model that
enforces only a set of specific properties that we have enumerated,
such as out-of-thin-air safety.
I believe that correctly synchronized programs are the exception
rather than the rule. Mistakes in programming are all too common.
So I have come to believe that consistency and causality are
properties any execution should have, even executions of
unsynchronized programs. I've yet to find any desirable optimizations
that would violate these properties, and I think it would be very
hard to devise such an optimization that didn't also violate other
properties we've agreed are essential.
An additional advantage is that we can provide an informal but
complete description description of the core memory model in a manner
appropriate
for something like JavaWorld or the next edition of Doug's book, and
that many programmers could develop an accurate mental model of the
JMM, without needing to look at any formal definitions.
Bill
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:46 EDT