fixST lost bottoms

[Arseniy Alekseyev]

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 at 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 at 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 at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20180708/1005a758/attachment.html>