There was some debate among us as to whether or not to try to give a
intuition for
the new model. Some thought people might just get confused by it, so we
withheld
it.
But some of us are now having second thoughts. So here is the intuition
that guided
us. It isn't a precise match-up to the semantics, but it is fairly
close.
It may or not be useful to you:
How could you possibly imagine getting the behavior described by
test case #4? The only real, half-plausible way seems to be to
allow programs to speculatively perform a write, aborting and
restarting things if, eventually, we don't commit/verify the write.
Note that by speculating on a write visible to other threads,
if we abort and rollback the speculation, we need to also
abort/rollback the other threads that were effected by the write.
But in a multithreaded context, such speculation can wind up
justifying itself, and produce behavior as seen in test case #4.
So, in general, self-justifying speculation isn't acceptable.
What if we use static analysis, and determine that there is some
way to continue the execution such that the action could occur.
Then can we speculate that the event occurs, in a way that allows
the event to self-justify itself?
Allowing this allows the behaviors of test cases #5 and #10, which
we don't want to allow.
What if we use static analysis, and determine that there is some
way to continue the execution, _without making any assumptions
about behaviors that could occur only through a data race_,
such that the action could occur.
Then we allow you to speculate that the action will occur, even if that
speculation winds up justifying itself.
Bill
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:01:00 EDT