Hi Simon,

On Wed, Aug 10, 2016 at 4:24 AM, Simon Marlow <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 approach 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:

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