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

[Daniel BÃnzli <daniel.buenzli@xxxxxxxxxxxx>]

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