Optimizations for mutable structures?

[Simon Marlow]

On 07 December 2005 15:14, Ian Lynagh wrote:

> On Wed, Dec 07, 2005 at 02:15:24PM -0000, Simon Marlow wrote:
>> On 07 December 2005 13:38, Malcolm Wallace wrote:
>> 
>>> Jan-Willem Maessen <jmaessen at alum.mit.edu> writes:
>>> 
>>>>    - Fetch elimination for imperative reads:
>>>>      writeIORef r e >> acts >> readIORef r
>>>>  === writeIORef r e >> acts >> return e
>>> 
>>> This transformation is valid only on single-threaded systems.
>>> If there is any possibility of an IORef being shared across threads,
>>> you are out of luck.
>> 
>> (assuming 'acts' doesn't modify 'r').
>> 
>> No, Jan's transformation is correct even in a multithreaded setting.
>> It might eliminate some possible outcomes from a non-deterministic
>> program, but that's ok.  There's no requirement that all
>> interleavings according to the semantics have to be implemented. 
>> This is a hard property to state precisely, indeed we gave up trying
>> to in the concurrency/FFI paper:
>> http://www.haskell.org/~simonmar/papers/conc-ffi.pdf, see Section 
>> 6.1.
> 
> I don't think it's true for this program:
> 
> import Data.IORef
> import Control.Concurrent
> 
> main = do m1 <- newEmptyMVar
>           m2 <- newEmptyMVar
>           let e = 6
>               not_e = 7
>               acts = putMVar m1 () >> takeMVar m2
>           r <- newIORef 5
>           forkIO $ do takeMVar m1
>                       writeIORef r not_e
>                       putMVar m2 ()
>           writeIORef r e
>           acts
>           readIORef r >>= print

Sorry for not being clear enough, see my other message.  I agree the
transformation is not valid in this case.  putMVar and takeMVar count as
modifying the IORef.

However... remove all the putMVars and takeMVars.  Do you think it's
valid now?  Even though after the transformation the program might
deliver a different answer?  (I claim yes).

Now, take the original program, but change the creation of m2 to
"newMVar ()", i.e. m2 starts off full.  Is the transformation valid now?
Well maybe, because in some interleavings acts does not block, and we
can prove that at compilation time.  Interesting - I think you could
justify doing the transformation in this case too, but I doubt any
compiler would go that far.

Cheers,
	Simon