It occurred to me that the intuitive description I sent earlier IS the
model. I don't need all the formalism in my document, other than the
straightforward, standard definition of a data race. Below, I have reworded
the intuition I sent earlier to make it more complete.
This is it, this is the formal Java model I propose!
Sarita
----------------------------------------------------------------
The SC- model := SC - discontinuities at data races
----------------------------------------------------------------
Executing in an SC fashion means: instructions execute one at a time,
instructions of each thread execute in program order, and a read returns the
value of the last conflicting write. (A read and write conflict if both are
to the same location.)
With SC-, the execution proceeds in an SC fashion (one at a time, in program
order), until a memory access M occurs that forms a data race either with
(1) a write that has already occurred or (2) a write that could occur if we
continued to execute in an SC fashion. Call this possible execution (where M
forms a data race) as E. SC- allows the following non-SC discontinuity at M.
If M is a read, it can return a value written by any conflicting write in E.
If M is a write, then M can deposit two values in memory - its own value and
the value of the write it races with in E. The impact of this is that a
subsequent read could see the value of either write (until a later non-race
conflicting write occurs).
However, the above discontinuities are allowed only if the execution we are
generating eventually produces some write that writes the discontinuous
non-SC value read or written by M, to the same location as M.
After the above non-SC discontinuity at M, the execution again proceeds in
an SC fashion - instructions execute one at a time and in program order,
with a read returning a value from the last conflicting write - until the
next data race discontinuity, which is handled as above.
----------------------------------------------------------------
P.S. We can strengthen or weaken the discontinuities if we like - this is a
decision the community should make. I will describe this in the next
message.
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:47 EDT