At 05:56 PM 7/14/2002, Bill Pugh wrote:
>At 5:23 PM -0700 7/13/02, Jerry Schwarz wrote:
>>At 12:17 PM 7/10/2002, Bill Pugh wrote:
>>
>>I think the problem is that some of us, including myself, don't see any
>>possible allowable reordering that results in r1 = 1.
>
>
>Perhaps, but so what? It isn't relevant that we can't think up a
>reordering that would induce it.
>
>Consider a program P.
>
>Let B(P) represent all of the behaviors that can be induced by by all of
>architectures and compiler transformations that you, me, and all the
>people on this list can think up.
This is fairly close to my position, with one caveat. The allowed
transformations aren't some collection that have been thought of already.
They are those that preserve single threaded semantics.
The prior question is how do we define the B transformation. I think it
should be done in stages.
First we define the semantics of a thread in isolation. This consists of
allowed sequences of read's and writes's to the shared store together with
the external (I/O) side effects. Ignoring synchronization issues, the
allowable compiler transformations are any that are consistent with the
original program under the assumption that the state of the shared store is
initially unknown, but is otherwise not mutated.
Secondly, we define the operation that combines threads by interleaving
their individual operations.
Finally the semantics of a program are the external (I/O) effects of the
semantics determined by the first two steps. That is, after combining
threads we throw away the (internal) operations on shared memory.
Note that in my formulation, out-of-air writes are allowed. For example,
one allowed transformation is
x = 2
to
x = 1;
x += 1;
In a previous email, you said that it is important to disallow this
transformation. I won't quibble with that as a requirement. I will,
however, quibble with the claim that no compiler would want to make that
transformation. Imagine a machine with one register and an add to memory
operation.
>Let B'(P) represent all the behaviors allowed by the semantics.
>
>Now, you seem indicate that you think B'(P) should be equal to B(P).
Yes. The only examples I've seen proposed for things that might be in B'(P)
and not in B(P) are those that involve knowing what other threads might
exist when determining the allowable transformations of a given thread. I'm
willing to forgo these in the interests of a simpler semantics.
>Clearly, as much as possible, B'(P) should be a superset of B(P) (it turns
>out we will have to rule out a few transformations that aren't treadsafe,
>but we'll ignore those for the moment).
>
>But you just aren't going to be able to make the semantics so tight that
>the only behaviors allowed are those that can be induced by
>transformations we can think of. If you attempt to do so, you are going to
>make the semantics more and more baroque. And you will almost certainly
>overshoot, and rule out some behavior that can be induced by some
>transformation we hadn't considered.
>
>You need to have a semantics that:
>
>* forbids the things that need to be forbidden
>* allows the things that need to be allowed
>* Is a simple as possible
>
>At 5:23 PM -0700 7/13/02, Jerry Schwarz wrote:
>>Assuming that x1 and x2 are local to the threads, then I think only way
>>that r1 can get 1 is by having the operations in Thread 1 have the ordering
>>
>> t1.x2=1 --> x=t1.x2 --> t1.x1=x --> r1=t1.x1
>
>No, in my example x1 and x2 were shared memory.
>
> 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:40 EDT