RE: JavaMemoryModel: Community Review Draft updated

From: Sarita Adve (sadve@cs.uiuc.edu)
Date: Wed Aug 06 2003 - 17:55:52 EDT


Bill and Jeremy,

Unfortunately, I couldn't get to the document until about an hour ago. I
am not done yet, but since I just saw this message, I thought I would
send my most important comments so far, and take a breather on this
myself. I understand you may not be able to incorporate these for the
community review.

- First, thanks for the great work!

- I myself used to call this topic "memory model" until I was told that
this term is also used for other aspects of memory (e.g., stack/heap
locations etc.). The community has used the term "memory consistency
model" for these issues, and I'd recommend continuation of that use.

- I strongly, strongly urge you not to use the terms consistency or
causality. For this version, if you can add a footnote saying these
terms are likely to change, it will be useful to ensure that they don't
get stuck, creating confusion for perpetuity. Consistency can be
replaced with happens-before consistency. I do not have a better word
for causality yet; in my prior work, I used "control condition" for the
analogous condition, but that's not a great term either.

- Aside from the terminology issue, I will argue hard that causality is
a greatly misleading concept for what this model gives. The use of that
term also seems to lead to text that is incorrect and/or misleading in
my view. For example, in the intuition text:
Causality means that an action cannot cause itself to happen. In other
words, it must
be possible to explain how the actions in an execution occurred without
depending on
one of the actions that you are trying to explain.

The first sentence is incorrect due to test 6. The second sentence
doesn't tell me much; hopefully, most models will have such a property.
For example, a model that requires that all reads return the value 1
also satisfies the condition you lay out in that sentence, and clearly
doesn't add much value. We can have an off-line discussion of this after
we've had a chance to recover. But there are many sentences throughout
the text that are along the same lines, and I think are incorrect (e.g.,
causality is a necessary condition). Even if you argue they are not
incorrect, they could certainly be confusing and/or misleading to the
careful reader.

- The atomicity discussion on page 10 is not related to JMM issues in my
opinion, but to the use of synchronization. There is a JMM-related
atomicity issue, but that is not brought up at all in the document. This
is related to a single write not appearing atomic (usually seen through
hardware optimizations). It is related to the happens-before condition,
not causality (recall Victor's examples from a few days ago).

- The one paragraph proof at the end of Section 4 explaining why
data-race-free programs get SC seems incorrect to me. It seems to assume
that all conflicting accesses in the execution you are trying to prove
the correctness of are ordered by hb. We don't know that - only SC
executions have that property, and we are trying to prove that the
execution in SC. So there seems to be a circularity in the argument.

- I am worried this document is still too complicated, and unnecessarily
so. It's undoubtedly a great improvement over the last version, and
terrific given the time constraint. But I think we still need to work
hard in the next few weeks to simplify it as much as possible, so this
stuff can become accessible to all in the first reading. Given all the
work in the past couple of weeks, I believe that is possible.

- By the way, I still have the reservations I discussed with you in our
last conversation, but alas, haven't been able to come up with concrete
examples yet to drive home the point. In any case, I am happy with how
things have worked out given the time constraint, thanks again for the
great work!

Regards,

Sarita

> -----Original Message-----
> From: owner-javamemorymodel@cs.umd.edu
> [mailto:owner-javamemorymodel@cs.umd.edu] On Behalf Of Bill Pugh
> Sent: Wednesday, August 06, 2003 3:49 PM
> To: javamemorymodel@cs.umd.edu; jsr-133-eg@jcp.org
> Subject: JavaMemoryModel: Community Review Draft updated
>
>
> Thanks for all the reading and bug fixes. The version made available
> yesterday was a little more ragged than we had intended.
>
> We've put a new copy up. In addition to a bunch of bug fixes, this
> also included language about the uncertain status of lost
> notifications.
>
> Unless I hear otherwise from Tim, Jeremy and I are done for today,
> and this will be the version sent to community review.
>
> Everyone feel free to take a week breather on this. Jeremy and I will.
>
> Bill
> -------------------------------
> JavaMemoryModel mailing list -
> http://www.cs.umd.edu/~pugh/java/memoryModel
>

-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:50 EDT