Here are some comments related to the recent discussions.
1. Sarita's proposal.
I like the presentation in Sarita's jmm.pdf. It is easy to follow and yet
it seems to have teeth, that is, there is not a big gap between the
intuitive explanation and the formal model. (Of course, cutting my teeth on
CnC undoubtedly made Sarita's presentation easier to follow. Softened me up
so to speak.)
I also like Sarita's code samples better than the more trivial ones that are
presented *first* in Bill and Jeremy's presentation. The presence of a
conditional statement and a curly brace or two evoke the idea of "program"
whereas the more trivial examples do not.
Btw, in looking at cnc-in-sc-.pdf, I question the definition of
happens-before:
I hb J if (1) I is before J [by program order].
Should this be [within the execution trace]?
2. Understandability of CnC
Victor writes:
Like Eliot, I found both A and B rather hard to understand. Some of the
difficulty may be due to the subtlety of the notion you are trying to
describe, but it is at least partly due to the way in which you are
describing it. Also like Eliot, I worry that a model that is too hard for
most people to understand (at least those who don't do research on memory
models) will not be useful.
Sarita writes:
... throughout this effort, my main complaint has been that their formalisms
and models lack intuition for why they are what they are. Hence, it has been
difficult to assess whether their model really does what it is meant to do
(since I don't know what it is meant to do). Unfortunately, I felt the same
with this version. [...] I would like to add to your goals: a minimal
condition for accepting a spec (parts D and E in your message) should be
that it should be understandable to at least the people who have worked on
this topic for some years.
=> I agree with all of the above. I don't buy the notion that an intuitive
understanding of consistency and causality provides enough detail for many
programmers. A JavaWorld article that does not at least touch on all of the
complexities of the model is of little use to me.
Bill writes:
An additional advantage is that we can provide an informal but complete
description of the core memory model in a manner appropriate for something
like JavaWorld or the next edition of Doug's book, and that many programmers
could develop an accurate mental model of the JMM, without needing to look
at any formal definitions.
=> I disagree. I'm still hoping for that informal description of CnC that
contains enough detail to satisfy the needs of programmers (like myself).
3. Causality tests
I (and Assaf, too?) have a problem with test #1.
Causality test case 1:
Initially, x = y = 0
Thread 1:
r1 = x
if r1 >= 0
y = 1
Thread 2:
r2 = y
x = r2
Behavior in question: r1 == r2 == 1
I can see how a static inter-thread analysis could decide that y must be 1,
and hence cause x to be 1, but this violates my intuitive understanding of
"cause". In my view, the only thing causing this strange result is the
compiler itself -- but aren't the rules of causality supposed to prevent the
compiler from manufacturing causes?
While I may not be upset by the result in question (I'd have to think about
it more), this is an example of where my intuitive notion of cause did not
serve me well. I find no "cause" for this result that can be traced back to
the program. The compiler did it -- in which case I might be better served
by a model that did not appropriate the word "cause" in this way.
-- Joe Bowbeer------------------------------- JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:48 EDT