fixST lost bottoms

[David Feuer]

That's a very scary, albeit contrived, example. I wonder if there are more
realistic functions that are susceptible to this attack from "safe"
Haskell. In light of your exploit, I'm leaning toward saying we probably
*should* fix this, but I'd like to hear your opinion.

On Sun, Jul 8, 2018, 6:51 PM Arseniy Alekseyev <arseniy.alekseyev at gmail.com>
wrote:

> 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/20180709/fccece61/attachment.html>