Bill,
I am reading the new memory model document and your previous note on the
philosophy of handling "causal loops." I have some initial questions and
comments below.
Philosophy of the new approach:
-------------------------------
As we discussed, I like the happens/before and a trace-based approach very
much, but I don't like the approach of leaving part of the spec to an
informal statement about causal loops. As you point out too, the causal loop
aspect is the most difficult part of formalizing memory models. If we
relegated that to an informal statement, we would effectively be making the
same mistake as many previous approaches. I therefore need to understand
what exactly you propose to leave out and why that is preferable to using
another approach for the spec. So quoting from your "philosophy" message:
> So I'm proposing that the formal semantics allow incorrectly
> synchronized programs to exhibit anomalous behavior that can only be
> explained by a causal loop. For example, the current rules I'm
> considering for "out-of-thin-air" safety would still allow the
> following to squeak by the formal version of the rules:
>
> Ex 4:
> Initially, x = y = z = 0
>
> Thread 1:
> z = 2
>
> Thread 2:
> r1 = z
> x = r1
>
> Thread 2:
> r2 = x
> r3 = r2 + 1
> y = r3
>
> Thread 3:
> r4 = y
> r5 = r4 - 1
> x = r4
>
>
> Causal loop behavior: r1 = 0, r2 = 2, r4 = 3
Is the above typo-free? Can you elaborate?
Also, you say:
>
> The formal rules will forbid Ex 3, because they will require that
> each value be created somewhere. However, this rule still allows Ex 4.
Again, is the above typo-free? That is, can you confirm that you are indeed
happy with your formal semantics forbidding Ex 3; i.e., the outcome r1=1
below?
> Ex 3:
> Initially, x = y = z = 0
>
> Thread 1:
> x = 1
>
> Thread 2:
> r1 = z
> r2 = x
> y = r2
>
> Thread 3:
> r3 = y
> z = r3
>
> The question in, can this program result in r1 = 1?
Alternative approach
---------------------
Quoting again from the philosophy message:
> So, at this point there are four possible options:
>
> a) Use a rule forbidding dependence cycles, knowing that this could forbid
> certain compiler optimizations.
>
> b) Use a double semantics approach. Have one memory model that is used for
> deciding whether something is a causal loop, and another memory model
> for execution that using the causal loop definitions from the other
> semantics. (Essentially what Sarita suggested a week ago).
>
...
> I am not happy with choices a or b, and we can't depend upon c
> happening when we need it to, if ever.
>
I wouldn't describe my approach as (b). The "second semantics" you ascribe
to my approach is analogous to the use of "execution trace" in your
approach. In other words, here's how my approach goes analgous to yours:
(1) Define an execution trace as ... [just like your approach, but my
execution traces are "weaker" than yours because I do not require that all
accesses of a single thread be in program order].
(2) Define when an execution trace is a valid execution trace. This requires
defining certain properties of the execution trace that may or may not
require looking at other execution traces. That's again just like your
approach. For example, for the thin-air property:
Define a flow dependence relation on actions of each trace, denoted fd, as
follows: I fd J if:
- I fd K fd J for some K or
- J reads a value written by I, unless J writes the same value in all
possible execution traces.
For an execution trace to obey thin-air property, fd should be acyclic.
So, what's the philosophical problem with this approach?
Circularity in proof to show SC:
--------------------------------
The proof that "correctly synchronized programs get SC" is incorrect because
it has a circularity in its argument. We want to define a program as
correctly synchronized if it is race-free in all *SC executions*. In that
case, we cannot assume a priori any information about that program on a
non-SC system. In particular, the current proof assumes that conflicting
accesses will be ordered by happens-before on a system obeying your memory
model, but that's exactly what you want to prove. Hence the circularity.
In other words, these proofs are also complicated in that they have to deal
with the causal loops issue - that is, we have to directly or indirectly
prove that a causal loop cannot cause a race that would not occur on an SC
execution but occurs in the execution of the system whose correctness we are
trying to prove. (So at the least, there needs to be "enough causal loop
avoidance" built into the formal spec to do the proof.)
Smaller issues that are easily resolved:
----------------------------------------
- I would reverse the happens-before order because that's the way it is
defined in the literature (starting from Lamport's original paper on
distributed systems).
- As others have pointed out, the happens-before definition and consequent
treatment of volatiles is incomplete, but easily fixed.
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:40 EDT