Hello,
I am done with all that I promised in my last message - I resolved the
problem with my model and have a new document. All the i's are not dotted
yet and all the t's are not crossed, but to first order, it is done. The
document is at http://www.cs.uiuc.edu/~sadve/JMM/jmm.pdf and I would
appreciate your feedback. The outline of the document is below. You don't
have to read all sections!
(Bill has been looking closely at the model for about a day now, and so far,
no problems I believe, but he is still looking.)
Thanks!
Sarita
-------------------------------------------------
Outline of the document:
Section I motivates a memory model for Java by giving (1) a set of
high-level/intuitive programmer-centric requirements underlying the model,
(2) discussing how to formalize these requirements, (3) giving an intuitive
picture of the full model based on such a formalization, (4) describing the
advantages of a model based on such a formalization, and (5) some possible
alternatives consistent with all of the above, but that may be slightly
stronger than the formal model specified in Section II.
Section II gives the formal model based on the above motivation. Section II
is self-contained, but reading Section I beforehand will aid its
understanding.
Section III describes (actually speculates) the changes needed to Section II
to express Bill's and Jeremy's (B/J) model, but without the prohibited reads
material. It also identifies the part of the resulting spec that makes it
necessary to have something like the prohibited reads material for B/J.
Section IV shows a concrete example of an execution allowed by the model in
Section II but not by B/J.
Section V provides the intuitive/informal version of B/J's model (as
summarized by B/J) for reference.
Section VI explains my view of the problems with B/J's intuition and its
formalization, underscoring the differences between the two models.
> -----Original Message-----
> From: owner-javamemorymodel@cs.umd.edu
> [mailto:owner-javamemorymodel@cs.umd.edu] On Behalf Of Sarita Adve
> Sent: Friday, July 25, 2003 10:07 AM
> To: javamemorymodel@cs.umd.edu
> Subject: RE: JavaMemoryModel: Updated JMM schedule and status report
>
>
...
> So, the upshot of all of this is that:
> (1) Until I or someone else (other than Bill/Jeremy) can
> honestly say they
> understand B/J's model, I believe we have a problem.
> (2) So until then, I will continue to consider my approach a serious
> candidate - to formalize what I guage to be B/J's intuition in a more
> intuitive fashion and/or to present an alternative (but
> close) semantics to
> B/J (again, in what I perceive to be a more intuitive way).
> (3) Even if B/J's model is satisfactorily formalized, if I
> can resolve the
> aforementioned problem with my model, it will have the
> advantage over B/J's
> model of not requiring causality.
>
> I will wrap this up from my side one way or another by the weekend.
>
> 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:46 EDT