Sorry for being off the list for a few days, I've been on vacation.
At 12:41 PM -0500 7/30/02, Sarita Adve wrote:
>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
Sorry, one typo (two threads labeled thread 2). Fixed below, with annotations
of which write is seen by each read.
Ex 4:
Initially, x = y = z = 0
Thread 1:
z = 2
Thread 2:
r1 = z (sees initial write of z = 0)
x = r1
Thread 3:
r2 = x (sees thread 4's x = 2)
r3 = r2 + 1
y = r3
Thread 4:
r4 = y (sees thread 3's y = 3)
r5 = r4 - 1
x = r4
Causal loop behavior: r1 = 0, r2 = 2, r4 = 3
> >
>> 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?
We do _not_ forbid r1 = 1. In fact, allowing r1 = 1 was what forced
us away from initWrites to our newest model.
>
> 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.
OK, this attempts to fix the the previous acyclic flow dependence
constraint by added a rule that something that writes a constant
value in all possible execution traces isn't flow dependent on any
other statement.
I have two problems with this. First, this definition depends upon
"all possible execution traces". But "all possible execution traces"
depends upon the acyclic flow dependence constraint, so you have a
circular definition.
But even if you fixed that, it is still fundamentally flawed, because
"all possible execution traces" is too broad.
For example, we had:
Ex 2:
Initially, x = y = 0
Thread 1:
r1 = x
r2 = r1*r1 - r1 + 1
y = r2
Thread 2:
r3 = y
r4 = r4*r4 - r4 + 1
x = r4
We modify example 2 slightly so that r2 and r4 aren't always 1:
Ex 2a:
Initially, x = y = z = 0, z is final
Thread 1:
z = Integer.getInteger("offset",1).intValue();
Thread 2:
join thread 1
r5 = z
r1 = x
r2 = r1*r1 - r1 + r5
y = r2
Thread 3:
join thread 1
r6 = z
r3 = y
r4 = r4*r4 - r4 + r6
x = r4
Now, a JIT running after thread 1 has could decide that r5 and r6 are
the constants 1 and get us back to the code and optimization from Ex
2.
The problem is that "all possible execution traces" is too broad.
First, the JIT may run after some computation has been performed, and
so already know that the set of possible executions is limited.
Secondly, the compiler may not that it won't generate all possible
execution traces, and take that into account in deciding whether
something is effectively constant.
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:41 EDT