RE: Optimizations for mutable structures?

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