Optimizations for mutable structures?

[Malcolm Wallace]

"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.

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.

> I don't think so.  Malcolm asserted that the transformation was invalid
> in a multi-threaded implementation; I disagree - it's just as valid in a
> multi-threaded implementation as a single-threaded one.

I think what I said was correct in general.  You need quite a lot of
side-conditions to assert the opposite.

Regards,
    Malcolm