Sylvia Else wrote:
> Under a different subject,
>
> 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.
Hello --
I am not sure what you are asking for makes sense. If there is a data
race involving x, and x is passed to some privilegedMethod, then any
reads done in that code are going to see the multiple uncoordinated
writes on x. The semantics cannot guarantee, for instance, that two
reads will return the same value (even if the environment is no longer
writing on x).
Thus if the author of privilegedMethod wants to do SC reasoning in the
body of the code he can do that only under the assumption that the data
items being read or written to by the body of the code (directly or
indirectly) are not involved in any races with anything that could
potentially run in the environment. Without type support (e.g. declare
the variable volatile) it would be very hard to establish that
pre-condition.
Hmm... interesting. Perhaps the type system should be extended so that a
programmer can specify that a method argument must be volatile.
This does bring up the interesting thought, though, whether there is
some operation that can be defined on x to resolve past races. I am
thinking of something like a "globally performed store" in release
consistency. Or, in the current context, an operator that dynamically
converts a normal location into a volatile location. I suspect this can
be supported in the semantics, but this might not be a good idea from
the viewpoint of programming practice.
Best,
Vijay
-------------------------------
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