Bill Pugh <pugh@cs.umd.edu> replies to me:
> > > Example 1
> >>
> >> Initially, x = y = 0
> >>
> >> Thread 1:
> >> r1 = x
> >> if r1 >= 0
> >> y = 1
> >>
> >> Thread 2:
> >> r2 = y
> >> x = r2
> >>
> >> Question: is it legal for this program to result in r1 = r2 = 1?
> >
> >Answer: no. As written, the assignment to y fails condition (2). We
> >must execute r1 = x first in thread 1.
>
> >2) A writes may be reordered across a control flow boundary iff it can
> > be shown that the particular write will occur in any execution.
>
> Why "no"? It is impossible in this program for x to contain a
> negative value. So the assignment (2) always occurs in any execution.
Ah, yes, I meant to note this (I knew I'd forgotten something in my
last mail, but could not figure out what on a re-reading): reordering
decisions are purely thread-local, and the value of x cannot be
determined locally. This assumption was unstated in our paper because
it was laregly irrelevant.
It's only when we start discharging operations _before_ reordering
that it becomes important. We didn't directly discuss this sort of
simplification in our paper. The connection to everyday compiler
analyses (and thus the overall importance of the problem) is pretty
clear.
Let me try to re-state (2) to make it clearer (and fix a typo to boot):
2) A write may be reordered across a control flow boundary iff it can
be shown that the particular write will occur in any execution,
regardless of the existence or behavior of other threads in the
system.
Yes, when reasoning about multithreaded programs (as a programmer or
as a language implementor), local information *is* special.
Of course, if all asymmetry is to be avoided, one could instead say:
2) A write may never be reordered across a control flow boundary.
This would cause real trouble on machines which reorder writes,
though.
-Jan
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:34 EDT