On Feb 25, 2004, at 3:50 PM, Vijay Saraswat wrote:
>
> To illustrate my point, lets modify the test case. Here is Test Case
> 18a
> ====================================================
> <H2>Causality test case 18</H2><PRE>Initially, x = y = 0
>
> Thread 1:
> 1: r3 = x
> 2: if (r3 == 0)
> 3: x = 42
> 4: r1 = x
> 5: y = r1
>
> Thread 2:
> 6: r2 = y
> 7: x = r2
>
> Thread 3:
> 8: if (false)
> 9 : x=43
>
> Behavior in question: r1 == r2 == r3 == 42
>
> Decision: Disallowed.
> </PRE>
> <HR>
> =======================================================
> If I follow through with your reasoning, the "conservative"
> calculation (any read can see any write) would say that x can take on
> the values 0,42,43. (You said lets assume any read can see any write.)
>
> Hence Line 4 cannot be replaced with r1=42.
>
> So adding "junk" will cause the semantics to disallow a behavior (the
> proposed behavior for Case 18).
You are confusing the compiler with the semantics.
Adding this additional Thread 3 should not change what behaviors are
allowed. 18a should still allow r1 = r2 = r3= 42.
However, with this change, the compiler might not actually perform the
transaction that resulted in that behavior in question. But it is still
allowed.
>
> This cant be right. The semantics should sastisfy the principle: Code
> that cannot possibly affect a computation should not affect it :-).
>
> I believe the issue here is that one simply cant "assume some type
> inference algorithm". The actual results returned by it might matter.
> A better alternative would be to design the semantics so that it is
> *independent* of any type inference algorithm.
This is what we have done. The semantics don't discuss any particular
form of type inference. However, the semantics need to be designed to
allow test case 18, so that a behavior that could result from one
particular form of conservative type inference is valid.
>
> The central point about Case 18 is that the behavior in question can
> be allowed only if one adds the condition (through type inference or
> whatever) that r3 takes on the values 0 and 42. It cannot be allowed
> if one ads the condition that r3 takes on the value 0 (only). Or 0 and
> 42 and 43 only. One cannot allow semantics to be defined in terms of
> the precision of some type inferencer -- without specifying that type
> inferencer. And that of course would be very unfortunate.
>
We don't, as I've mentioned. Type inference provides us with a
motivating example, but is not part of the semantics.
It is valid to make a conservative approximation that r3 can be either
0 or 43. It is also legal to make the conservative approximation that
r3 is 0, 42 or 43. If you want to show that r3 is only 0 is a valid
conservative assumption, you have to get into the details of the memory
model. In this case, it isn't.
In performing any inter-thread analysis, you have to be very careful
about your assumptions about the memory model, since, as we've seen,
the exact properties of the memory model can be very subtle. But if you
perform a conservative analysis, using a conservative approximation to
the memory model, you are allowed to use that information (you have to
be a little careful to make sure that when doing conservative analysis,
everything is conservative in the same direction; for this case, you'd
probably want to use an approximation to the memory model that allowed
at least as many behaviors as the JMM).
Bill
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:58 EDT