JavaMemoryModel: SC- update

From: Sarita Adve (sadve@cs.uiuc.edu)
Date: Wed Jan 07 2004 - 05:08:27 EST


Based on feedback from Bill, Jeremy, Joe, and Victor, and some insights
while working out proofs, I have been able to significantly simplify the SC-
model I sent out earlier. It is now simple enough that I can motivate and
describe it in 3 short paragraphs. I do so below and discuss the
implications in the next message. The core intuition is the same as before -
a violation of SC should only occur due to a data race, and the violation
should not itself cause a data race or values that are used to justify the
violation.

I have also finished the proofs to show that SC- appears SC to
data-race-free programs and that it allows all optimizations that I believe
are implemented today. Specifically, it is sufficient if reads return
hb-consistent values, synchronization accesses are SC, and there is no
"write speculation." This includes release consistent and lazy release
consistent systems (i.e., standard reorderings and more). It also allows
aggressive speculation on reads.

The documents describing the above are at http://www.cs.uiuc.edu/~sadve/jmm.

The following gives the basic idea for the model. Please refer to the above
document for the full motivation and formalization.

-----------------------------The SC- model ----------------------

Our abstraction of an execution is that of memory accesses executing one at
a time in program order, with reads returning the value of some write in the
execution. The memory model constrains the writes whose value a read is
allowed to return. For example, SC requires a read to return the value of
the conflicting write that occurred last before it. A read that does not do
so is a violation of SC and is referred to as a non-SC read. In general, a
non-SC read may return the value of a conflicting write that already
occurred or that will occur in the future. (Below, when we refer to a value
returned by a read, we refer to the write to the same location that wrote
that value.)

Informally, an execution E obeys SC- if all the values of all its reads can
be validated in some total order. A read's value is validated if it occurs
in a valid execution Ev and either (1) the value is an SC value for the read
in Ev or (2) the read and/or the write that wrote that value are involved in
a data race in Ev and the write is hb-consistent for the read in Ev. An
execution Ev is valid if any non-SC read in it is a previously validated
data read from E with the same value as in E.

More precisely, an execution E obeys SC- if all its reads can be validated
in some total order. A read R' is validated for E if there exists an
execution Ev such that:
o All non-SC reads in Ev are data reads that occur in E, have been
previously validated for E, and return the same value in Ev and E.
o Let R be R' or a previously validated read in E. Let R return the value of
W in E. Then
  - W and R occur in Ev, and W is hb-consistent for R in E and Ev.
  - If R is synchronization, then W is the last conflicting write before R
in E and Ev.
  - Either W and R form a data race in both E and Ev or W hb R in both E and
Ev.

----------------------------------------------------------------------------

--

Sarita

------------------------------- JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:56 EDT