Re: JavaMemoryModel: Updated JMM schedule and status report

From: Victor Luchangco (victor_l@theory.lcs.mit.edu)
Date: Fri Jul 25 2003 - 12:15:59 EDT


Bill and Jeremy (and others),

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. However, I realize that many other
requirements compete with simplicity, and that the model proposed is a
compromise that has been worked out through much discussion. So my
main comment here is on the presentation.

The main gripe I have with both documents is that some terms are not
defined fully. In some cases, an intuitive understanding may be
sufficient, for example in the case of an action in an execution trace
being "generated by" a statement of a program. (Formally, I assume we
should be given a mapping from actions in an execution trace to the
statement of the program that generated it.) However, it would be
good to spell out precisely what information carried by actions. Does
every read action, for example, also specify which write action it
"sees", or just the value that it reads? At first, it seems like only
the value is specified, but in that case, the definition of prescient
requires an additional function that maps each read action to the
write action it sees. Similarly, in Section 2.2.1 of A, why does the
definition of action correspondence not imply that the causal orders
in both execution traces are the same: they are the same length and
the ith element (I assume i is universally quantified, but you should
be explicit) of each is the same. Perhaps i should range over only
those indices less than or equal to the index of the actions we are
trying to show a correspondence between, though this is not what the
full semantics in Figure 1 says.

I also think the definition of valid_k in A is broken because the
execution traces in valid_k are only of length k. By definition, the
last action in the causal order can never be prescient: a prescient
action must have some action later than it in the causal order.
Perhaps you are implicitly assuming that all actions that are not
explicitly in the causal order are ordered after all actions in the
causal order. Or perhaps you just want to change the definition of
"prescient" so that an action x is prescient in an execution trace iff
some action that happens before x is not causally ordered before x or,
if x is a read action, the write action that it sees is not causally
ordered before x. Personally, I would prefer to require that the
causal order totally order all actions, and then adjust the definition
of valid_k to consider only those actions in the "k-prefix" of the
causal order.

I didn't understand the discussion on prohibited executions at all,
but it didn't seem like I was supposed to understand it. (I prefer
the approach in B where you explicitly say to ignore prohibited
executions--at least until the "Alternative Executions" section, which
I still didn't understand completely either.) Maybe the discussion in
the chapter is fuller and more understandable.

In general, I prefer B to A because it seems crisper and easier to
understand. However, (a) I read A first, which probably helped me
understand B, (b) I appreciate the formal semantics presented in
Figure 1 or A, and (c) *some* of the discussion in Section 1 of A
would probably be helpful in B.

I realize that too much formalism can get in the way of understanding,
so I'm not advocating presenting everything in a full formal semantics
with a bunch of symbols and definitions (though I do think there should
be a carefully checked formal semantics underlying everything, so any
ambiguities in the informal description can be resolved). However, I
do think those definitions that are made should be as unambiguous as
possible without the defintions that are being elided.

Finally, one "historical" note: The memory model you are calling
"consistency" (please use a different, more specific name!) is, I
believe, essentially the same as the dag-consistency model of Blumofe,
et al. (IPPS 96). (In our SPAA 98 paper, Matteo Frigo and I present a
formal "computation-centric" framework, in which we define a family of
dag-consistent models; this model is WW-dag consistency in that
family.)

                                Victor

PS. Is there a full formal semantics in the style of Figure 1 available
   for the whole memory model specification? If so, could I get a copy
   of it? (I didn't see one on the webpage, but I wasn't sure where to
   look.)
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



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