From 280be11cb4706e039cf4e9f68a5ae38b0aef9340 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 28 May 2017 00:35:57 +0200 Subject: [stm] Remove state-handling from Futures. We make Vernacentries.interp functional wrt state, and thus remove state-handling from `Future`. Now, a future needs a closure if it wants to preserve state. Consequently, `Vernacentries.interp` takes a state, and returns the new one. We don't explicitly thread the state in the STM yet, instead, we recover the state that was used before and pass it explicitly to `interp`. I have tested the commit with the files in interactive, but we aware that some new bugs may appear or old ones be made more apparent. However, I am confident that this step will improve our understanding of bugs. In some cases, we perform a bit more summary wrapping/unwrapping. This will go away in future commits; informal timings for a full make: - master: real 2m11,027s user 8m30,904s sys 1m0,000s - no_futures: real 2m8,474s user 8m34,380s sys 0m59,156s --- lib/future.ml | 82 ++++++++++++++++------------------------------------------- 1 file changed, 22 insertions(+), 60 deletions(-) (limited to 'lib/future.ml') diff --git a/lib/future.ml b/lib/future.ml index d9463aa0f..09285ea27 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -6,12 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* To deal with side effects we have to save/restore the system state *) -type freeze -let freeze = ref (fun () -> assert false : unit -> freeze) -let unfreeze = ref (fun _ -> () : freeze -> unit) -let set_freeze f g = freeze := f; unfreeze := g - let not_ready_msg = ref (fun name -> Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^ "Please wait or pass "^ @@ -30,6 +24,7 @@ let customize_not_here_msg f = not_here_msg := f exception NotReady of string exception NotHere of string + let _ = CErrors.register_handler (function | NotReady name -> !not_ready_msg name | NotHere name -> !not_here_msg name @@ -59,7 +54,7 @@ type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computat and 'a comp = | Delegated of (unit -> unit) | Closure of (unit -> 'a) - | Val of 'a * freeze option + | Val of 'a | Exn of Exninfo.iexn (* Invariant: this exception is always "fixed" as in fix_exn *) and 'a comput = @@ -74,7 +69,7 @@ let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x = ref (Ongoing (name, CEphemeron.create (uuid, f, Pervasives.ref x))) let get x = match !x with - | Finished v -> unnamed, UUID.invalid, id, ref (Val (v,None)) + | Finished v -> unnamed, UUID.invalid, id, ref (Val v) | Ongoing (name, x) -> try let uuid, fix, c = CEphemeron.get x in name, uuid, fix, c with CEphemeron.InvalidKey -> @@ -95,13 +90,13 @@ let is_exn kx = let _, _, _, x = get kx in match !x with | Val _ | Closure _ | Delegated _ -> false let peek_val kx = let _, _, _, x = get kx in match !x with - | Val (v, _) -> Some v + | Val v -> Some v | Exn _ | Closure _ | Delegated _ -> None let uuid kx = let _, id, _, _ = get kx in id -let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None)) -let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ()))) +let from_val ?(fix_exn=id) v = create fix_exn (Val v) +let from_here ?(fix_exn=id) v = create fix_exn (Val v) let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn @@ -110,7 +105,7 @@ let create_delegate ?(blocking=true) ~name fix_exn = let _, _, fix_exn, c = get ck in assert (match !c with Delegated _ -> true | _ -> false); begin match v with - | `Val v -> c := Val (v, None) + | `Val v -> c := Val v | `Exn e -> c := Exn (fix_exn e) | `Comp f -> let _, _, _, comp = get f in c := !comp end; signal () in @@ -124,17 +119,16 @@ let create_delegate ?(blocking=true) ~name fix_exn = ck, assignement signal ck (* TODO: get rid of try/catch to be stackless *) -let rec compute ~pure ck : 'a value = +let rec compute ck : 'a value = let _, _, fix_exn, c = get ck in match !c with - | Val (x, _) -> `Val x + | Val x -> `Val x | Exn (e, info) -> `Exn (e, info) - | Delegated wait -> wait (); compute ~pure ck + | Delegated wait -> wait (); compute ck | Closure f -> try let data = f () in - let state = if pure then None else Some (!freeze ()) in - c := Val (data, state); `Val data + c := Val data; `Val data with e -> let e = CErrors.push e in let e = fix_exn e in @@ -142,60 +136,30 @@ let rec compute ~pure ck : 'a value = | (NotReady _, _) -> `Exn e | _ -> c := Exn e; `Exn e -let force ~pure x = match compute ~pure x with +let force x = match compute x with | `Val v -> v | `Exn e -> Exninfo.iraise e -let chain ~pure ck f = +let chain ck f = let name, uuid, fix_exn, c = get ck in create ~uuid ~name fix_exn (match !c with - | Closure _ | Delegated _ -> Closure (fun () -> f (force ~pure ck)) + | Closure _ | Delegated _ -> Closure (fun () -> f (force ck)) | Exn _ as x -> x - | Val (v, None) when pure -> Val (f v, None) - | Val (v, Some _) when pure -> Val (f v, None) - | Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v) - | Val (v, None) -> - match !ck with - | Finished _ -> CErrors.anomaly(Pp.str - "Future.chain ~pure:false call on an already joined computation.") - | Ongoing _ -> CErrors.anomaly(Pp.strbrk( - "Future.chain ~pure:false call on a pure computation. "^ - "This can happen if the computation was initial created with "^ - "Future.from_val or if it was Future.chain ~pure:true with a "^ - "function and later forced."))) + | Val v -> Val (f v)) let create fix_exn f = create fix_exn (Closure f) let replace kx y = let _, _, _, x = get kx in match !x with - | Exn _ -> x := Closure (fun () -> force ~pure:false y) + | Exn _ -> x := Closure (fun () -> force y) | _ -> CErrors.anomaly (Pp.str "A computation can be replaced only if is_exn holds.") -let purify f x = - let state = !freeze () in - try - let v = f x in - !unfreeze state; - v - with e -> - let e = CErrors.push e in !unfreeze state; Exninfo.iraise e - -let transactify f x = - let state = !freeze () in - try f x - with e -> - let e = CErrors.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 -let force ~pure x = purify_future (force ~pure) x -let chain ~pure x f = - let y = chain ~pure x f in - if is_over x then ignore(force ~pure y); +let chain x f = + let y = chain x f in + if is_over x then ignore(force y); y -let force x = force ~pure:false x let join kx = let v = force kx in @@ -205,12 +169,11 @@ let join kx = let sink kx = if is_val kx then ignore(join kx) let split2 x = - chain ~pure:true x (fun x -> fst x), - chain ~pure:true x (fun x -> snd x) + chain x (fun x -> fst x), chain x (fun x -> snd x) let map2 f x l = CList.map_i (fun i y -> - let xi = chain ~pure:true x (fun x -> + let xi = chain x (fun x -> try List.nth x i with Failure _ | Invalid_argument _ -> CErrors.anomaly (Pp.str "Future.map2 length mismatch.")) in @@ -226,6 +189,5 @@ let print f kx = match !x with | Delegated _ -> str "Delegated" ++ uid | 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) + | Val x -> str "PureVal" ++ uid ++ spc () ++ hov 0 (f x) | Exn (e, _) -> str "Exn" ++ uid ++ spc () ++ hov 0 (str (Printexc.to_string e)) -- cgit v1.2.3