JavaMemoryModel: The Intuition Is the Model - the full model is in this email!

From: Sarita Adve (sadve@cs.uiuc.edu)
Date: Mon Jul 28 2003 - 20:29:07 EDT


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