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

From: Bill Pugh (pugh@cs.umd.edu)
Date: Thu Mar 18 2004 - 14:08:19 EST


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

-------------------------------
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