Re: JavaMemoryModel: The property of "race-free implies SC"

From: victor.luchangco@sun.com
Date: Fri Oct 31 2003 - 18:19:27 EST


Hi Jason,

I went back and re-read your email from last Friday, where you said:

> I mean r1=r2=1 is _equally_ not bizarre in both cases if we adopt a
> slightly different mentality, i.e. if we don't need to strictly
> follow the "race-free (under SC) programs are SC" rule.

It seems that you want to weaken the definition of race-free, so that
some programs will be considered race-free that are not currently so
considered. I didn't address this issue specifically.

I agree that there exists a perspective that makes the r1=r2=1 result
in those programs "not bizarre". But most programmers don't have that
perspective, and it's not effective to legislate what perspective
programmers must have. I would prefer a different base model than SC,
but, as I said, there isn't any other model that has widespread
acceptance. Even for the JMM, there is no expectation that it will be
widely understood. Instead, we expect that most programmers will only
understand SC, and that will be sufficient for them to program in
Java, because they will write race-free programs. If we had a perfect
(or reasonable conservative) race detector, we wouldn't even bother
telling most programmers the rest of the details. But since we don't,
we want to give them some support to debug programs into which they
inadvertantly insert races. (Personally, I think we should strengthen
the JMM only to provide "security"--not to help debugging--but others
disagree.)

In any case, I'm not sure what new definition of race-free you are
proposing, so it's hard to argue for or against a hypothetical model.

> I think the original reason to define race-freedom using SC might be
> trying to avoid the circularity of JMM specification and race
> definition

I don't think this is the main reason to define race-freedom in terms
of SC. The main reason stems from the belief that SC is the only
model that most programmers understand. If writing correct programs
depends on understanding the definition of races, then that definition
had better be in terms of models programmers understand, leaving SC as
the only choice.

I think you are really questioning whether that belief--that SC is the
only memory model most programmers understand--is correct. This is an
empirical question, one that I believe is easy to decide: Just ask the
programmers you know if they really understand any model other than
SC. I would be surprised if you can find any university or company
with ten people who don't study memory models that really understand
any model other than SC and per-location SC (aka coherence), unless
their company builds a computer with that memory model. Even in Sun,
most people reason about TSO (the memory model provided by SPARC) by
saying what membars need to be inserted to guarantee SC (though there
probably are ten programmers who understand TSO better than that).

                                 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