Examples such as U7 are very important to understand what is going on.
If my model supported U7 I would be very worried and would be looking to
examine my approach and see if something fundamental needed to change.
Patching things up will work -- until the next problem is found. To
attain convergence and be sure of your ground, a first principles
approach is often necessary, particularly in concurrency theory where
reasoning can be very tricky.
I understand you are under a deadline. Unfortunately, deadlines cant
solve technical problems.
Here is why U7 is so bad. It essentially revives "Thin air reads". If
there is a program with a single write to a variable r1, and after the
program has terminated you observe that the value of r1 is 1, you should
be able to infer that the value written into r1 was 1. Therefore you
should get the same result if in the original program you replaced the
write to r1 with r1=1. Try that in U7 -- replace r1=x with r1=1. Now how
on earth does 2 get into y and z?
Let me formulate another principle: The Substitution Principle.
(Incidentally, I noticed in 1985 that this principle was violated by Udi
Shapiro's Concurrent Prolog and was led to formulate a synchronization
operation, the ! operators, that respected it ... and this later was
found to be the same as the synchronization construct in GHC and Parlog
and ALPS and become the basis of concurrent constraint programming. The
theoretical development that was then enabled has stood the test of time.)
In this context, here is what the principle says. Consider a program P
with a single assignment to a variable x. If this program has an
execution sequence at the end of which you can observe a value k for the
variable, then you should be able to execute the same execution sequence
for the program P' obtained from P by replacing the assignment to x by x=k.
(In the concurrent logic programming case, the principle was that if an
agent A can be executed to give as a result a subtitution theta, then
the agent theta(A) can terminate successfully, i.e. execute the same
execution sequence.)
Now if your semantics supports U7, then it must violate the Substitution
Principle. For you cannot possibly argue that the following Test case
U7a will allow the given behavior:
-----------------------------------------------------
Test case U7a
Same as U7 except that r1=x in Thread 3 is replaced by r1=1.
Behavior in question: r1=1, r2=r3=2
-----------------------------------------------------
Best,
Vijay
Sarita Adve wrote:
>Hi Vijay,
>
>Thanks very much for your comments. There aren't any typos for the other
>examples. As we said in the document, we aren't too thrilled with those
>tests. We have some ideas on how to change the model to address those tests.
>But the simple ideas we tried have failed. For the more complex ideas, we
>just haven't had the time to stress them enough yet, so they are on the back
>burner. Maybe we'll get to them tomorrow, but if you want to dive in to
>figure out changes, go right ahead.
>
>However, from our point of view, given the upcoming deadline, we feel it is
>more important to nail down a model that obeys the key golden (admittedly
>informal) properties: (1) it shouldn't prohibit reasonable optimizations,
>(2) it should provide SC for data-race-free programs, (3) it shouldn't lead
>to safety/security violations, and (4) it should be relatively simple and
>understandable.
>
>So to the extent that people have time to devote to this work before the
>deadline, we really feel it is more important to be 100% sure that the
>unified model does indeed obey the above golden properties. If we can be
>convinced that the above test results violate these properties, we will go
>full throttle on our ideas for changing the model. Again, I am not trying to
>belittle your concerns, just being pragmatic in the face of the upcoming
>deadline (we ourselves have been forced to change our original goals due to
>pragmatism, but on balance, we are quite thrilled with this new model).
>
>And we also apologize that we haven't done the best possible job motivating
>this model and really driving home its simplicity (and it really is very
>simple). But again, we are trying to do the best we can, and updating the
>documents as fast as we can.
>
>Sarita
>
>
>
>>-----Original Message-----
>>From: owner-javamemorymodel@cs.umd.edu
>>[mailto:owner-javamemorymodel@cs.umd.edu] On Behalf Of Vijay Saraswat
>>Sent: Tuesday, March 16, 2004 7:04 PM
>>To: Bill Pugh
>>Cc: javamemorymodel-cs.umd.edu; Wayne Carr
>>Subject: JavaMemoryModel: Re: Important typo fix in unified
>>model description: U6 is not allowed
>>
>>
>>What about U7 and the others? Is this a typo or do some
>>definitions in
>>the model need to change to rule this out? (I am trying to
>>figure out if
>>I should dive into the current definition of the model or
>>wait if there
>>are changes coming.)
>>
>>Bill Pugh wrote:
>>
>>
>>
>>>The unified proposal said in the caption for U6 that U6 was
>>>
>>>
>>allowed by
>>
>>
>>>the new model.
>>>
>>>U6 is _not_ allowed by the new model, as was stated
>>>
>>>
>>elsewhere in the
>>
>>
>>>document.
>>>
>>>I've updated the document on the web page.
>>>
>>>Bill
>>>
>>>
>>>
>>>
>>>
>>-------------------------------
>>JavaMemoryModel mailing list -
>>http://www.cs.umd.edu/~pugh/java/memoryModel
>>
>>
>>
>
>
>
>
>
-------------------------------
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