RE: JavaMemoryModel: Comments on Sarita's example for our model, and on Sarita's model

From: Sarita Adve (sadve@cs.uiuc.edu)
Date: Fri Aug 16 2002 - 13:46:20 EDT


Bill,

Thanks for your comments on my model. They certainly make me think about
ways to try to make the model better, but I still don't see any
fundamental problems with my approach.

Summary:

The key problem raised (about initial conditions) is trivial to handle
(it arose because I didn't give my formal definition of a program). The
rest are a set of general comments (some invalid in my opinion),
addressed below.

Details:

> Part of the problem is that proving that a memory model has desirable
> properties X, Y and Z doesn't mean the memory model also has
> desirable properties A and B. And it is impossible to ensure that we
> have enumerated all of the desirable properties.

I am not sure what this is trying to say. I believe all models would
suffer from this problem. If you are saying that your approach is better
because it is more likely that it serendipitously incorporates some
desirable property for the future, then that seems like a weak argument.
Because it is equally likely that it inadvertently incorporates a
requirement that is too strong for the future.

>
> Another property that it would be nice to have.
>
> Say you have a program P, and initial condition I1 and I2. These
> initial conditions might be set from the command line, environment
> variables, or the initialization of the program. Assume that the part
> of the program that sets the initial conditions is correctly
> synchronized.
>
> Further assume that under initial conditions I1, the entire program
> is correctly synchronized. However, under initial conditions I2, the
> program is not correctly synchronized.
>
> You would like to have the property that under initial conditions I1,
> the program obeys sequentially consistent semantics.
>
> Sarita's proposal doesn't have that property. Consider:

Valid conclusion based on the document on the web site, but it isn't
true. I didn't put in the formal definition of a program in the writeup.
In my past work, a program has included the initial conditions, external
inputs, etc. I'll add that in shortly.

>
> Initially, x = y = 0, foobar = either true or false
>
> Thread 1:
> if foobar
> x = 1
> y = 1
>
> Thread 2:
> if x = 1
> y = 1
>
> Thread 3:
> if y = 1
> x = 1
>
> OK, if foobar = true, this program has a data race. However,
> if foobar=false, this program is correctly synchronized.
> However, under Sarita's model
> threads 2 and 3 could write to x and y even when foobar=false.

This isn't the case if you consider that the program is also a function
of the initial conditions, command line, etc. That is, the program with
initial condition foobar = true is different from the program with
foobar = false.

>
> Our previous semantics handles this case, but not other issues with
> initial conditions. We hope to handle this in tomorrow's revision.
>
> General comments on Sarita's model. Her first two conditions
> essentially give us model A (of the two models I described
> previously). Her conditions (3) and (4) are designed further restrict
> the model to prohibit causal loops.
>
> However, I don't feel that they are entirely satisfactory.
>
> First, both conditions are intended to do the same thing. If either

No, the conditions are not intended to do the same thing, and I believe
that's a strength of this approach - each requirement is there for an
explicit reason. The rationale document
(http://www.cs.uiuc.edu/~sadve/jmm-appendix.pdf) explains clearly what
each one is meant for. Condition 3 is meant to prohibit non-SC data
races and #4 is meant to prohibit values that aren't generated from
constant assignment statements in the program (i.e., from thin air).
You've been clubbing both together under the informal term "causal loop"
without defining what that means, and without explicitly addressing it
in your model. My approach is the only one so far that formally
captures these notions explicitly. It is possible that there is a way to
formally unify the two ideas of non-SC data races and out-of-thin-air
values, and it would be great if someone could do it, but I haven't seen
that yet. Until then, they are treated separately in my model.

> condition really captured everything it needed to capture, there
> wouldn't be a need for the other condition.

See above.

>
> For example, condition (4) doesn't mention control dependence, yet
> there is no reason to believe that control dependence is better
> handled by (3) than flow dependence.

I don't know what is the concern here. It is not like control dependence
and flow dependence are the problems per se. They are symptoms or causes
of the problems. I classify the problems due to these dependences into
two categories (SC data races and program-generated values), and provide
a requirement to handle each category. I consider it a strength that
this approach does not need to mention control dependence explicitly.
Needless to say, (3) implicitly imposes constraints on both control and
data dependences, but only for the explicit purpose of prohibiting
non-SC data races.

>
> Condition (4) forces a compiler to reason about possible executions
> in a semantics that doesn't include (4) in order to determine whether
> a value is truly constant.
>

Again, why is that a problem? Analogously, your PUR condition requires
the compiler to finally validate an execution with PURs against one
without PURs.

Also, note that there will be other accompanying sets of sufficient
conditions that are more amenable to use by hardware and compiler
designers. These conditions will be stronger than the model, but can be
used by Joe designer who doesn't want to deal with the full generality
of the model.

> Condition (3) has significant problems with contamination across
> initial conditions, as I've mentioned.

No, see above.

> I believe it also suffers from
> the problem Sarita mentioned with revision of a week ago; that it
> doesn't handle statement splitting transformations.

I also mentioned a solution then (and it was a problem with your model
as well). I'll put the solution up on the web site in a bit. If you have
a specific example in mind, please let me know.

Thanks again for the comments. I will try further to see if I can
improve things to better address some of your general comments. But
again, I still don't see any show stoppers with the approach.

Sarita

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



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