diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-03 20:34:09 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-16 13:15:12 +0100 |
commit | bff51607cfdda137d7bc55d802895d7f794d5768 (patch) | |
tree | 1a159136a88ddc6561b814fb4ecbacdf9de0dd70 /lib/future.ml | |
parent | 37ed28dfe253615729763b5d81a533094fb5425e (diff) |
Getting rid of Exninfo hacks.
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
Diffstat (limited to 'lib/future.ml')
-rw-r--r-- | lib/future.ml | 25 |
1 files changed, 14 insertions, 11 deletions
diff --git a/lib/future.ml b/lib/future.ml index b851f912c..52a060c93 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -26,7 +26,7 @@ let _ = Errors.register_handler (function "asynchronous script processing.") | _ -> raise Errors.Unhandled) -type fix_exn = exn -> exn +type fix_exn = Exninfo.iexn -> Exninfo.iexn let id x = prerr_endline "Future: no fix_exn.\nYou have probably created a Future.computation from a value without passing the ~fix_exn argument. You probably want to chain with an already existing future instead."; x module UUID = struct @@ -43,7 +43,7 @@ end module UUIDMap = Map.Make(UUID) module UUIDSet = Set.Make(UUID) -type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation] +type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] (* Val is not necessarily a final state, so the computation restarts from the state stocked into Val *) @@ -51,7 +51,7 @@ and 'a comp = | Delegated of (unit -> unit) | Closure of (unit -> 'a) | Val of 'a * Dyn.t option - | Exn of exn (* Invariant: this exception is always "fixed" as in fix_exn *) + | Exn of Exninfo.iexn (* Invariant: this exception is always "fixed" as in fix_exn *) and 'a comput = | Ongoing of (UUID.t * fix_exn * 'a comp ref) Ephemeron.key @@ -66,9 +66,10 @@ let get x = | Finished v -> UUID.invalid, id, ref (Val (v,None)) | Ongoing x -> try Ephemeron.get x - with Ephemeron.InvalidKey -> UUID.invalid, id, ref (Exn NotHere) + with Ephemeron.InvalidKey -> + UUID.invalid, id, ref (Exn (NotHere, Exninfo.null)) -type 'a value = [ `Val of 'a | `Exn of exn ] +type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn ] let is_over kx = let _, _, x = get kx in match !x with | Val _ | Exn _ -> true @@ -116,7 +117,7 @@ let rec compute ~pure ck : 'a value = let _, fix_exn, c = get ck in match !c with | Val (x, _) -> `Val x - | Exn e -> `Exn e + | Exn (e, info) -> `Exn (e, info) | Delegated wait -> wait (); compute ~pure ck | Closure f -> try @@ -127,12 +128,12 @@ let rec compute ~pure ck : 'a value = let e = Errors.push e in let e = fix_exn e in match e with - | NotReady -> `Exn e + | (NotReady, _) -> `Exn e | _ -> c := Exn e; `Exn e let force ~pure x = match compute ~pure x with | `Val v -> v - | `Exn e -> raise e + | `Exn e -> Exninfo.iraise e let chain ~pure ck f = let uuid, fix_exn, c = get ck in @@ -167,12 +168,14 @@ let purify f x = let v = f x in !unfreeze state; v - with e -> let e = Errors.push e in !unfreeze state; raise e + with e -> + let e = Errors.push e in !unfreeze state; Exninfo.iraise e let transactify f x = let state = !freeze () in try f x - with e -> let e = Errors.push e in !unfreeze state; raise e + with e -> + let e = Errors.push e in !unfreeze state; Exninfo.iraise e let purify_future f x = if is_over x then f x else purify f x let compute x = purify_future (compute ~pure:false) x @@ -214,4 +217,4 @@ let print f kx = | Closure _ -> str "Closure" ++ uid | Val (x, None) -> str "PureVal" ++ uid ++ spc () ++ hov 0 (f x) | Val (x, Some _) -> str "StateVal" ++ uid ++ spc () ++ hov 0 (f x) - | Exn e -> str "Exn" ++ uid ++ spc () ++ hov 0 (str (Printexc.to_string e)) + | Exn (e, _) -> str "Exn" ++ uid ++ spc () ++ hov 0 (str (Printexc.to_string e)) |