Hi Jason,
> > Summary: the most meaningful exploitation of the race-free property
> > occurs in the context of race-free under SC.
> I respect your assessment, but I'm still not totally convinced about the
> above statement.
If we agree on the following
- we would like to provide SC; the only reason we don't is for performance
- SC is the only memory model that is widely understood by programmers
- programmers should generally be writing race-free programs
then I don't understand your objection to defining race-freedom in terms
of SC. It is possible to use other definitions, but the point is to make
it as easy as possible for programmers to determine that their programs
are race-free. Given a perfect (or at least conservative, but not too
conservative) race detector, it may not matter much how we define races,
but there is no such race detector, and there are reasons to believe we
could never have one--that any conservative race detector would be too
conservative. (In fact, even requiring programs to always be race-free
is generally considered too conservative.)
Now, we can quibble (and I do) with whether SC is really the model we
want to provide, but it's far too late for this argument to be had for
the JMM. In any case, no other model has widespread acceptance, so
there aren't any real alternatives.
> Now, we can either define race-free'ness based on SC or JMM.
I'm not sure what it would mean to define race-freedom in terms of the
JMM. There are at least two dangers with trying to do so. First, the
JMM (any of the proposed variants) is more complicated than SC. Thus,
a definition of races in terms of the JMM will be more complicated than
one in terms of SC. In fact, given the second assumption above, most
programmers won't understand the JMM, so they won't understand any
definition based on it. Second, we could fall into circularity. The
way the JMM is currently defined, this may not be a problem, but it
was definitely a problem in many of the early attempts to define memory
models. In fact, Sarita's work on memory models was probably the first
to address this difficulty with any clarity, and even so, circularity
in memory model definitions persisted (probably still persists).
The point is that by defining races in terms of SC, most programmers
(the ones who only understand SC) will only have to know about SC.
They won't need to understand any of the intricate details of the JMM.
Instead, they can assume SC, and just know they are required to ensure
their programs are race-free (defined in terms of SC). All the other
aspects of the JMM are only for those "expert" programmers who need to
write programs with races, and they will need to understand the JMM in
more detail. Even the expert programmers will be happy that they can
ignore the JMM details for most of their programs, which will be
race-free, and only have to think harder for a few programs where the
extra complexity of allowing races is required.
If this explanation is not convincing, perhaps you could explain more
what concrete benefits you believe will accrue by defining races in
terms of the JMM instead of SC. I didn't understand this motivation
from the examples you provided.
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:52 EDT