Re: JavaMemoryModel: Are correctly synchronized code fragment executions SC?

From: Sylvia Else (sylviae@optushome.com.au)
Date: Thu Mar 18 2004 - 16:50:18 EST


At 02:08 PM 18/03/2004 -0500, Bill Pugh wrote:

>On Mar 17, 2004, at 5:59 PM, Sylvia Else wrote:
>>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.
>
>method boundaries are invisible to the memory model.
>
>And must be so, since you want to allow inlining of methods and
>optimization across method
>boundaries.
>
>That said, method parameters are local variables and cannot be in a data race.
>
> Bill
>

This is why I didn't post an example with my original question. The issue
is not whether you can argue that the problem does not arise in a
particular instance, but whether it can be shown never to arise. Maybe it's
sufficient to say that a method that contains no data races will have an SC
execution (despite optimizations across method boundaries), but I haven't
seen that stated. The statements regarding SC executions relate to programs.

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:01 EDT