Re: JavaMemoryModel: Causality Test 16

From: Jeremy Manson (jmanson@cs.umd.edu)
Date: Sat Dec 20 2003 - 18:26:34 EST


> =========================
>
> Causality test case 16
>
> Initially, x = 0
>
> Thread 1:
> r1 = x
> x = 1
>
> Thread 2:
> r2 = x
> x = 2
>
> Behavior in question: r1 == 2; r2 == 1
>
> Decision: Allowed.
>
> ==========================
>
> I'm having some difficulty seeing why this isn't like test case 5. Although
> there are executions that result in r1 == 2, and executions that result in
> r2 ==1, I cannot see an execution that produces both, so one or other value
> is out of thin air even though there are other non-out-of-thin air
> executions that store that value.

The major difference is that in this case, both writes occur in every
execution, whereas in test case 5, the writes of 1 in threads 1 and 2 only
occur if the read in thread 4 sees the value 1. To put it another way,
the writes have been caused to occur in 16, but not in 5.

I should add that if only one of r1 == 2 or r2 == 1 can be true, then the
assumption is sequential consistency. The model isn't really built around
sequential consistency. It is more built around happens-before; this
result is harmonious with with happens-before.

Having said this, here is how this test case plays out in our model. There
is a justification order over actions in an execution, and a read can see
any write that occurs earlier in the justification order as long as it is
not prevented from doing so by synchronization or program order (i.e.,
happens-before).

Justification order can map to program order, or an action can be
performed early if it occurs in every execution (in our model). In case
16, we can have:

x = 1 (thread 1)
r2 = x (sees 1)
x = 2 (thread 2)
r1 = x (sees 2)

x = 1 occurs out of program order; it can do so because it occurs in every
execution. (In Sarita's model, it can occur out of program order because
it is on a cycle)

I hope that clears it up.

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



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