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