Re: Is Safe Haskell intended to allow segfaults?

I see three major stories here: 1.) If you remove IO from being able to be compiled inside Safe code _at all_ most packages I have that bother to expose Safe information will have to stop bothering. I'd have to cut up too many APIs into too many fine-grained pieces. This would considerably reduce the utility of Safe Haskell to me. Many of them expose a few combinators here and there that happen to live in IO and I can view offering Safe or Trustworthy to users as a 'the pure stuff looks really pure' guarantee. For the most part it 'just works' and Trustworthy annotations can be put in when I know the semantics of the hacks I'm using under the hood. 2.) Assuming instead that you're talking about a stronger-than-Safe additional language extension, say ReallySafe or SafeIO, it all comes down to what the user is allowed to do in IO, doesn't it? What effects are users granted access to? We don't have a very fine-grained system for IO-effect management, and it seems pretty much any choice you pick for what to put in the sandbox will be wrong for some users, so you'd need some sort of pragma for each IO operation saying what bins it falls into and to track that while type checking, etc. At least then you could say what you are safe with respect to. That all seems to be rather a big mess, roughly equivalent to modeling an effect system for IO operations, and then retroactively categorizing everything, putting a big burden on maintainers and requiring a lot of community buy-in, sight unseen. 3.) On the other hand, someone could _build_ an effect system in Haskell that happens to sit on top of IO, holding effects in an HList, undischarged nullary class constraint, etc. then pull a couple of Trustworthy modules around it for embedding the effects they want to permit and build this today without any compiler support, they'd just have to make a final application-specific Trustworthy wrapper to run whatever effects they want to permit into their program. It is more invasive to the code in question, but it requires zero community organizing and we've already got all the compiler mojo we need. The downside is the Trustworthy wrappers at the bottom of the heap and that it doesn't interoperate with basically anything already written. -Edward On Tue, Aug 9, 2016 at 10:45 PM, Ryan Newton wrote:

I'm hearing that Safe Haskell is great for pure use cases (lambda bot). But that doesn't depend on being able to write arbitrary IO code inside the Safe bubble, does it? In fact *all* of IO could be outside the safe boundary for this use case, could it not? Are there any existing cases where it is important to be able to build up unsafe IO values inside -XSafe code?

Edward, why does it seem like a losing proposition? Are there further problems that come to mind? ezyang mentioned the subprocess problem. I don't have a strong opinion on that one. But I tend to think the safe IO language *should* allow subprocess calls, and its a matter of configuring your OS to not allow ptrace in that situation. This would be part of a set of requirements for how to compile and launch a complete "Safe Haskell" *program* in order to get a guarantee.

My primary interest is actually not segfault-freedom, per-se, but being able to define a memory model for Safe Haskell (for which I'd suggest sequential consistency). FFI undermines that, and peek/poke seems like it should cluster with FFI as an unsafe feature. I'm not inclined to give a memory model to peek or FFI -- at that level you get what the architecture gives you -- but I do want a memory model for IORefs, IOVectors, etc.

We're poking at the Stackage package set now to figure out what pressure point to push on to increase the percentage of Stackage that is Safe. I'll be able to say more when we have more data on dependencies and problem points. Across all of hackage, Safe Haskell has modest use: of the ~100K modules on Hackage, ~636 are marked Safe, ~874 trustworthy, and ~118 Unsafe. It should be easy to check if any of this Safe code is currently importing "Foreign.*" or using FFI.

My general plea is that we not give the imperative partition of Haskell too much the short end of the stick [1]. There is oodles of code in IO (or MonadIO), and probably relatively little in "RIO". To my knowledge, we don't have great ways to coin "RIO" newtypes without having to wrap and reexport rather a lot of IO functions. Maybe if APIs like MVars or files were overloaded in a class then GND could do some of the work...

-Ryan

[1] In safety guarantees, in optimizations, primops, whatever... For instance, I find in microbenchmarks that IO code still runs 2X slower than pure code, even if no IO effects are performed.

On Tue, Aug 9, 2016 at 5:13 PM, Edward Kmett wrote:

...

I've always treated Safe Haskell as "Safe until you allow IO" -- in that all 'evil' things get tainted by an IO type that you can't get rid of by the usual means. So if you go to run pure Safe Haskell code in say, lambdabot, which doesn't give the user a means to execute IO, it can't segfault if all of the Trustworthy modules you depend upon actually are trustworthy.

Trying to shore up segfault safety under Safe in IO seems like a losing proposition.

-Edward

On Mon, Aug 8, 2016 at 1:27 PM, Ryan Newton wrote:

...

We're trying to spend some cycles pushing on Safe Haskell within the stackage packages. (It's looking like a slog.)

But we're running up against some basic questions regarding the core packages and Safe Haskell guarantees. The manual currently says: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/safe_haskell...

*Functions in the IO monad are still allowed and behave as usual. * As usual? So it is ok to segfault GHC? Elsewhere it says "in the safe language you can trust the types", and I'd always assumed that meant Safe Haskell is a type safe language, even in the IO fragment.

Was there an explicit decision to allow segfaults and memory corruption? This can happen not just with FFI calls but with uses of Ptrs within Haskell, for example the following:

```

{-# LANGUAGE Safe #-}

module Main where

import Foreign.Marshal.Alloc

import Foreign.Storable

import Foreign.Ptr

import System.Random

fn :: Ptr Int -> IO ()

fn p = do

-- This is kosher:

poke p 3

print =<< peek p

-- This should crash the system:

ix <- randomIO

pokeElemOff p ix 0xcc

main = alloca fn

```

-Ryan

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