Re: JavaMemoryModel: Why CnC

From: Doug Lea (dl@cs.oswego.edu)
Date: Tue Jul 29 2003 - 08:47:51 EDT


I've been slaving away at JSR-166 stuff (with similar, scarily close
deadlines as JSR-133), so haven't been paying enough attention to
discussions over the past week or so, but here's my take on it.

There are several levels of intuitiveness, understandaiblity, and
simplicity of JSR-133, that you can think of in terms of five
different documents:

A. The quick read, for all programmers:
  1. Lock/unlock, volatile read/write, and thread-start/thread-terminate
     all have the straightforward semantics we've been advocating for years.
  2. Final fields are constant unless you expose "this" in constructor.
  3. Races not covered by above lead to surprising outcomes, but
     minimally, maintain type safety.

B. FAQs/Guides for programmers dealing with common kinds of races
  1. Double-check
  2. Ordering of non-volatile read/write wrt locks and volatiles
  3. ... a few more along these lines
  4. Directions for decoding spec/model for other cases, under the
     assumption that most programmers never will.

C. FAQs/Guides for compiler writers
  As in my "Cookbook" http://gee.cs.oswego.edu/dl/jmm/cookbook.html --
  with a similar tone as (A/B): Concise descriptions of
  the miminally sufficient steps to comply, coverage of common
  special cases, and refs to spec/model for those few (if any) who will need
  to read them.

D. The JLS spec
  i.e., replacement for current JLS chapter 17, that might or might not
  contain full description of underlying model.
  
E. The underlying formal model
  i.e., the outcome of the current discussion

For most of us, parts A, B, and C have always been the most important,
because they have the most impact, even though none of them are
officially part of JSR-133 spec, which consists only part D.

I believe that Part A would be the same under both CnC (Bill & Jeremy)
and SC- (Sarita).

Parts B and C would differ across CnC vs SC- only in small ways, but
as far as I can see, the places where they differ all favor CnC in
terms of strength of guidance and desirability of outcomes. This is no
accident. Many of the details were driven by these kinds of use cases
over the past five years.

Part E (and D, to the extent that it contains full model) would of
course differ most, and I suspect that Sarita is right that SC- is a
more understandable basis for a spec and might be a better basis for
automated reasoning about programs.

In a perfect world, some variant of SC- and CnC would prove to be
equivalent. We might not have time now to chase perfection though. In
which case, it looks like we should stick to CnC for JSR-133 spec.
Or maybe there is a way to write (D) JLS-spec that has the effect
of delaying commitment to formal model??

-Doug
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



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