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

[Christophe Troestler <Christophe.Troestler@xxxxxxxxxxx>]

On Sat, 31 Jan 2015 21:07:22 +0000, Thomas Leonard wrote:
> 
> [â] But the real problem here is that by making exceptions fatal we
> turn every exception used in existing OCaml code into a security
> vulnerability. [â]

Since OCaml supports exceptions, I think there is no doubt that we
must handle them effectively â not just wipe them under the carpet and
let them abort the program/unikernel.  Ideally Lwt should deal
sensibly with exceptions (and the discussion seems to imply there are
areas of improvement â but it is unclear to me how you can do that
efficiently without using a try block in all binds).  So it seems to
me that there is little choice but that exceptions be turned into
failed threads at the programmer's discretion.  Maybe ârunâ should be
renamed ârun_exnâ to indicate that exceptions pass through and the
"safe" run should be

    run : (unit -> 'a t) -> [`Ok of 'a | `Exn of exn]

As it was previously mentioned, I also think that using "error-aware
return types" should be limited mostly to cases where the failure is
not really an error and should be dealt with immediately by the
caller.  And I agree with Thomas when he says that overusing this
scheme will result in errors being ignored instead of being dealt with
properly.

There are however errors that you want to mandate that they are dealt
with but not necessarily at the calling point.  A typical example to
me is âreadâ because it is often much "higher" in the program that an
appropriate response to a failing read can be made â this is important
for libraries that will post-process âreadâs and will have no idea
what to do if âreadâ fails.

To make the discussion a bit more concrete, here is a signature
illustrating how these latter errors may be handled:

    type ('a, 'b) t
    val return : 'a -> ('a, 'b) t
    val ( >>= ) : ('a, 'b) t -> ('a -> ('c, 'b) t) -> ('c, 'b) t
    val fail : ([> ] as 'b) -> (_, 'b) t
    val fail_exn : exn -> ('a, 'b) t
    val catch : ('a, 'b) t -> ('b -> ('a, 'c) t) -> ('a, 'c) t
    val catch_exn : ?exn:(exn -> ('a, 'b) t) -> (unit -> ('a, 'b) t) -> ('a, 
'b) t
    val run : (unit -> ('a, unit) t) -> [`Ok of 'a | `Exn of exn]
    val run_exn : ('a, unit) t -> 'a

Some remarks.  The âfailâ function imposes that the errors are labeled
with polymorphic variants.  Since these are not qualified by the
module and to allow generic treatment, a good idiom would probably be
to use something like â`X of X.errâ where â`Xâ is sufficiently
explicit and âX.errâ enumerates the possible failures for the module
âXâ.  The function âcatch_exn fâ will catch exceptions raised by âfâ
as well as failed-threads ones (by default, only turning all exceptions
into failing thread ones).  The use of âunitâ in â('a, unit) tâ ensures
that the thread is of type â(_, 'b) tâ â i.e. that all errors have
been dealt with â so it can be unified with a non-polymorphic variant
type.

This is similar to declaring

    type ('a, 'b) t = ('a, 'b) Result.t Lwt.t

except that one cannot ditch the âResult.tâ (and one avoids 1
indirection per bind).

Unfortunately, it is some work to ensure that the compiler understands
that all errors were dealt with.  Consider

    let m1 = fail(`X 1) >>= fun x -> fail `Y

Then

    let m2 = catch m1 (function `X x -> return x
                              | e -> fail e)

will not do, you have to write

    let m2 = catch m1 (function `X x -> return x
                              | `Y as e -> fail e)

to make sure âm2â shows that â`Xâ is no longer an issue.  Thus
defining good types to use â#typeâ is important.

My 0.02â,
C.

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