Re: JavaMemoryModel: OK, time to get moving again

From: jmanson@cs.umd.edu
Date: Mon Feb 10 2003 - 22:16:26 EST


Hello,

> 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.

I hope that I can help...

>
> 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:

This, I think, is an important point, worth dwelling on for a moment.
The level of the complication of the semantics is one of the least
important points of all of this. The most important point is that we
cover all of the informal semantics: that we enable all of the
optimizations and provide all of the necessary guarantees that we have
spent 3+ years agreeing on.

I don't think this is a particularly simple task, nor can a formal
semantics which has these properties be described simply; this is
especially true when we start to consider some of the causal loop
behaviors that we have looked at in the last year.

It does become a problem when trying to explain the memory model to people
who aren't interested in the formalization, but I think that one of the
things we can (and should) do is provide a translation layer. We need to
communicate what safe programming idioms are, and what compiler
transformations are legal.

Anyway, onward. Rereading this somewhat later, it was a lot to respond to
at once. Some of the clarifications may not be all that clarifying; if
they aren't, please tell me and I'll give it a better shot.

>
> - 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.

Well, our main point is roughly that an instruction corresponds to one JVM
opcode. A getfield, getstatic or arrayload opcode corresponds to a Read,
and a putfield, putstatic or array store corresponds to a Write. A
monitorenter is a lock, and a monitorexit is an unlock. Those are pretty
much all of the operations that affect global memory in the ways we care
about for the purposes of our semantics.

Perhaps that should be made more explicit?

> - 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.

Yes; you can read it (as it is supposed to be) in Figure 13. That's a
copy and paste error :). Thanks.

> -- 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).

Hopefully, the fix on that last typo cleared up some of this. The English
version of the requirements here would read "For every action 'a' in a
valid execution in valid_{k+1}, whenever the causal order for that action
appears in some execution in valid_k, 'a' must be allowed"

So, {a' e E | a' <_co a} is the set of actions that are a causal order for
a. If that set of actions is a subset of the set of actions that
comprises some execution E' in valid_k, then a must be be allowed in E'
(otherwise we can't validate the execution we are trying to validate).

Is the subset notation really very confusing here? Or was it the typo, or
the fact that this is just generally confusing? Or some mix?

> -- i would've worked through this much faster had the example(s) in
> section 4.2 been explained fully.
[snip]
> I've assumed you're building just valid_1 from valid_0 here---is this true?

Yes: we just need to validate the one execution trace (x == y == 1 here).
Since this execution trace occurs in valid_1, that is all we need to
construct.

> -- 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?

The intuition is that the inclusion of new execution traces may add
additional opportunities to add new traces. Consider one of our examples:

Thread 1
g2: x = a;
g3: b = 1;

Thread 2
g4: y = b;
g5: a = 1;

Happens before

Thread 3

if (x + y == 2)
  S;

Only after valid_1 can we even do what is inside S;. If there are more
reads that need to be "allowed" inside S, then they need to be done in
valid_2.

We are probably not guaranteed to reach a fixed point, as the presence of
infinite loops could cause this sort of thing to happen repeatedly.

> -- 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)...

The notion of a partial trace is something of an artifact of our model; it
is separate from the notion of the valid set. In order to validate an
execution with a new read in valid_k+1, you need to demonstrate that that
read is allowed to occur in some execution in valid_k. In the example
(which is the same as the example above), "S" is not allowed to occur in
any execution in valid_k. So we validate just enough of the execution to
allow S to occur, and then we can proceed.

This is orthogonal to the issue of the existance of valid_2...n, where we
are actually worrying about new values becoming legal for potentially
unsynchronized reads, not simply the program's being allowed to proceed.

> - p.13 yet again, second last paragraph of section 6.0. redundant
> "prohibited".

That's not really a typo: it is referring to the set of prohibited traces.
But I'll take it out, it's confusing.

> 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:

I'l try to explain this a little better in the text, but you seem to get
the drift, so I'll work on the explanation some more and punt on it here.

[re: figure 15]
> As well, why did you pick a trace leading to (0,0,0) as a replacement
> in these cases?

We didn't have to. We could just as easily picked another trace. The
point is only that there has to be an alternate trace.

> - 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.

I'm going to work on explaining this one a little, too.

> - 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?

It doesn't really make it difficult, because the full memory model is the
union of the results of this function with all legal prohibited sets,
including the empty one.

Another way of thinking about it is that prohibited sets are optional. If
a trace gets in, then there is some combination of prohibited sets that
will *not* take it out; this makes that trace legal.

I hope this response helps some. As I said, writing it all at once
probably doesn't do much for its comprehensibility, so if you have any
questions about my answers, please feel free to re-ask.

Thanks for your help and corrections!

                                        Jeremy
-------------------------------
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