> From: Eliot Moss <moss@freya.cs.umass.edu>
> I urge you to make that model more explicit, in order to make your model
> more clear. Personally, I would prefer NOT using an underlying total
> ordering -- in physically dispersed systems, under special relativity not
> all events will be perceived in the same order by all observers. But SOME
> events will be. I would say that IN EFFECT you should be defining the
> "relativity model" for Java memory.
It is worth pointing out that the version of the semantics that we posted
was somewhat larval. As Bill said, "The write up is rough, but complete
enough to ask for (forgiving) feedback on."
Having said that, I don't think that you have to worry about an underlying
total ordering in our model, which seems to be your major concern. There
is an ordering in an execution, but the results returned by a specific
read are determined by a reasonably nondeterministic process.
Lets ignore Prescient Unsynchronized Reads (PURs) for the moment, and
pretend all reads and write are to the same memory location. The rule is
simply that a read r may observe (nondeterministically) the value of any
write w1 that occurred before it in the execution, unless there is another
write w2 that occurs on a happens-before path from r to w1.
I'll go through an example to make this clearer.
Initially, x == 0
Thread 1 Thread 2 Thread 3
Lock a
x = 1
Unlock a
x = 2
Lock a
r = x
Unlock a
The writes that occurred before the read r = x in this execution are the
write in thread 1, the write in thread 3, and the initialization of the
variable to 0. There is a happens-before relationship between the unlock
in thread 1 and the lock in thread 2. Therefore, there is a write (x = 1)
that occurs on a happens-before path between the write x = 0 and the read
r = x; r cannot be 0 in this execution trace. So r can be either 1 or 2.
Note that this is only true in this execution trace. In other execution
traces (the one where thread 2 completes first, for example), r can have
the value 0.
So you don't have to worry about each memory location being modeled as a
"place".
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:41 EDT