
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?
If you want to restrict the intermediate actions to be non-blocking, such that another thread cannot run, then that is an extra (and significant) proof obligation.
And AFAICS your non-blocking argument only applies to co-operative scheduling. If pre-emption is permitted (e.g. interrupt-handling), then all bets are off, because an arbitrary thread could write to the IORef at any moment.
No, that is exactly what I disagree with. Faced with non-derministic semantics, the compiler does *not* have to preserve all possible outcomes. In other words, it does not have to assume that an IORef can be modified between any two arbitrary instructions. If we had to assume this, then indeed all bets would be off, and C compilers would be very much more restricted in what optimisations they could perform. I don't know how I can explain this a different way - it seems pretty obvious to me, but I'm probably not explaining it well :-/ You cut the example from my message - did you agree with the conclusion? Or the conclusion I made from Ian's example? Cheers, Simon