JavaMemoryModel: Let them write race-free code (was: The property of "race-free implies SC")

From: Joseph Bowbeer (jozart@csi.com)
Date: Tue Nov 11 2003 - 01:00:33 EST


Victor Luchango writes:

"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 inadvertently insert
races. (Personally, I think we should strengthen the JMM only to provide
"security"--not to help debugging--but others disagree.)"

I can see how this view could be appealing to JVM implementers, and I'm not
saying that it's wrong, but I am concerned about what programmers in the
trenches will think if the EG adopts this as their party line.

I'm afraid that it may come across as elitist. I also find it unappealing
because it contradicts the transparency that characterizes the rest of the
Java language.

Furthermore, it ignores the impact of the new JMM on the existing code base,
which has been developed over the past seven years. (This existing code has
been tuned to the de facto JMM as it is loosely defined by the existing
JVMs -- not by the existing JLS.)

The preface to the community review draft of the JMM states: "The proposed
core semantics should not cause issues for existing JVM implementations".
What, however, can we tell the users and maintainers of the existing code
base about the impact of the proposed semantics? They will also be
interested in understanding the potential impact of a new JMM. How can they
do this if they can't understand it? How can they do this if they're unable
to tell if their code is race-free or not?

To complicate matters, even for programmers writing new code, I don't
believe the threading model of AWT has ever been defined clearly enough for
anyone to know whether a sizeable GUI application is completely race-free or
not. Similarly, while Swing's single-threaded subsystem would appear to
simplify the task of writing race-free programs, its interactions with AWT,
and the places where its own implementation violates its own rules(*),
leaves areas of uncertainty in many applications. (For most GUI developers,
avoiding deadlock is a much more pressing issue than avoiding races.)

I don't have any alternatives to offer, and in some ways I find consolation
in the fact that there *is* no practical tool for detecting races: if a tool
can't do it then the compilers probably can't either...

But I do want to caution the EG against adopting a position that may be
perceived as out of touch with reality. And I want to encourage the EG to
continue in their efforts to make the entire JMM specification
understandable to everyone.

--
Joe Bowbeer

(*) Namely: asynch updates in AbstractDocument

----- Original Message ----- From: <victor.luchangco@sun.com> To: "Yue Yang" <yyang@cs.utah.edu> Sent: Friday, October 31, 2003 3:19 PM Subject: Re: JavaMemoryModel: The property of "race-free implies SC"

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:53 EDT