One high level property of the proposed JMM is that if a program
is free of race conditions (under Sequential Consistency
interleaving), it should behave as SC.
While this property seems to be a good standard for straight-line code,
it is not as "natural" when applied for making branch decisions.
Consider the following example:
(initially a = b = c = 0):
T1 T2
r1 = a; r2 = b;
c = 1; if(r2 > 0)
if(r1 > 0) a = 1;
b = 1;
Because it's race-free under SC, it prohibits r1=r2=1 since SC doesn't
allow it. 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.
One alternative is to give up the "race-free implies SC" property.
I understand this property has a very legit motivation - algorithms and
compilation techniques developed for SC can be safely reused,
assuming one can prove the code is race-free. However, I'm wondering
how significant its practical advantage is. After all, precise race
analysis is a very hard problem and JMM is supposed to be as relaxed
as possible to enable more optimization opportunities. This property
seems to make it even harder to reason about Java programs.
- 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