At 11:04 AM -0700 9/24/01, Keith Randall wrote:
> A clarifying question about this semantics - consider the following
>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
>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
if x != 0
y = 1
if y != 0
x = 1
You must be careful to not allow this program to result in x = 1 and y = 1.
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