>
> Because of the fences in CRF, it's easy to see what movement is allowed:
> memory operations can move into a lock region but can't move out.
>
> The operational semantics model is less direct in this regard. (And your
> explanations below help a little, but not enough.)
>
> I can't see why, from the definitions of lock and unlock and writeNormal and
> readNormal, a write can't move up out of a lock region. (Or may be it can.)
(I am hoping the trip up to NY hasn't clouded my brain further) The trick
is that it isn't prevented because of memory semantics. It is prevented
because introducing it would violate the requirement that any reordering
remain operationally equivalent to the original ordering. So you have to
prove you aren't changing the semantics of the program by moving the
write/read out of the lock region. For example, you can't introduce
deadlock. This is tricky, but since proving this sort of thing is
possible (I could imagine some sort of hoisting with variables which could
be proven thread-local), we should allow it.
> Also, I can't see how a write below a lock region can move up into the lock
> region -- because the side effects of the write will be transmitted to other
> threads by the unlock. (You cover this a little below but I'm still missing
> something.)
It is tricky to explain without relying too much on the semantics we
wrote. I'll try it that way (without having the actual set names in front
of me).
Here's a bit of code to illustrate:
initially, allWrites_v = {42} (or, to think of it another way, v == 42).
Assume all overwritten sets are empty.
Thread 1
unlock m // overwritten_m U= overwritten_t1
write 1 to v // allwrites_v += 1, allWrites ={42, 1}
Thread 2
read v // reads some arbitrary value from allwrites_v - overwritten_t2
Thread 3
lock m // overwritten_t3 U= overwritten_m
read v // reads some arbitrary value from allwrites_v - overwritten_t3
This is the original order. Assume thread 1 occurs before thread 2 or
thread 3. After thread 1 executes, allWrites_v == {1,42} and
overwritten_m is empty. Thread 2 can read 1 or 42 from v because it picks
an arbitrary value from allWrites_v - overwritten_t2, and overwritten_t2
is empty. Thread 3 also can see 1 or 42 because it reads some arbitrary
value from allWrites_v - overwritten_t3, and overwritten_t3 is empty.
Now assume that we switch the order of the instructions in thread 1.
allWrites_v is, again, {1,42}. Now, however, overwritten_m is {[v,42]},
because it knows v has been overwritten. Thread 2 can still see either 42
or 1 because no thread communications have occurred to tell it about
overwritten_m. Thread 3 does know that 42 has been overwritten, because
of the lock. Thread 3 can only read 1 from v.
So, the change is that before thread 3 could arbitrarily choose to read 1
or 42 from v, whereas now it can only read 1. *This doesn't matter*.
*Having* to read 1 is the same as *choosing arbitrarily* to read 1, which
was legal before. The execution is still equivalent to a legal one.
This is a little tricky to see. We just have to remember that a
nondeterministic choice can be implemented by always choosing the same
thing, because random is not the same as uniformly distributed.
I hope that clears it up a little.
>
> Similarly, I can't see why a read in a lock region can't move down below the
> lock region.
Same deal as the moving writes up: as long as it doesn't affect the
program semantics you are fine.
Jeremy
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:31 EDT