fixST lost bottoms

[David Feuer]

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

[Levent Erkok]

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.

Post by David Feuer
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!
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[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

Post by Levent Erkok
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
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.
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.

Post by David Feuer
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!
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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

[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.

Post by 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

Post by Levent Erkok
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
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.
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.

Post by David Feuer
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!
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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

[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).

Post by 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 <

Post by 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

Post by Levent Erkok
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
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.
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.

Post by David Feuer
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!
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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

[Edward Kmett]

Arseniy's example definitely leaves me inclined to say we should fix rather
than just document this.

-Edward

On Sun, Jul 8, 2018 at 6:51 PM Arseniy Alekseyev <

Post by 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

Post by Levent Erkok
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
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.
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.

Post by David Feuer
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!
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
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
For more options, visit https://groups.google.com/d/optout.