Optimizations for mutable structures?

[Robert Dockins]

On Dec 7, 2005, at 12:05 PM, Simon Marlow wrote:

> On 07 December 2005 16:38, Malcolm Wallace wrote:
>
>> "Simon Marlow" <simonmar at microsoft.com> writes:
>>
>>> I should have said that if 'acts' blocks, then the transformation is
>>> invalid.
>>
>> Well that is exactly what I was assuming when I said that the
>> transformation is invalid. In the general case, for some arbitrary
>> actions between the write and the read (excluding another write of
>> course), there is no guarantee that the IORef remains unmodified.
>
> This is an analysis that's performed all the time in C compilers, it's
> quite straightforward to do a good approximation.  One simple  
> algorithm
> is: a store can be forwarded to a matching read as long as there  
> are no
> intervening writes that may alias, or function calls.
>
> C does this and C has threads, so what's the difference?

I would personally be very uncomfortable justifying a semantic  
transformation based on common practice in C compilers.  What exactly  
are the semantics of C programs and why do we believe that C  
compilers are correct?

I'd much rather see some argument in terms of an appropriate  
definition of observational equivalence.

[snip]

Rob Dockins