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