Is Safe Haskell intended to allow segfaults?
rrnewton at gmail.com
Wed Aug 10 20:48:30 UTC 2016
On Wed, Aug 10, 2016 at 4:24 AM, Simon Marlow <marlowsd at gmail.com
> Definining a safe subset of IO is usually an application-specific
> decision, e.g. do you want to allow access to the filesystem but without
> allowing openFile "/dev/mem"? It's a minefield.
I respect your intuition that this is a "minefield" (and Edward's "big
mess"), but I still want to unpack this further.
I would propose that a MemSafe app is a two-part contract that is half an
OS responsibility and half language/runtime responsibility.
1. OS: guarantee that all system calls (including file access) from the
process do not violate the processes memory, outside of certain opt-in DMA
2. Lang/runtime: create a binary "ensuring" that all instructions
executed in the process maintain the type safety of memory and follow the
memory model. (Scare quotes due to large TCB.)
With this division, "/dev/mem" and subprocess/ptrace are definitely the job
of the OS or containerization. Blame for a bug would fall to category 1.
A MemSafe app needs a launcher/harness to check that category 1 is enforced
properly. I'm not proposing that GHC needs to generate that. It should be
Ryan, if you want to give an operational semantics for memory in IO, why
> not start from the subset of IO that you can accurately model - the basic
> IO structure together with a set of primitives - and define the semantics
> for that? That's typically what we do when we're talking about something
> in the IO monad.
Yes, indeed, that has been the
approach <http://homepages.dcc.ufmg.br/~camarao/fp/articles/lazy-state.pdf> for
decades (and the same thing you and I do with other monads like Par
There's something unsatisfying here though -- we love to build model
languages that include the effects we want to talk about *at that time* --
perhaps just MVars, just putChar, or just STM. But of course there's a big
leap from these small treatments to GHC, with its multitude of moving
parts. That's partly why I think SafeHaskell is so great; it's a Full
Language which aims for serious, statically enforced guarantees.
Well, almost a full language ;-). You can't run programs in it, unless you
*extend* the TCB. It's kind of like Rust if you were required to use an
"unsafe" block to write main().
Anyway, here's a draft paper that does propose a small model language. It
adds a memory model to Haskell plus IORefs/STRefs/TVars, and explains how,
when executed on a machine with relaxed TSO memory (store buffers), the IO
writes need to be fenced, but the ST and STM ones don't:
Do we need a memory model? I concur with David Terei's arguments from 5
Note however, that the implementation in this paper is TSO only.
Implementation on ARM would be a bit different, but the relationship
between IO/ST and IO/STM would stay the same.
Ryan Yates & others, I'm curious if you think the treatment of STM is
satisfactory. Like ppopp05, we do not model retrying explicitly, and our
goal here is to show the interaction of the different effects.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the ghc-devs