Re: JavaMemoryModel: The property of "race-free implies SC"

From: Yue Yang (yyang@cs.utah.edu)
Date: Fri Oct 24 2003 - 12:36:48 EDT


Hi Victor,

On Fri, 24 Oct 2003, Victor Luchangco - Sun Microsystems wrote:

> Hi Jason,
>
> You said:
>
> > Suppose we add a read of c in T2 as follows:
>
> > r1 = a; r2 = b;
> > c = 1; r3 = c;
> > if(r1 > 0) if(r2 > 0)
> > b = 1; a = 1;
>
> > Now the code contains races and it doesn't need to follow SC. So
> > there is really no compelling reason for prohibiting r1=r2=1.
> > (Allowing r1=r2=1 doesn't seem to be too bizarre since the branch
> > conditions are consistent with the results of interest.) But if we
> > allow the two cases to have different executions, programmers can't
> > freely add debug reads without worrying about the legal outcome.
>
> I don't understand your reasoning here. Why is r1=r2=1 any less
> bizarre in this case than in the case that c is not read? Certainly
> there are reasons to argue against the "race-free programs are SC"
> requirement, but these arguments have been had, and the conclusion, as
> I understand it, is that forgoing this requirement may cause too much
> code to break, because it deviates too much from the intuitive model
> that Java programmers supposedly have in their heads (even if that
> model is malformed and inconsistent). Staying close to this model was
> one of the desiderata (though lower than logical consistency and
> reasonable implementability) for the JMM.
>

I mean r1=r2=1 is _equally_ not bizarre in both cases if we adopt a
slightly different mentality, i.e. if we don't need to strictly follow
the "race-free (under SC) programs are SC" rule. In fact, my point is
exactly that the two cases should be treated the same way. Just adding
one read shouldn't alter the legal results even though it changes the
race situations under SC.

This suggestion is actually less intimidating than it appears. Note that
both cases would contain races under the JMM if JMM allows r1=r2=1 in
those cases. So it seems to be more reasonable to follow "race-free (under
JMM) programs are SC" as a guideline. In other words, Java programmers can
still maintain "backward compatibility" by making sure their code is race
free for the underlying Java memory model, rather than SC.

I think the original reason to define race-freedom using SC might be
trying to avoid the circularity of JMM specification and race definition
(Before specifying JMM, how can we use it to define race conditions?).
But this "race-free programs are SC" property should be a result derived
from the JMM after JMM is defined. It's also not apparent to me how it can
help race-containment issues. Is there any fundamental reason that
we have to use SC to define race conditions?

- Jason

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



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