Under a different subject,
At 12:22 PM 17/03/2004 -0500, Bill Pugh wrote:
>On Mar 16, 2004, at 9:22 PM, Sylvia Else wrote:
>
>> At 08:01 PM 16/03/2004 -0500, Bill Pugh wrote:
>>
>>
>>We put U7 in the document because we weren't thrilled with it.
>>
>> It is pretty horrible, but after all the code is not correctly
>> synchronized. It did though raise another question in my mind. Is it
>> true that all correctly synchronized code fragments will show SC behaviour?
>>
>> Sylvia
>
>That depends on what your definition of "fragment" is.
>
>If a fragment is a set of threads that definitely has no interaction
>with any other threads, that this property is clearly so.
>
>I suspect we have the Isolation principle I postulated before, but
>we haven't done a proof of it.
In more concrete terms, my concern was along these lines:
int x;
void userMethod()
{
/* Interact with another thread to perform a data race involving x. */
...
/* Invoke privileged method passing x. */
System.privilegedMethod(x);
}
In this case, the implementation if privilegedMethod is a code fragment. If
the race in userMethod() can leak into the execution of privileged method
so that it is no longer SC, then the SC reasoning used by the developer of
privilegedMethod() is no longer valid, and the developer's proof that it is
safe does not stand up.
Since method calling is not special in the model, it seems to me that we do
need a proof that executions of correctly synchronized code fragments are SC.
Sylvia.
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:01:00 EDT