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?
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"?
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
------------------------------------------------------------
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.
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.
Best,
Vijay
-------------------------------
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