fixST lost bottoms

[Arseniy Alekseyev]

I do find it scary, but I personally am in no position to express opinion
on what should happen (I'm not on any committee and I'm not even a regular
Haskell user).

On Mon, 9 Jul 2018 at 05:08, David Feuer <david.feuer at gmail.com> wrote:

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