Unfortunately, this message went out prematurely. The simplification of
(3) below isn't quite enough, and I need to think some more to see
what's possible. More later,
Sarita
> -----Original Message-----
> From: owner-javamemorymodel@cs.umd.edu
> [mailto:owner-javamemorymodel@cs.umd.edu] On Behalf Of Sarita Adve
> Sent: Tuesday, July 30, 2002 7:04 PM
> To: javamemorymodel@cs.umd.edu; jsr-133-eg@jcp.org
> Subject: JavaMemoryModel: Another approach
>
>
> Based on points raised in my message earlier today, I attach
> a one page alternative model (.doc and .pdf). I have
> deliberately tried to use a flow analogous to that of the new
> Manson/Pugh model to underscore that Bill and I are
> converging (although not there yet). I would appreciate
> feedback. The rest of this message is
> motivation/justification for the attached model (vs.
> Manson/Pugh) and the difference from my previous proposal.
> You do not need to read this to understand the attached model.
>
> Sarita
>
>
> ----------------------------------------------------------------
>
> The attached model vs. Manson/Pugh and my previous proposal:
>
> As in my earlier message today, I don't like the idea of
> having an informal accompaniment to the spec on a matter that
> clearly pertains to the memory model (as Bill proposes).
> Hence, the quest for another approach.
>
> I have also said before that I think the model needs to be
> tied more directly to the intuition for what's necessary and
> sufficient. A few months ago, I tried to articulate this
> intuition and its formalization, based on several discussions
> with Bill. The intuitive requirements then seemed to be:
> (1) SC for correctly synchronized programs, (2)
> not-out-of-thin-air values for reads, and (3) that the effect
> of a data race be contained within the program areas that
> were directly impacted by the data race.
>
> After reading the new M/P document, I believe that we may
> want only the
> following: (1) and (2) as before, but (3) should simply be:
> values read should be consistent with happens-before. This
> simplifies my previous proposal considerably, resulting in
> the attached document.
>
> So as feedback, I would particularly like to know if you
> think this revised
> (3) is reasonable or if it should be stronger. Regardless of
> what approach we use, I think it is important to be able to
> articulate the intuitive requirement that we are after.
>
> Finally, as I said in my message this morning, for most
> memory models, it is complicated to derive a (correct) proof
> to show that correctly synchronized programs get SC. With the
> attached style, such a proof is not needed since part of the
> *definition* of the model is that correctly synchronized
> programs will give SC.
>
> Sarita
>
> --------------------------------------------------------------
> ---------
> Sarita Adve
> Associate Professor
> Department of Computer Science Email:
> sadve@cs.uiuc.edu
> University of Illinois at Urbana-Champaign Office: 3302 DCL
> 1304 West Springfield Avenue Phone: 217-333-8461
> Urbana, IL 61801-2987 Fax: 217-333-3501
> WWW URL: http://www.cs.uiuc.edu/~sadve
> --------------------------------------------------------------
> ---------
>
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:40 EDT