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

From: Sylvia Else (
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
>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.


JavaMemoryModel mailing list -

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