
On Dec 7, 2005, at 12:05 PM, Simon Marlow wrote:
On 07 December 2005 16:38, Malcolm Wallace wrote:
"Simon Marlow"
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