Re: JavaMemoryModel: Semantics musings

From: Bill Pugh (pugh@cs.umd.edu)
Date: Tue Sep 25 2001 - 11:36:29 EDT


At 11:04 AM -0700 9/24/01, Keith Randall wrote:
>
> A clarifying question about this semantics - consider the following
>program fragment:
>
>r1 = x
>r2 = x
>if (r1 == r2)
> y = 42
>
>Is "y = 42" allowed to be reordered across the control-flow boundary?
>On first reading, I thought it couldn't, because r1 and r2 may contain
>different values, depending on the behavior of other threads.
>However, in an implementation I'm always allowed to choose a subset of
>behaviors, and let me choose the subset that does both "r1 = x" and
>"r2 = x" atomically (otherwise known as redundant load elimination).
>This optimization requires no knowledge of the existence of other
>threads or their behavior. Am I now allowed to reorder "y = 42"
>across the control flow boundary?

I believe we need to allow for this, other we loose compositionality
of transformations.

>
>More generally, do I need to show that the write will occur in any
>execution, over ALL possible interleavings, or only the interleavings
>that might actually occur?

Doing this in the semantics without creating any circularities in the
definition is a little tricky, but is what we have to do.

For example, consider:

Initially, x = y = 0

Thread 1:
   if x != 0
     y = 1

Thread 2:
   if y != 0
     x = 1

You must be careful to not allow this program to result in x = 1 and y = 1.

        Bill
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



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