> 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.,
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.
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