[GHC] #11760: runST with lazy blackholing breaks referential transparency

28 Mar 2016

      #11760: runST with lazy blackholing breaks referential transparency
-------------------------------------+-------------------------------------
           Reporter:  Yuras          |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.10.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 A thunk created with `runST` can be evaluated twice by different threads
 producing different results. An example (taken from
 https://twitter.com/obadzz/status/714081240475951105):

 {{{#!hs
 {-# LANGUAGE RecordWildCards #-}

 import qualified Data.STRef.Lazy as S
 import Control.Monad
 import Control.Monad.ST.Lazy
 import Control.Concurrent

 data ListRef s a = ListRef
   { element :: a
   , readCounter :: Int
   , rest :: Maybe (S.STRef s (ListRef s a))
   }

 toList :: S.STRef s (ListRef s a) -> ST s [(a, Int)]
 toList r = do
   ListRef{..} <- S.readSTRef r
   S.modifySTRef r $ \e -> e
     { readCounter = readCounter + 1
     }
   xs <- maybe (return []) toList rest
   return $ (element, readCounter) : xs

 circularList :: ST s (S.STRef s (ListRef s Char))
 circularList = do
   x3 <- S.newSTRef (ListRef 'c' 0 Nothing)
   x2 <- S.newSTRef (ListRef 'b' 0 (Just x3))
   x1 <- S.newSTRef (ListRef 'b' 0 (Just x2))
   S.modifySTRef x3 $ \e -> e
     { rest = Just x1
     }
   return x1

 l :: [(Char, Int)]
 l = take 15 $ runST $ circularList >>= toList

 main :: IO ()
 main = do
   void $ forkIO $ print l
   void $ forkIO $ print l
   void getLine
   print l
 }}}

 The output (run multiple times to reproduce):

 {{{
 $ ghc --make -O -threaded -outputdir=.build test.hs
 [1 of 1] Compiling Main             ( test.hs, .build/Main.o )
 Linking test ...
 $ ./test +RTS -N2
 [('b',0),('b',0),('c',0),('b',1),('b',1),('c',1),('b',2),('b',2),('c',2),('b',3),('b',3),('c',3),('b',5),('b',4),('c',4)]
 [('b',0),('b',0),('c',0),('b',1),('b',1),('c',1),('b',2),('b',2),('c',2),('b',3),('b',3),('c',3),('b',4),('b',4),('c',4)]

 [('b',0),('b',0),('c',0),('b',1),('b',1),('c',1),('b',2),('b',2),('c',2),('b',3),('b',3),('c',3),('b',4),('b',4),('c',4)]
 $ ghc --version
 The Glorious Glasgow Haskell Compilation System, version 7.10.1
 $
 }}}

 Note that the last 3 elements are `('b',5),('b',4),('c',4)` or
 `('b',4),('b',4),('c',4)`.

 I was able to reproduce it with few weeks old HEAD. With `-feager-
 blackholing` it works as expected.

 `unsafePerformIO` uses `noDuplicate` to prevent such kind of issue. Should
 `runST` do something similar?

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11760
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

tags

participants (1)