Is Safe Haskell intended to allow segfaults?

[Ryan Newton]

Heh, ok, segfaults themselves are a red herring.  More precisely:

The operational semantics for a SafeIO language should always accurately
model its memory state.  The application should not compute (take a step in
the semantics) in a way that exposes corrupt memory or arbitrary undefined
behavior.  Nor should it violate the memory model.

Moving immediately to the "Terminated" state is fine, whether it be due to
out-of-memory, kill -SEGV, cosmic rays, or hardware failure.  An FFI call
that corrupts memory is bad (may result in arbitrary behavior, not just
termination) as is ptrace'ing.

Naturally, all Unsafe code is part of the TCB, as is the OS and GHC, and
low-level data structure libs and bindings.  It's a big TCB.  Still, it's
something to be able to write an app that doesn't automatically get added
to this TCB just by virtue of being an *app* (main::IO).




On Tue, Aug 9, 2016 at 10:52 PM, Brandon Allbery <allbery.b at gmail.com>
wrote:

> On Tue, Aug 9, 2016 at 4:19 PM, Edward Z. Yang <ezyang at mit.edu> wrote:
>
>> If you can execute subprocesses, you could always spawn gdb to
>> attach via ptrace() to the parent process and then poke around
>> memory.
>>
>
> Don't even need that if you're just talking segfaults, you can always
> spawn a subprocess "kill -SEGV $PPID" :)
>
> Unless you have full control over all the code that could be run in
> subprocesses, it's not going to be safe much less Safe.
>
> --
> brandon s allbery kf8nh                               sine nomine
> associates
> allbery.b at gmail.com
> ballbery at sinenomine.net
> unix, openafs, kerberos, infrastructure, xmonad
> http://sinenomine.net
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160809/5e2d5acf/attachment-0001.html>