Is Safe Haskell intended to allow segfaults?

[Ryan Newton]

Hi Simon,

On Wed, Aug 10, 2016 at 4:24 AM, Simon Marlow <marlowsd at gmail.com
<https://mail.google.com/mail/?view=cm&fs=1&tf=1&to=marlowsd@gmail.com>>
wrote:

> 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
   regions.
   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
separate.

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
<http://research.microsoft.com/en-us/um/people/simonpj/papers/concurrent-haskell.pdf>
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
<http://research.microsoft.com/en-us/um/people/simonpj/papers/parallel/monad-par.pdf>).
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:

   http://www.cs.indiana.edu/~rrnewton/papers/sc-haskell_draft.pdf

Do we need a memory model?  I concur with David Terei's arguments from 5
years ago
<https://mail.haskell.org/pipermail/haskell-cafe/2011-May/091963.html>.
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.

Cheers,
  -Ryan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160810/2666eb42/attachment.html>