I would like to add to this that my model (from last summer -
http://www.cs.uiuc.edu/~sadve/JMM/jmm.pdf) does not have this problem.
It also has only two requirements or properties:
(1) Data-race-free parts of a program are guaranteed SC behavior.
(2) Values are not generated out-of-thin-air.
Compared to Bill's/Jeremy's model I feel these two requirements are closer
to programmer-level guarantees we want to ensure, and so their formalization
is more likely to capture exactly the necessary constraints that should be
imposed for the Java model.
My model also prohibits all of the other results that Bill recommends
prohibiting below (figures 2, 3, 4).
But it does not prohibit figure 1 because the above properties do not
require that it be prohibited.
Finally, regarding the statement about Bill/Jeremy's model:
> 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)
>
Note that my model directly states the first of the above "good things" as
its first property (i.e., this property is not a side-effect, it is the
first specified property of the model as it should be).
Similarly, the second good thing above is the second specified property of
the model (I have earlier argued that the no flow dependence cycles property
is synonymous with, and the formalization of, the not-out-of-thin-air
property). Again, this is not a side effect of my model, it is the model.
Finally, regarding the third "good thing" above, why do we need it? The
specific example that Bill has in Figure 4 is prohibited by my model too.
But it is prohibited by the first property of my model (data-race-free parts
of the program should see SC behavior), which is a more fundamental
property.
I will post a more elaborate "rationale" document for my model on Monday, in
case that helps further.
Sarita
> -----Original Message-----
> From: owner-javamemorymodel@cs.umd.edu
> [mailto:owner-javamemorymodel@cs.umd.edu] On Behalf Of Bill Pugh
> Sent: Friday, June 27, 2003 9:27 AM
> To: javamemorymodel@cs.umd.edu
> Subject: JavaMemoryModel: Should we prohibit all causal loops?
>
>
> 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
>
-------------------------------
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