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
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:56 EDT