In some offline discussions with Sarita, she raised the question of
whether we in fact need to prohibit all causal loops.
Informally, our model has two rules.
* consistency (e.g., each read R must see the value of some write W1 that
occurs, such that no other write W2 is guaranteed to overwrite
W1 and occur between W1 and R).
* no causal loops (e.g., an event must not occur only because the event is
already assumed to occur).
For example, consider Figure 1:
Initially, x = 0, y = 0, a[0] = 1, a[1] = 2
Thread 1 Thread 2
r1 = x r3 = y
a[r1] = 0 x = r3
r2 = a[0]
y = r2
Prohibited behavior r1 == r2 == r3 == 1?
How could this have happened?
r3 == 1 can only be explained by having r2 == 1
r2 == 1 can only be explained if the write to a[r1] didn't overwrite a[0]
the write to a[r1] doesn't overwrite a[0] only if r1 != 0
r1 != 0 can only be explained by having r3 == 1
So we claim that this is a causal loop, and must be prohibited.
Sarita points out that this is a data race, and that no value is
being read out of thin air, and asks what is so bad about allowing
this behavior.
OK, so right now our model is basically:
* consistency (each read sees a write that is allowed by the
happens before ordering)
* no causal loops
These two rules give us several other good things for free:
* Correctly synchronized programs have SC behavior (see Figure 2)
* No flow dependence cycles (see Figure 3)
* No flow/control-dependence cycles (see Figure 4)
--------------
Figure 2: Initially, x = y = 0
Thread 1 Thread 2
r1 = x r2 = y
if r1 > 0 if r2 > 0
then y = 42 then x = 42
Prohibited behavior: x == y == 42
--------------
Figure 3: Initially, x = y = 0
Thread 1 Thread 2
r1 = x r2 = y
y = r1 x = r2
Prohibited behavior: x == y == 42
--------------
Figure 4: Initially, x = y = 0
Thread 1 Thread 2
r1 = x r2 = y
if r1 > 0 if r2 > 0
then y = 42 then x = 17
else y = 0 else x = 0
Prohibited behavior: x == 17, y == 42
--------------
So since we get all of these nice behaviors out of two simple
concepts, I think that trying to get into details of which kinds of
causal loops are allowed and which are forbidden is going to be
confusing and unlikely to capture the behavior we want.
We played around with trying to formalize the concepts of flow
dependence cycles and flow/control dependence cycles, and were never
able to come up with anything satisfying. The idea of no causal
cycles seems much clearer and intuitive (even if the formalization of
that concept is difficult to understand).
So I think that forbidding causal cycles is the right way to go, and
we need to forbid the prohibited behaviors in Figures 1-4 of this
email.
Anyone want to argue that we should allow the behaviors in any of
these figures?
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:46 EDT