Jeremy,
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.)
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.)
Similarly, I can't see why a read in a lock region can't move down below the
lock region.
I'd appreciate it if you could illustrate how one goes about reasoning about
these properties using the definitions in your model.
-- Joe Bowbeer----- Original Message ----- From: "Jeremy Manson" <jmanson@cs.umd.edu> To: <javamemorymodel@cs.umd.edu> Sent: Friday, March 30, 2001 7:36 AM Subject: JavaMemoryModel: Re: movement into synchronized blocks
> > PS - I'm still fairly sure there's a difference in the movement of memory > operations allowed by the two proposals, but I'm less sure about the > details. > > The CRF paper explicitly states that it permits normal reads and writes to > move into a lock region, and prevents memory operations inside the lock > region from moving outside. > > But what movement is allowed by the operational semantics model? My > revised interpretation is that normal writes can move up and down across a > lock but cannot cross an unlock; while normal reads cannot cross a lock > but can move up and down across an unlock. What's the real story?
Normal reads and writes can move into a synchronized block from either direction. There is actually a short note about this in the tech report version of the paper, which should be available sometime today. In more detail:
A lock acts as an acquire. Moving a read past a lock does not affect the memory semantics. As soon as a write occurs, that value goes into the set of values that can be read from the variable. A read will essentially pick one of these values at random to be read. The lock operation may remove some of these values from this set, but any of the values that are left over will still have been in the set when the read originally would have occurred. So the "random" value picked is just a little less random, but that's okay, because we don't say "random with guaranteed equal probability across all platforms".
An unlock acts as a release. Moving a write up before an unlock operation doesn't make any difference; a read in another thread picks a value at random that has been written to the variable. Again, it is simply "more likely" to pick the value for the write if there is communication between the threads through the monitor.
Now, this explanation skims over how values for a variable are removed from the set, but that happens in fairly obvious ways.
I have been thinking of different ways to say all of that for a few days now; I am sticking it in my "explanatory note" on the model. I am actually coming to the conclusion that it is difficult to explain it without some previous understanding of our model. Is the above at all comprehensible?
We have a section in the tech report with more on the differences between our model and CRF, but it would be impossible for it to come from us without its making ours sound better (insert smiley face here). And anyway, if we didn't believe we could build a better mousetrap, what would be the point of building one at all? We could just buy one from the hardware store like everyone else.
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