**Next message:**jmanson@cs.umd.edu: "Re: JavaMemoryModel: OK, time to get moving again"**Previous message:**Jeremy Manson: "Re: JavaMemoryModel: OK, time to get moving again"**In reply to:**Jeremy Manson: "Re: JavaMemoryModel: OK, time to get moving again"**Next in thread:**jmanson@cs.umd.edu: "Re: JavaMemoryModel: OK, time to get moving again"**Reply:**jmanson@cs.umd.edu: "Re: JavaMemoryModel: OK, time to get moving again"**Reply:**Jeremy Manson: "Re: JavaMemoryModel: OK, time to get moving again"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

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

**Next message:**jmanson@cs.umd.edu: "Re: JavaMemoryModel: OK, time to get moving again"**Previous message:**Jeremy Manson: "Re: JavaMemoryModel: OK, time to get moving again"**In reply to:**Jeremy Manson: "Re: JavaMemoryModel: OK, time to get moving again"**Next in thread:**jmanson@cs.umd.edu: "Re: JavaMemoryModel: OK, time to get moving again"**Reply:**jmanson@cs.umd.edu: "Re: JavaMemoryModel: OK, time to get moving again"**Reply:**Jeremy Manson: "Re: JavaMemoryModel: OK, time to get moving again"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

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