**Next message:**Bill Pugh: "JavaMemoryModel: Way forward on JSR-133"**Previous message:**Sarita Adve: "RE: JavaMemoryModel: Examples similar to tests 5 and 10"**In reply to:**Sarita Adve: "RE: JavaMemoryModel: Examples similar to tests 5 and 10"**Next in thread:**Bill Pugh: "RE: JavaMemoryModel: Examples similar to tests 5 and 10"**Reply:**Bill Pugh: "RE: JavaMemoryModel: Examples similar to tests 5 and 10"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

At 07:32 AM 1/12/2004, Sarita Adve wrote:

*>Hi Victor,
*

*>
*

*> > But according to my vague intuition, Example 1 should not have been
*

*> > allowed. Does M/P really allow it? I'm not comfortable
*

*> > enough with the
*

*> > model--in fact, I still find the M/P specification ambiguous in some
*

*> > places--to say for sure. The reason I'm not sure is that if you
*

*> > restrict the non-forbidden executions to be those in which
*

*> > T2's read of
*

*> > Z returns 2, then don't we then always get that r2 = 2?
*

*>
*

*>The forbidden execution part allows us to say that if Z=2 happens first, we
*

*>can forbid r2 returning 0. However, it does not let us forbid r2 from
*

*>returning 1. More precisely,
*

*>we forbid the following prefixes:
*

*>
*

*>Prefix 1: Z=2; r2=Z==0
*

*>Prefix 2: Z=2; r1=X==0; r2=Z==0
*

*>
*

*>That is, forbid all prefixes that start with Z=2 and read r2=Z==0 after
*

*>that. Now we consider an execution where Z=2 executes first. Then X=1 is
*

*>guaranteed to execute and so can execute presciently and we can have the
*

*>above execution.
*

The form of this argument seems to be something like:

When we reach r1=X in T1 we can make certain assumptions about the state of

the world that will result in an execution in which we will read 1. Because

of that the compiler can presciently assume that X will have the value 1

without violating "not out of thin air". The kind of assumptions we can

make are "forbidden prefix".

My question is: what privileges the "forbidden prefix" form of the

assumptions? Why shouldn't the compiler be allowed to make whatever

assumptions it wants about the state of the other threads when it decides

to force a prescient read?

If we think compilers ought to be allowed this kind of reasoning then we

should state the principal and leave the details to the compiler authors to

work out.

I hypothesize that if we allow the compiler to make arbitrary assumptions

about the state of the other threads subject only to their being consistent

with what has already happened in the current thread then we end up with

something like SC-.

*>In example 2, we cannot create such a set of forbidden prefixes because by
*

*>the time we come to Z=2, we have already committed to reading 1 for Y. But
*

*>why should that matter?
*

*>
*

*>It just occurs to me that if we replace "prefixes" with "subsets" of
*

*>forbidden accesses, we may be able to weaken M/P. I need to think about this
*

*>some more and discuss off-line with Bill/Jeremy.
*

You're toying with another kind of assumption that you want to allow

compilers to make. But again what privileges this new kind of assumption?

*> > (I do think it is important that any
*

*> > model we propose have a clear formal specification, so that
*

*> > such proofs
*

*> > are possible. The M/P model needs a bit more work on this
*

*> > front. I also
*

*> > think "conceptual integrity" is important, but neither SC-
*

*> > nor M/P has,
*

*> > in my opinion, the clear upper hand on this criterion.)
*

*>
*

*>Can you elaborate on what you mean by "conceptual integrity?"
*

*>
*

*>Sarita
*

*>
*

*>
*

*>-------------------------------
*

*>JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
*

-------------------------------

JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel

**Next message:**Bill Pugh: "JavaMemoryModel: Way forward on JSR-133"**Previous message:**Sarita Adve: "RE: JavaMemoryModel: Examples similar to tests 5 and 10"**In reply to:**Sarita Adve: "RE: JavaMemoryModel: Examples similar to tests 5 and 10"**Next in thread:**Bill Pugh: "RE: JavaMemoryModel: Examples similar to tests 5 and 10"**Reply:**Bill Pugh: "RE: JavaMemoryModel: Examples similar to tests 5 and 10"**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:56 EDT
*