This might be just me expecting too much guarantees from ST monad, but it seems to me that this is a potential violation of memory-safety.

Consider the program below.

The use of [unsafeWrite] in [silly_function] is guarded by the code above (we know we wrote [sz] so we should read back [sz]). It ought to be safe if you can rely on sequential execution of ST monad with no preemption.

However, it does end up preempted due to the use of [mfix] elsewhere in the program, which leads to a segmentation fault.

import Data.Array.ST

import Data.Array.Base

import Control.Monad.ST.Strict

import Control.Monad.Fix

silly_function :: STArray s Int Int -> Int -> ST s ()

silly_function arr a = do

  (0, sz) <- getBounds arr

  writeArray arr 0 sz

  let !res = a

  sz <- readArray arr 0

  unsafeWrite arr sz res

foo :: ST s Int

foo = do

  arr <- newArray (0, 10) 0

  mfix $ \res -> do

    n <- readArray arr 0

    writeArray arr 0 1000000000

    if n > 0

    then

      return 666

    else do

      silly_function arr res

      readArray arr 10

main = print $ runST foo

On Sun, 8 Jul 2018 at 22:26, Levent Erkok <erkokl@gmail.com> wrote:

Hi David,

Wonderful example. I'm afraid no-eager-blackholing also breaks the "no spooky action at a distance" rule. Since `x` is not used recursively, we should be able to pull it out of the `mfix` call, transforming the original to:

foo :: ST s Int

foo = do

  ref <- newSTRef True

  x <- readSTRef ref

  mfix $ \res -> do

    if x

      then do

        writeSTRef ref False

        return $! res + 5 -- force the final result

      else return 10

I believe this variant will produce <<loop>> with or without eager-blackholing, as it should. By this argument alone, I'd say the no-eager-blackholing breaks mfix axioms for strict-state.

This example is also interesting from a pure termination point of view: Moving things "out-of" mfix usually improves termination. In this case, the opposite is happening.

Strictly speaking, this is in violation of the mfix-axioms. But I doubt it's worth losing sleep over. I suggest we add this as an example in the value-recursion section on how eager-blackholing can change things.

Cheers,

-Levent.

On Sun, Jul 8, 2018 at 9:40 AM, David Feuer <david.feuer@gmail.com> wrote:

I filed a ticket[*] for this, but I think maybe the libraries list should weigh in on whether it is something that should be fixed. In general, fixST f is supposed to bottom out if f forces its argument. However, the lazy way GHC blackholes thunks under evaluation sometimes leads to the computation being run again. In certain contrived situations, this can allow the computation to succeed!

The example I give in the ticket:

import Control.Monad.ST.Strict

import Control.Monad.Fix

import Data.STRef

foo :: ST s Int

foo = do

  ref <- newSTRef True

  mfix $ \res -> do

    x <- readSTRef ref

    if x

      then do

        writeSTRef ref False

        return $! res + 5 -- force the final result

      else return 10

main = print $ runST foo

Here, the computation writes to an STRef before forcing the final result. Forcing the final result causes the computation to run again, this time taking the other branch. The program prints 15. When compiled with -O -feager-blackholing, however, the expected <<loop>> exception occurs.

As far as I know, this weirdness never changes the value produced by a non-bottoming computation, and never changes a non-bottoming computation into a bottoming one. The fix (defining fixST the way fixIO is currently defined) would have a slight performance impact. Is it worth it?

[*] https://ghc.haskell.org/trac/ghc/ticket/15349

_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

--
You received this message because you are subscribed to the Google Groups "haskell-core-libraries" group.
To unsubscribe from this group and stop receiving emails from it, send an email to haskell-core-libraries+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.