Xen project Mailing List

On Tue, Feb 3, 2015 at 4:41 PM, Daniel BÃnzli <daniel.buenzli@xxxxxxxxxxxx> wrote:

Sorry, somehow I missed that message.

> Sure, but I don't see what difference any of this cancellation stuff
> makes. Layering a second error monad on top of Lwt won't un-break
> cancellation.

Right. There may be ways of trying to reimplement a sane cancellation API on top of the existing one though.

> So, whether we continue to use Lwt.cancel or not, I don't see it as an
> argument for separating error handling out of Lwt.

The argument here is to explicitly know what can happen when you invoke things and hence facilitate 1) the knowledge of their existence without resorting to documentation (which is sadly never written) 2) their *correct* handling if needed.

> But the real problem here is that by making exceptions fatal we turn
> every exception used in existing OCaml code into a security
> vulnerability. To kill my service, an attacker only needs to find some
> way of triggering some code path to throw an exception.

Right we can't do that. I'd suggest the strategy should be for programmers to:

1) Always handle exceptions without restoring to lwt's failed state (i.e. everything except Invalid_argument, Out_of_memory and Division_by_zero).

2) Provide an exception trap abstraction to be used at appropriate points to prevent Unikernel termination on uncaught exceptions. Here I would suggest to try to make the use of the trap *show up in the types* so that mirage signatures could enforce trap usage on implementations and thus provide clear safety checkpoints.

> - If I accepted XML, they could send invalid XML (even xmlm throws).
Yes. Side note, the fact that xmlm throws is a design error, I'm very ashamed of that library. See Jsonm for a better-behaved design (basically `('a, 'b) result`).

> OK, but how? Do you have a concrete proposal? What would your error
> monad do differently to Lwt that would make it work where Lwt doesn't?

Lwt's failed state is, like exceptions, completly implicit, it doesn't show in the types what failures can happen. For hints of proposals see previous messages. I think that a lot of people standardized on the `('a, 'b) result` type for a good reason.

> The Lwt error monad uses exceptions as values. It seems like you need some open type
> at any rate, and in 4.01 exceptions are the only option. (a universal
> type works if you give up matching)

Wouldn't `('a, 'b) result` with variant composition and a one sub-level universal type (as suggested in my last message) solve the problem ?

> > I'm really not fond of this. You can use open polymorphic variants for this or a closed one with a few known common cases and a custom one with a printable universal type. But then it seems you are designing with the idea of using Lwt's failed state as an error mechanism which I disagree with.
>
> This is possible, but there are trade-offs:
>
> 1. It's hard to propagate the error when you don't care (99% of the
> cases I suspect). How would you rewrite the bad code you linked above
> in mirage-www with this scheme?

Well using `('a, 'b) result`'s monadic bind.

> 2. How do you attach extra detail to the cases (a universal 'cause'
> nested in each one)?

Yes. Like suggested in the last message.

> 3. You can't match on a printable universal type even if you know the
> concrete implementation.

Implementation should expose the projection function of the universal type. If it wishes your program can then precisely handle the errors of the implementations it knows by testing the universal type with the different projection functions provided by the implementations and return only return generic errors on the ones it doesn't know.

Best,

Daniel

_______________________________________________
MirageOS-devel mailing list
MirageOS-devel@xxxxxxxxxxxxxxxxxxxx
http://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel

Re: [MirageOS-devel] Error handling in Mirage - request for comments!