Hi folks,
I was out of email contact for most of today, and my email access will
be intermittant until next Friday. But I wanted to confirm a few
things people have said in my name :) and make a few other points.
First, I talked with Bill and Jeremy yesterday about their new model,
and I do now understand what they are saying, and I find it about as
easy to understand as Sarita's model. That is, I find the formalism
about as easy. The actual model is a bit more complicated because of
the prohibited set, but it seems that it may capture the intuition that
some people want, where none of the other models do. (In particular,
it forbids Causality Test 5, or at least we think it does. I'm not yet
sufficiently adept at reasoning with this model that I can say these
things with confidence--I had though SC-2 forbade that test, but I was
wrong, as Bill showed me.)
Second, I apparently keep getting confused about whether accesses to
volatiles are sequentially consistent, and what that means for the rest
of the program. Bill's response to Jan seems adequate to me, but I'll
have to give it more thought to be sure. In any case, the Manson-Pugh
model needs to be updated to reflect that additional requirement. (I
apologize to Jan for confusing him both forwards and backwards on this
issue. Serves him right for listening to me.)
Third, Sarita noted that in SC- only reads in data races need validation,
and that this point may be implicitly true in M/P as well. We should
check this to be sure. In particular, I don't see anything in M/P to
say that synchronization reads cannot be prescient. (The synchronization
order restriction needed to address Jan's point may also address this
point, however.)
Fourth, I think Hans makes a great point that I keep meaning to make:
For many executions, we probably don't really care whether they are
allowed or disallowed by the model. I feel this way about test 5
(and 10).
Fifth, Greg Wright and I have been discussing motivations for disallowing
various behaviors. (Greg couldn't send his reply directly to the list
himself, but he sent mail to Bill and me.) Basically, he would like to
have sequential consistency guaranteed, but concedes that it would be
too expensive. Once that is given up, he doesn't see much motivation
to prohibiting any other executions except for safety (including
security, etc.). Debugging help would be good too, but since we want
people to write correctly synchronized programs, the question is not
whether the restriction on the behavior enables us to understand where
a particular value comes from, but whether it helps us find the data
race that allowed non-SC behavior. (Greg, if I've misrepresented any
of your views, let me know and I'll forward your mail to the list.)
I strongly agree with this view.
Sixth, I think there are three sets of "consumers" for the JMM:
"ordinary" programmers, JVM and compiler implementors, and "expert"
programmers (e.g., Doug Lea). For "ordinary" programmers, the model
they should come away with is "Write correctly synchronized programs,
and you'll get SC. In any case, you'll get safety (whatever that
means, but definitely including type-safety)." To put it crassly, I'm
not sure we care too much about the "expert" programmers, except to
make sure that the specific non-data-race-free programs they want to
write (and that we want them to write) are correct under the JMM. If
they aren't smart enough to understand whatever model we come up with,
they don't qualify as "experts". (By "understand", I don't mean they
have a good intuitive sense--just that for any specific execution,
they can reason whether it is or is not allowed.)
Thus, I think the main audience of the JMM we are working on is
for implementors. Thus, the choice of formalism should be informed by
what these implementors will use the model for, which is probably to
prove that certain program transformations maintain correctness.
This insight (which I owe to Bill and Jeremy--or at least I formed it
from conversations with them) makes me much more comfortable with the
notion of "causality" (let's find a new name for this), which I still
do not find "natural" or "intuitive", my previous mail notwithstanding.
It's not necessary to build an intuitive programmer's model for the JMM
as programmers shouldn't be using it for the most part. They should be
writing correctly synchronized programs. Only a few programmers, and
only in a few circumstances, should ever write incorrectly synchronized
programs. The only help we need to give outside of this is to help
programmers find their data races, not reason about why they got the
particular values they did.
Thus, I want to reiterate a sentiment expressed by several (including
Sarita, Jan and me) on this list: In the absence of strong arguments
to the contrary, I would prefer to allow "strange" behaviors than
prohibit them. The only "strong" arguments that have so far been
compelling to me are "It violates either SC for correctly synchronized
programs or some safety property, as evidenced by a specific example
that we agree is bad" and "It helps us reason using the model in a way
that we want to reason using the model". And the latter is only
compelling if it is substantial or if I don't really care about the
execution in question. (I apologize to Jan and Sarita if they don't
share that opinion.)
Finally, I really appreciate all the work that everyone has done on
the model, especially Bill and Jeremy and Sarita. As Jan said, I too
am frankly amazed. I held out little hope that I would ever
understand the Manson-Pugh model, but Jeremy and Bill have done a
great job in cleaning it up, and even swaying me in some ways to their
side (even though I still prefer the model to be weak). Thanks too to
Jan, Greg Wright, Eric Allen, Dave Detlefs, Alex Garthwaite and others
who have let me bounce ideas off them, and bounced many of their own
on me, and given me much food for thought, and of course, to Sarita
for providing a model which allowed us to discuss these issues more
clearly.
Victor
-------------------------------
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