Sarita's new model does not seem unreasonable. But Jeremy and I
have only had a week to review it, and have not yet managed to feel
comfortable with it at any intuitive level. We've looked at the
proofs, and don't see any obvious flaws but also don't have
confidence that they are correct. Our experience over the past year
or two has shown that this is very subtle stuff, and both Sarita and
us have found holes in each other's approaches (and those of others)
only after months of staring at them.
The model Jeremy and I have been working on has only undergone
tweaks in the past several months, and we have a simulator that runs
it over dozens of test cases, verifying that the results are as we
expect.
We have about weeks to finish up the public review draft, and to
the extent people have time to spend on the JMM, I'd like to
encourage people to further examine final fields and other
non-causality related issues, which haven't gotten the attention they
need. Jeremy and I have a lot of work to do finishing up the
document, doing Javadoc comments, and so on.
So here is my proposal.
I think we need to keep the current formalism for the core memory
model. However, we will change the proposal to note that the details
of the causality semantics come from trying to find a way of
formalizing informal constraints, and that people should not be
writing code that depends upon the formal causality details. It is
not the intention of the semantics to forbid reasonable compiler or
architectural optimizations that might, in combination, produce
surprising results. If, in the future, we find such optimizations
that lead to violations of the formal causality spec, the spec may be
changed in future revisions of the JLS to accommodate them. It
particular, causality test cases 5 and 10 will be listed as ones that
are forbidden by the current formalism, but that if future
optimizations make it desirable to allow them, and no compelling
safety or security problem is found to result from allowing them,
then it is likely that the JLS would be revised to allow them.
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:56 EDT