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