**Next message:**Vijay Saraswat: "JavaMemoryModel: The Ucases"**Previous message:**Bill Pugh: "JavaMemoryModel: IMPORTANT: New Unified JMM formalism, $100 reward for any flaws"**In reply to:**Bill Pugh: "JavaMemoryModel: IMPORTANT: New Unified JMM formalism, $100 reward for any flaws"**Next in thread:**Bill Pugh: "JavaMemoryModel: Important typo fix in unified model description: U6 is not allowed"**Reply:**Bill Pugh: "JavaMemoryModel: Important typo fix in unified model description: U6 is not allowed"**Reply:**Bill Pugh: "Re: JavaMemoryModel: IMPORTANT: New Unified JMM formalism, $100 reward for any flaws"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

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

**Next message:**Vijay Saraswat: "JavaMemoryModel: The Ucases"**Previous message:**Bill Pugh: "JavaMemoryModel: IMPORTANT: New Unified JMM formalism, $100 reward for any flaws"**In reply to:**Bill Pugh: "JavaMemoryModel: IMPORTANT: New Unified JMM formalism, $100 reward for any flaws"**Next in thread:**Bill Pugh: "JavaMemoryModel: Important typo fix in unified model description: U6 is not allowed"**Reply:**Bill Pugh: "JavaMemoryModel: Important typo fix in unified model description: U6 is not allowed"**Reply:**Bill Pugh: "Re: JavaMemoryModel: IMPORTANT: New Unified JMM formalism, $100 reward for any flaws"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

*
This archive was generated by hypermail 2b29
: Thu Oct 13 2005 - 07:00:59 EDT
*