Hi,
I'm also going through the latest draft. I have been reading various
documents for a while now, and exploring the archive. I'm not real happy
with my comprehension of the current semantics, so i've tried to figure
out what i don't understand in terms of questions below.
BTW, I thought one of the goals was to produce a *simpler*, *more
understandable* semantics. I'm not sure this goal will be achieved as the
semantics are described in this draft---proving a trace correct or
incorrect in the final semantics is definitely not going to be easy in
general. Perhaps this complicated model is inevitable---on to the
questions then:
- the basic model assumes a very stripped down version of statements, but
does not seem to be the same as bytecode. Are the semantics of evaluation
etc in larger java expressions well-defined enough that your program model
can be umambiguously derived (with respect to memory model orderings) from
a real java program with larger stmts/expressions? Doesn't seem unlikely
offhand, but these issues are subtle so i'd like to see an argument.
- p.4 typo in figure 1 (as described in the post i'm replying to)
- does figure 9. have a typo (rather 2 typos)? "<co" is a binary
operator, so should that be ...\{a' <_{co} a\}... ? Otherwise i just
don't understand your notation.
- When i try and understand figure 9, i get numerous 'semantic parse
errors' due to inconsistent typing clues:
-- You keep using executions as sets, but that is not how they are
defined; they are defined on page 2 as an interleaving of actions
according to a partial order (this is vague too, but i can live with
that). An ordering is of course a set of pairs, but i couldn't seem to
get that to work as what you mean by sets; i suspect you mean just the
elements of E without order. You need an operator to convert execution
traces into sets (or define executions as sets and have the ordering
separate) if you want to test membership or subsets. Without this it is
not clear to me if the set(?) "{a' e E| a' <co}" (in as much as i can
parse that) is meant to be an ordered subsequence of E or a(n unordered)
set. This is not helped by the use of curly braces for ordered sets.
I'd appreciate set notation ("{}") for sets and vector notation ("<>")
for vectors (eg causal order list should be a vector).
-- i'm a bit unclear on what "allowed in/by" means. The def at the end of
page 3 is with respect to reads only. Writes are always 'allowed,' but
only if they appear in the trace, correct?
-- i would've worked through this much faster had the example(s) in
section 4.2 been explained fully. You may want to consider describing
first E, the causal order (this you do), and then exactly which are the
elements of valid_0 relevant to each action in E and how each such E'
allows the indicated action. I've assumed you're building just valid_1
from valid_0 here---is this true?
-- generally, i'm unsure of the impact of building valid_(k+1) sets beyond
k=0. Are there any insights that would explain what happens to valid_(k+1)
as k grows? If we're always just building valid_1 from valid_0 then i
think i can see why the valid_1 traces would be sensible, but it is less
clear why building e.g. valid_1000 from valid_999 cannot produce very
strange results. I suppose they will all be consistent by construction
... is there anything else to say about them? Do we reach a fixed point?
-- i don't think i fully understand the problem being handled by section
5. Is this an example of building valid_2 from valid_1 by only using a
partial trace in constructing valid_1 from valid_0? A step-step
explanation would help. Actually, i'd like to see a lot more discussion
of the whole issue of partial traces (pun unintended)...
- top of p.13. Figure reference is broken. You should've seen a
complaint about that in latex.
- p.13 again; is the reference to figure 14 correct? Seems like you're
referring to the program, not the set of outcomes (ie should be figure
12-a).
- p.13 yet again, second last paragraph of section 6.0. redundant
"prohibited".
- the issue of prohibited traces seems like a hack. I do see how it
solves the problem, but why based on a single read? I also do not
understand the requirement: "E' is an alternate execution trace that
contains r and the causal trace r has in E, but returns a different value
for r." That is:
-- we're talking about a variable read for r---that is, a static read
action, and not a runtime action, right? (otherwise i don't see how it can
return a different value---are not runtime actions associated with their
values read?). What does it mean for E' to "contain r"---just that we
execute that static stmt as some point? More importantly, what does it
mean that E' contains the causal trace r has in E. Do you mean any one of
the causal sequences of E leading to any particular runtime execution of r
exists as a subsequence of a (any?) causal order for E'? It would probably
help a lot to work through your example in detail, showing the actual
<E,r,E'> triples (not just their results in terms of i,j,k).
- in Figure 15, the behaviour of (i,j,k) is said to be not in valid_0 for
a result of (1,0,0) and in valid_0 for (0,1,0). But there is no
sequentially consistent execution that would produce i=0 and j=1. Is this
another typo ((1,0,0) and (0,1,0) roles reversed)? Same problem in figure
14. As well, why did you pick a trace leading to (0,0,0) as a replacement
in these cases?
- The hand-waving in the very last sentence of 6.1 is not convincing. Can
you explain exactly how the read of 2 in h2 is validated, in very explicit
terms of valid sets and elements? I don't see any valid seq. cons.
execution that contains h1 (reads 2) as an action. Is this done by
constructing valid_2 after valid_1? I'm confused here; perhaps there's
something basic i've misunderstood.
- figure 16 should refer to theorem 7.2 i think and not theorem 1 (but
i've still to go through the theorems in detail).
- a more general point: i can imagine proving a trace E is in some valid
set valid_k, and from a formula similar to figure 9 prove that therefore E
is in valid_(k+i) i>0, and thus valid. But in the revised version of that
formula (figure 13), valid_(k+1) is not a trivial superset of valid_k
anymore due to the removal of prohibited executions. Proving that a
particular E gets into valid_k and is in every valid_(k+i) i>0 is
therefore not so obviously trivial. Is this intended? Surely this makes
figuring out whether a trace is valid somewhat difficult?
Thanks for any response(s). Sorry for the occasional acerbic tone in the
questions; it's been a frustrating read. :)
ttfn,
clark
clump@cs.mcgill.ca
On Sun, 9 Feb 2003, Jeremy Manson wrote:
> > Could someone kindlly tell me:
> >
> > What do the variables a and b have to do with anything? Where
> > do b1 and b2 come from?
>
> Slight typo there: that should be x == y == false, not a == b == false.
> b1 and b2 are local boolean variables.
>
> You will find us doing that a lot: we tend not to declare the local
> variables.
>
> I hope that helps. The basic idea is that x == true and y == false cannot
> happen. Also, by the same principle, x == false and y == true cannot
> happen, and the point is made elsewhere that x == y == true cannot happen.
>
> x == false and y == true (or vice versa) cannot happen, formally speaking,
> because that is not what we call a "consistent" execution. The reads are
> not "allowed", by our definition of "allowed" (which is right near the
> figure).
>
> x == true and y == true cannot happen for a different reason: i.e., the
> writes cause each other to happen. We disallow this sort of causality
> loop.
>
> Jeremy
> -------------------------------
> 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:42 EDT