At 12:44 PM -0800 1/12/04, Jerry Schwarz wrote:
>>
>
>The form of this argument seems to be something like:
>
>When we reach r1=X in T1 we can make certain assumptions about the
>state of the world that will result in an execution in which we will
>read 1. Because of that the compiler can presciently assume that X
>will have the value 1 without violating "not out of thin air". The
>kind of assumptions we can make are "forbidden prefix".
>
>My question is: what privileges the "forbidden prefix" form of the
>assumptions? Why shouldn't the compiler be allowed to make whatever
>assumptions it wants about the state of the other threads when it
>decides to force a prescient read?
>
>If we think compilers ought to be allowed this kind of reasoning
>then we should state the principal and leave the details to the
>compiler authors to work out.
Forbidden prefixes are design/needed to capture are cases where the
compilers or architectures execute programs in a way such that not
all behaviors are possible.
For example, :
* non-volatile long reads and writes might always be performed
atomically
* a read might always see the value of a previous write within the
thread, even though it might be possible for it to see other
writes [could occur through forward substitution]
* two reads might always see the same value [could occur through
redundant load elimination]
The point is, we need to allow compilers and systems to use this
information, and if an action is now guaranteed do to such a
transformation, be allowed to
perform it presciently.
I worried that if I tried to enumerate such transformations, I'd
leave some out. Alternatively, if I said the compiler can do anything
it wants to, we aren't providing any kind of definitive spec.
>
>I hypothesize that if we allow the compiler to make arbitrary
>assumptions about the state of the other threads subject only to
>their being consistent with what has already happened in the current
>thread then we end up with something like SC-.
The trick here is that we are allowing the compiler to make
assumptions about the possible future behavior of the program.
The problem is that the compiler should only be allowed to assume
something if it is true, and is true in a way that doesn't depend on
the assumption. For example, in causality test case 4, if thread 1
assumes that thread 2 will write 1 to x, then it might decide that it
can write 1 to y, which leads to behavior we must not allow.
Alternatively, you can't assume that two reads will always see the
same value, and use this to derive a behavior in which they see two
different values.
I don't think that the idea Jerry suggests, about allowing threads to
make assumptions based only on their own state, is a useful way to
try to relax M/P to make it closer to SC-.
Bill
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:56 EDT