On Mar 16, 2004, at 6:12 PM, Vijay Saraswat wrote:
> Some comments on the tests.
>
> 1. Is there a reason why U4 *should be* prohibited? I understand that
> the MPS model prohibits it. The question is: why should it be
> prohibited?
No particularly reason to prohibit it. It just is prohibited by the
unified proposal.
>
> 2. I would consider a model that prohibits U4 but accepts U5 flawed,
> or at least in need of further study. Again, is there a reason why U4
> should be prohibited and U5 accepted, other than "thats what the model
> does"?
We worked hard to come up with a simple and acceptable model that would
allow arbitrary thread merging/inlining.
The only simple and acceptable one we came up with does not.
>
> Out of curiosity what does the MPS model say about the following U3a:
>
> ------------------------------------------------------------
> Test U3a
> Initially, a=b=c=d=0
>
> Thread 1 (as in Thread 1, Test U3)
>
> Thread 2:
> join Thread 1
> r2=b;
> if (r2 == 1) c=1;
>
> Thread 3:
> join Thread 2;
> r3=c;
> if (r3--1) d=1;
>
> Thread 4 (as in Thread 4, Test U3)
> Behavior in question: r1=r3==r4==1;r2==0
U3 has only 2 threads, I presume you are talking about U4 here.
The new model allows this behavior (it is essentially the same as U5).
> ------------------------------------------------------------
>
> 3. Again: Why should U6 be accepted? One should be able to understand
> the behavior of a program through a single execution, without having
> to resort to "hypothetical executions". I cannot see a single
> execution that can cause this behavior. In a single execution, since
> there is a single write on r3, either the value stored there is going
> to be 1 or 0. For the desired behavior, it must be 0. Therefore x and
> y cannot be 1, hence r1 and r2 cannot be 1.
>
> A semantics that does not support this reasoning would be very odd
> indeed.
There was a typo in the figure caption. U6 is not allowed by the new
model.
>
> 4. Same as U6. Why should this be accepted? Again, r1 can be either 1
> or 2. Lets say its 1 because that is the behavior in question. Now the
> only possible values for a read on y are 0 or 1. So r2 and r3 cannot
> be 2!
>
> As above, I would consider a semantics that supports U7 seriously
> flawed.
>
We put U7 in the document because we weren't thrilled with it.
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:59 EDT