From aa7c872724e0d9bb79520152d613085c92d67236 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 19 Mar 2014 14:13:20 +0100 Subject: STM: when an error occurs in a worker send back a bunch of states In this way when the user fixes the script only a small part of the broken proof has to be recomputed on master. The density of states sent back decreases as they get far from the error. I.e. counting from the error, the worker sends back states at distance 0 1 2 3 5 7 10 14 19 26 35 47... --- toplevel/stm.ml | 35 ++++++++++++++++++++++++++--------- 1 file changed, 26 insertions(+), 9 deletions(-) diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 4f8149229..e7597a1b7 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -206,6 +206,7 @@ module VCS : sig val reached : id -> bool -> unit val goals : id -> int -> unit val set_state : id -> state -> unit + val get_state : id -> state option val forget_state : id -> unit (* cuts from start -> stop, raising Expired if some nodes are not there *) @@ -359,6 +360,7 @@ end = struct (* {{{ *) | Some x -> x | None -> raise Vcs_aux.Expired let set_state id s = (get_info id).state <- Some s + let get_state id = (get_info id).state let forget_state id = (get_info id).state <- None let reached id b = let info = get_info id in @@ -554,7 +556,7 @@ end = struct (* {{{ *) with VCS.Expired -> anomaly (str "not a cached state (expired)") let assign id s = - try VCS.set_state id s + try if VCS.get_state id = None then VCS.set_state id s with VCS.Expired -> () let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable) @@ -680,8 +682,9 @@ end = struct (* {{{ *) type response = | RespBuiltProof of Entries.proof_output list * float - | RespError of (* err, safe, msg, safe_state *) - Stateid.t * Stateid.t * std_ppcmds * State.frozen_state option + | RespError of (* err, safe, msg, safe_states *) + Stateid.t * Stateid.t * std_ppcmds * + (Stateid.t * State.frozen_state) list | RespFeedback of Interface.feedback | RespGetCounterFreshLocalUniv | RespGetCounterNewUnivLevel @@ -967,10 +970,10 @@ end = struct (* {{{ *) last_task := None; raise KillRespawn | TaskBuildProof(_,_,_, assign,_,_,_,_), - RespError(err_id,valid,e,s) -> + RespError(err_id,valid,e,valid_states) -> let e = Stateid.add ~valid (RemoteException e) err_id in assign (`Exn e); - Option.iter (State.assign valid) s; + List.iter (fun (id,s) -> State.assign id s) valid_states; (* We restart the slave, to avoid memory leaks. We could just Pp.feedback (Interface.InProgress ~-1) *) last_task := None; @@ -1110,10 +1113,24 @@ end = struct (* {{{ *) prerr_endline (string_of_ppcmds (print e)); prerr_endline ("last safe id is: " ^ Stateid.to_string safe_id); prerr_endline ("cached? " ^ string_of_bool (State.is_cached safe_id)); - let state = - if State.is_cached safe_id then Some (State.get_cached safe_id) - else None in - marshal_response !slave_oc (RespError (err_id, safe_id, print e, state)) + let prog old_v n = + if n < 3 then n else old_v + n/3 + if n mod 3 > 0 then 1 else 0 in + let states = + let open State in + let rec aux n m prev_id = + let next = + try Some (VCS.visit prev_id).next + with VCS.Expired -> None in + match next with + | None -> [] + | Some id when n = m -> + prerr_endline ("sending back state " ^ string_of_int m); + let tail = aux (n+1) (prog m (n+1)) id in + if is_cached id then (id, get_cached id) :: tail else tail + | Some id -> aux (n+1) m id in + (if is_cached safe_id then [safe_id,get_cached safe_id] else []) + @ aux 1 (prog 1 1) safe_id in + marshal_response !slave_oc (RespError(err_id, safe_id, print e, states)) | e -> pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e)); flush_all (); exit 1 -- cgit v1.2.3