The pitch I would like to make to you all is to adopt the basic SC-
intuition and framework in my "the intuition IS the model" message. That is,
reason with SC like semantics as much as possible, with the only non-SC
discontinuity occurring at data races. These discontinuities are expressed
as strange values read and written by these data races.
The remaining question then is "how strange should these discontinuous
values get?":
I am really not the most qualified to answer this, so I present a
preference, with several options. One of these options could very well
result in CnC and may well be the final choice of this community, but I feel
my framework allows us to make this choice in a more informed way, with more
intuition.
First, my preference:
Based on whatever little past experience I have with this topic - weaker is
better, because there is no way to predict what optimizations people will
think of in the future. Of course, the problem is that the level of weakness
has to be balanced against intuition for the users of the model.
I believe the SC- model I have presented so far provides a reasonable
balance. It is not the weakest possible. But making it weaker will make the
wording (not necessarily the intuition) more complex. It is not the
strongest possible either, as Bill's examples today have shown.
But it can be made stronger easily. I think the race read discontinuity is
the key place to strengthen if you all want that; the write discontinuity is
ok.
So, the only phrase to change in the formal model is the one after the ****
below:
If M is a read, it can return a value written by *****any conflicting write
in E.
Here are some things we can add to make this closer to CnC (any combination
can be added):
If M is a read, it can return a value written by a conflicting write W in E
such that:
(1) the write W should also occur in the execution we are generating and
write the same value (this will prohibit Bill's example 1 and 2a, if you all
do want to prohibit those examples).
(2) W should not be ordered after M by happens-before in E,
(3) there should be no write W', such that W happens-before W'
happens-before M in E,
Etc.
I have some reasonable ideas for weakening the model too (e.g., to allow
example 2 from Bill), but I think it is not yet time for that!
In conclusion, I want to add that the fact that I think I can make SC- come
close to CnC is not a coincidence. It is because I have drawn a *LOT* from
my discussions with Bill/Jeremy, to determine the right balance between
weakness and intuition described above. The previous weak versions I used
were shot down by Bill/Jeremy for good reason and reflect a tremendous
effort.
Sarita
-----Original Message-----
From: Sarita Adve [mailto:sadve@cs.uiuc.edu]
Sent: Monday, July 28, 2003 7:29 PM
To: 'javamemorymodel@cs.umd.edu'
Subject: The Intuition Is the Model - the full model is in this email!
It occurred to me that the intuitive description I sent earlier IS the
model. I don't need all the formalism in my document, other than the
straightforward, standard definition of a data race. Below, I have reworded
the intuition I sent earlier to make it more complete.
This is it, this is the formal Java model I propose!
Sarita
----------------------------------------------------------------
The SC- model := SC - discontinuities at data races
----------------------------------------------------------------
Executing in an SC fashion means: instructions execute one at a time,
instructions of each thread execute in program order, and a read returns the
value of the last conflicting write. (A read and write conflict if both are
to the same location.)
With SC-, the execution proceeds in an SC fashion (one at a time, in program
order), until a memory access M occurs that forms a data race either with
(1) a write that has already occurred or (2) a write that could occur if we
continued to execute in an SC fashion. Call this possible execution (where M
forms a data race) as E. SC- allows the following non-SC discontinuity at M.
If M is a read, it can return a value written by any conflicting write in E.
If M is a write, then M can deposit two values in memory - its own value and
the value of the write it races with in E. The impact of this is that a
subsequent read could see the value of either write (until a later non-race
conflicting write occurs).
However, the above discontinuities are allowed only if the execution we are
generating eventually produces some write that writes the discontinuous
non-SC value read or written by M, to the same location as M.
After the above non-SC discontinuity at M, the execution again proceeds in
an SC fashion - instructions execute one at a time and in program order,
with a read returning a value from the last conflicting write - until the
next data race discontinuity, which is handled as above.
----------------------------------------------------------------
P.S. We can strengthen or weaken the discontinuities if we like - this is a
decision the community should make. I will describe this in the next
message.
-------------------------------
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