Re: JavaMemoryModel: IMPORTANT: New Unified JMM formalism, $100 reward for any flaws

From: Vijay Saraswat (vijay@saraswat.org)
Date: Tue Mar 16 2004 - 18:12:53 EST


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