Doug (and others),
[A summary with 5 points appears at the end, for those too busy to read the
full message.]
Thanks very much for the succinct summary, it helps me to better understand
our goals here.
I would like to add to your goals: a minimal condition for accepting a spec
(parts D and E in your message) should be that it should be understandable
to at least the people who have worked on this topic for some years.
Otherwise, we will have undermined this whole process (that Bill has put
together in the most exemplary way). Unfortunately, I believe that CnC does
not satisfy this minimal condition yet, so I believe it will be a mistake to
adopt it at this point (deadline constraints notwithstanding).
The only paragraph in your message that favors CnC is:
> 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.
Again, what I am pitching here is my framework. I will make SC- as strong as
my understanding of CnC. I will put that document up in just a few hours (I
have already explained how to do it), and it will still be less than a page.
This will allow us to take the happens-before consistency issue and all the
examples that Bill has brought up so far out of the equation. It will not
allow us to do a formal proof that SC- = CnC, because I (and I suspect
others) cannot understand CnC well enough for that yet.
I feel that your statement "This is no accident. Many of the details were
driven by these kinds of use cases over the past five years." is unfair in
favoring CnC. I believe one (by no means the only) significant part of the
reason it is no accident that CnC is somewhat acceptable right now is
because I've been pushing Bill hard on this. For example, last summer, Bill
and Jeremy had declared the model done, without even defining causal loops.
I had to argue really hard and (I believe) succeeded in changing their minds
only when I discovered (after a lot of work) a smoking gun example where a
realistic compiler optimization gave unacceptable results for their model.
Similar instances occurred before last summer as well. I could spend the
rest of the week looking for a smoking gun with CnC, but I feel I don't need
to any more because I believe now we have a good alternative (of which Bill
and Jeremy are as much a part). The reason CnC is where it is is no accident
- it involves a lot of sweat on my part, and of course more on the part of
Bill and Jeremy. And similarly the reason SC- is where it is is no accident
either - it involves a lot of sweat on Bill and Jeremy's part, and they
share the credit for it with me. The point of this paragraph is:
Given the above history, I don't see how one can accept at face value that
CnC will be more desirable than SC- (with the additions I will put up).
>
> 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.
Thanks for noting this. If you agree with my previous paragraph, this
further weakens the argument for "CnC as it is."
> 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??
I am happy to chase perfection, if Bill/Jeremy get CnC to a point where we
can do proofs. If CnC isn't understandable, I don't see how we can adopt it,
without seriously undermining this whole process of the last four years.
So, here is the bottomline the way I see it -
(1) I am happy to put the time to prove SC- (or a derivative) is
semantically the same as CnC so we can all be confident of making the right
choice. But this requires Bill and Jeremy to make CnC more understandable
(enough to do the equivalence proof), which I believe is necessary anyway. I
am also happy to devote more time to work with Bill and Jeremy on CnC.
However, with all my other priorities, I can justify spending more serious
time on this effort only if all three of us are given credit for the
eventual model that is referenced, and we continue to view this as a
cooperative rather than competitive effort.
(2) If people want to accept "CnC as it is" (for what seems to me to be on
faith), then I would appreciate messages from the expert group and others on
the mailing list to that effect ASAP, so I can stop spending more of my time
on a foregone conclusion.
(3) Conversely, if others feel that there is still value in working towards
convergence between CnC and SC- before making the final decision,
*****PLEASE VOICE YOUR OPINION NOW.********
(4) If Bill and Jeremy get CnC to a point where I can in all honesty
understand it well enough to do equivalence proofs, and yet cannot close the
gap with SC- within two of my working days, I will vote for the revised CnC
due to the deadline constraint. Unfortunately, I will not be able to vote in
favor of "CnC as it is," in good conscience (in which case, I can abstain or
step down from the EC if needed). I also just read Victor's suggestion,
which may possibly be an option.
(5) Regardless, I will put up a document shortly, with SC- beefed up with
everything that I understand right now about CnC.
Again, Bill and Jeremy have put in a tremendous effort for which I have the
deepest regard. I do not wish to take away from them in any way whatsoever,
I just think we have a little more ways to go.
Sarita
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:48 EDT