I have added a "rationale" section to my Java model document
http://www.cs.uiuc.edu/~sadve/JMM/jmm.pdf, and also made a few changes to
address the example in figure 4 below (which Bill pointed out wasn't
properly addressed).
Any comments will be much appreciated.
Thanks,
Sarita
> -----Original Message-----
> From: owner-javamemorymodel@cs.umd.edu
> [mailto:owner-javamemorymodel@cs.umd.edu] On Behalf Of Sarita Adve
> Sent: Friday, June 27, 2003 11:31 AM
> To: 'Bill Pugh'; javamemorymodel@cs.umd.edu
> Subject: RE: JavaMemoryModel: Should we prohibit all causal loops?
>
>
> 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
>
-------------------------------
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