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

Date: Tue Nov 11 2003 - 16:02:12 EST

Joe (and others),

I admit I wrote my previous email to emphasize that difficulty of
understanding the details of the JMM. I agree that more tact is
desirable when making this point widely. Indeed, when I say "most
programmers", I generally include myself in this group. Even "expert"
programmers will not want to think about the intricacies of the JMM
most of the time--only when they absolutely have to. They should need
to do this about as often as they need to revert to native code. And
"non-expert" programmers should never have to do this. I'm happy to
let programmers decide for themselves whether they are experts, as
long as they realize that any reasoning about the JMM--other than "SC
for race-free programs"--is hard. There is no elitism about this: it's
hard for everyone; anyone who says different is lying.

I think the "party line" should be something like:

  The JMM guarantees SC for race-free programs, where race-free is
  defined as follows: <insert some definition that only requires an
  understanding of SC>.

  Most programs should be race-free; a race usually corresponds to a
  bug in the program. Programs with races will generally restrict
  these races to occur in tightly controlled situations, where careful
  reasoning can be done and documented (e.g., formal proofs) to show
  that the resulting code is correct. Such reasoning will necessarily
  rely on the details of the JMM, as elaborated in <wherever this is
  described>. Decades of experience in concurrent programming has
  shown that programs with races, but lacking careful proofs, almost
  always exhibit some wrong behavior, and that such behavior is often
  not uncovered even by rigorous testing.

We should also say something like:

  The details of the JMM--beyond guaranteeing SC for race-free
  programs--are complicated, and intended primarily to guarantee
  safety to protect Java programs from malicious code, and for JVM
  implementors to have an unambiguous specification of what they are
  required to implement. The proposed semantics should not cause
  problems for existing JVM implementations. [Is this true? I guess
  it depends on what you mean by "cause problems".] Rather, it is
  intended to define unambiguously the informal semantics that most
  Java programmers implicitly assumed. Unfortunately, formalizing
  this informal semantics has turned out to be complicated. Indeed,
  in some cases, various interpretations of the memory guarantees were
  inconsistent. The resulting specification is a compromise between
  simplicity, safety and implementability. For most programs, which
  are intended to be race-free, a programmer can assume SC. This
  assumption greatly simplifies reasoning about the program.

I'm sure something more succinct is possible, but that's the general
idea. No appeal to elitism is necessary to make this argument: We
would all love to have a simpler model, if it also satisfies the other
requirements (i.e., "safety"--whatever that means--and efficient
implementability). If anyone proposes a simpler model that we can
agree (hah!) is "safe enough" and can be implemented "efficiently
enough", we would adopt it in a heartbeat.

I have no practical advice for writing race-free GUIs, but it seems to
me that a threading model (or any model) that isn't defined clearly
enough to determine whether a program is race-free is a model in
serious need of fixing (or at least clarification). Of course, that
is a problem for a different JSR. :)

> 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.

This goal is laudable, but I believe unachievable. I would be surprised
if the EG can come up with a JMM specification that *anyone* (even them)
understands completely at one time. Certainly, I don't. I can reason
about the JMM by doing careful proofs that rely on only having to check
little steps at a time. I use a rough understanding of the whole model
to guide my reasoning, but I rely on the formal structure of a proof to
avoid missing cases. Unless the program is race-free.

JavaMemoryModel mailing list -

This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:53 EDT