From 7cfcaa57a68ea9abde9e2558ceef86589aa26d6d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 8 Oct 2014 17:28:18 +0200 Subject: STM: primitives to snapshot a .vi while in interactive mode --- lib/future.ml | 1 + lib/future.mli | 1 + lib/remoteCounter.ml | 3 ++ lib/remoteCounter.mli | 3 ++ lib/stateid.ml | 9 +++++ lib/stateid.mli | 10 ++++++ library/library.ml | 46 +++++++++++++++++-------- library/library.mli | 3 +- stm/asyncTaskQueue.ml | 12 +++++-- stm/asyncTaskQueue.mli | 7 +++- stm/stm.ml | 92 +++++++++++++++++++++++++------------------------- stm/stm.mli | 19 ++++++++--- stm/tQueue.ml | 9 ----- stm/tQueue.mli | 3 -- toplevel/vernac.ml | 4 +-- 15 files changed, 137 insertions(+), 85 deletions(-) diff --git a/lib/future.ml b/lib/future.ml index 6ebbd4b1d..4437cec84 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -41,6 +41,7 @@ module UUID = struct end module UUIDMap = Map.Make(UUID) +module UUIDSet = Set.Make(UUID) type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation] diff --git a/lib/future.mli b/lib/future.mli index 18b014132..a03823af8 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -61,6 +61,7 @@ module UUID : sig end module UUIDMap : Map.S with type key = UUID.t +module UUIDSet : Set.S with type elt = UUID.t exception NotReady diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml index 72887b21a..c0217b22e 100644 --- a/lib/remoteCounter.ml +++ b/lib/remoteCounter.ml @@ -37,6 +37,9 @@ let new_counter ~name a ~incr ~build = let backup () = !counters +let snapshot () = + List.map (fun (n,v) -> n, Obj.repr (ref (ref !!(Obj.obj v)))) !counters + let restore l = List.iter (fun (name, data) -> assert(List.mem_assoc name !counters); diff --git a/lib/remoteCounter.mli b/lib/remoteCounter.mli index 5a47ba663..18e6b6b59 100644 --- a/lib/remoteCounter.mli +++ b/lib/remoteCounter.mli @@ -20,4 +20,7 @@ val new_counter : name:string -> type remote_counters_status val backup : unit -> remote_counters_status +(* like backup but makes a copy so that further increment does not alter + * the snapshot *) +val snapshot : unit -> remote_counters_status val restore : remote_counters_status -> unit diff --git a/lib/stateid.ml b/lib/stateid.ml index 09cc2b7e8..59cf206e2 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -39,3 +39,12 @@ let compare = Int.compare module Set = Set.Make(struct type t = int let compare = compare end) +type ('a,'b) request = { + exn_info : t * t; + stop : t; + document : 'b; + loc : Loc.t; + uuid : 'a; + name : string +} + diff --git a/lib/stateid.mli b/lib/stateid.mli index 11fac7a92..341544a67 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -33,3 +33,13 @@ val of_xml : xml -> t * The initial_state_id is assumed to be safe. *) val add : exn -> ?valid:t -> t -> exn val get : exn -> (t * t) option + +type ('a,'b) request = { + exn_info : t * t; + stop : t; + document : 'b; + loc : Loc.t; + uuid : 'a; + name : string +} + diff --git a/library/library.ml b/library/library.ml index 7f5ca5af6..ceadb3ace 100644 --- a/library/library.ml +++ b/library/library.ml @@ -670,19 +670,35 @@ let error_recursively_dependent_library dir = writing the content and computing the checksum... *) let save_library_to ?todo dir f otab = - let f, todo, utab, dtab = - match todo with + let f, except = match todo with | None -> assert(!Flags.compilation_mode = Flags.BuildVo); - f ^ "o", (fun _ -> None), (fun _ -> None), (fun _ -> None) - | Some d -> - assert(!Flags.compilation_mode = Flags.BuildVi); - f ^ "i", (fun x -> Some (d x)), - (fun x -> Some (x,Univ.ContextSet.empty,false)), (fun x -> Some x) in - let cenv, seg, ast = Declaremods.end_library dir in + f ^ "o", Future.UUIDSet.empty + | Some (l,_) -> + f ^ "i", + List.fold_left (fun e r -> Future.UUIDSet.add r.Stateid.uuid e) + Future.UUIDSet.empty l in + let cenv, seg, ast = Declaremods.end_library ~except dir in let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in - assert(!Flags.compilation_mode = Flags.BuildVi || - Array.for_all Future.is_val opaque_table); + let tasks, utab, dtab = + match todo with + | None -> None, None, None + | Some (tasks, rcbackup) -> + let tasks = + List.map Stateid.(fun r -> + { r with uuid = Future.UUIDMap.find r.uuid f2t_map }) tasks in + Some (tasks,rcbackup), + Some (univ_table,Univ.ContextSet.empty,false), + Some disch_table in + let except = + Future.UUIDSet.fold (fun uuid acc -> + Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc) + except Int.Set.empty in + let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in + Array.iteri (fun i x -> + if not(is_done_or_todo i x) then Errors.errorlabstrm "library" + Pp.(str"Proof object "++int i++str" is not checked nor to be checked")) + opaque_table; let md = { md_name = dir; md_compiled = cenv; @@ -695,11 +711,11 @@ let save_library_to ?todo dir f otab = let (f',ch) = raw_extern_library f in try (* Writing vo payload *) - System.marshal_out_segment f' ch (md : seg_lib); - System.marshal_out_segment f' ch (utab univ_table : seg_univ option); - System.marshal_out_segment f' ch (dtab disch_table : seg_discharge option); - System.marshal_out_segment f' ch (todo f2t_map : 'tasks option); - System.marshal_out_segment f' ch (opaque_table : seg_proofs); + System.marshal_out_segment f' ch (md : seg_lib); + System.marshal_out_segment f' ch (utab : seg_univ option); + System.marshal_out_segment f' ch (dtab : seg_discharge option); + System.marshal_out_segment f' ch (tasks : 'tasks option); + System.marshal_out_segment f' ch (opaque_table : seg_proofs); close_out ch; (* Writing native code files *) if not !Flags.no_native_compiler then diff --git a/library/library.mli b/library/library.mli index c92b9d623..9e914d9bb 100644 --- a/library/library.mli +++ b/library/library.mli @@ -43,7 +43,8 @@ val import_module : bool -> qualid located -> unit val start_library : string -> DirPath.t * string (** {6 End the compilation of a library and save it to a ".vo" file } *) -val save_library_to : ?todo:(int Future.UUIDMap.t -> 'tasks) -> +val save_library_to : + ?todo:((Future.UUID.t,'document) Stateid.request list * 'counters) -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit val load_library_todo : diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 74e83a39f..22e7c0243 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -304,13 +304,19 @@ module Make(T : Task) = struct flush_all (); exit 1 done - let dump () = - assert(WorkersPool.is_empty ()); (* ATM, we allow that only if no slaves *) - List.map fst (TQueue.dump queue) + let clear () = + assert(WorkersPool.is_empty ()); (* We allow that only if no slaves *) + TQueue.clear queue + + let snapshot () = + List.map fst + (TQueue.wait_until_n_are_waiting_then_snapshot + (WorkersPool.n_workers ()) queue) let init n = WorkersPool.init n manage_slave (fun n -> Printf.sprintf "%s:%d" T.name n) + let destroy () = WorkersPool.destroy (); TQueue.destroy queue diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli index ddbb28457..cd91ba129 100644 --- a/stm/asyncTaskQueue.mli +++ b/stm/asyncTaskQueue.mli @@ -61,6 +61,11 @@ module Make(T : Task) : sig val set_order : (T.task -> T.task -> int) -> unit - val dump : unit -> T.task list + (* Take a snapshot (non destructive but waits until all workers are + * enqueued) *) + val snapshot : unit -> T.task list + + (* Clears the queue, only if the worker prool is empty *) + val clear : unit -> unit end diff --git a/stm/stm.ml b/stm/stm.ml index 5349b85a8..026866616 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -701,14 +701,6 @@ let record_pb_time proof_name loc time = hints := Aux_file.set !hints Loc.ghost proof_name proof_build_time end -type 'a a_request = { - r_exn_info : Stateid.t * Stateid.t; - r_stop : Stateid.t; - r_document : VCS.vcs; - r_loc : Loc.t; - r_uuid : 'a; - r_name : string } - exception RemoteException of std_ppcmds let _ = Errors.register_handler (function | RemoteException ppcmd -> ppcmd @@ -730,7 +722,7 @@ module Task = struct t_uuid : Future.UUID.t; t_name : string } - type request = Future.UUID.t a_request + type request = (Future.UUID.t,VCS.vcs) Stateid.request type error = { e_error_at : Stateid.t; @@ -746,17 +738,17 @@ module Task = struct let extra_env () = !async_proofs_workers_extra_env let name_of_task t = t.t_name - let name_of_request r = r.r_name + let name_of_request r = r.Stateid.name let request_of_task age { t_exn_info;t_start;t_stop;t_loc;t_uuid;t_name } = assert(age = `Fresh); try Some { - r_exn_info = t_exn_info; - r_stop = t_stop; - r_document = VCS.slice ~start:t_stop ~stop:t_start; - r_loc = t_loc; - r_uuid = t_uuid; - r_name = t_name } + Stateid.exn_info = t_exn_info; + stop = t_stop; + document = VCS.slice ~start:t_stop ~stop:t_start; + loc = t_loc; + uuid = t_uuid; + name = t_name } with VCS.Expired -> None let use_response { t_assign; t_loc; t_name } = function @@ -795,13 +787,13 @@ module Task = struct Proof_global.return_proof () let build_proof_here (id,valid) loc eop = Future.create (State.exn_on id ~valid) (build_proof_here_core loc eop) - let perform { r_exn_info; r_stop = eop; r_document = vcs; r_loc } = + let perform { Stateid.exn_info; stop = eop; document = vcs; loc } = try VCS.restore vcs; VCS.print (); let rc, time = let wall_clock = Unix.gettimeofday () in - let l = Future.force (build_proof_here r_exn_info r_loc eop) in + let l = Future.force (build_proof_here exn_info loc eop) in l, Unix.gettimeofday () -. wall_clock in VCS.print (); RespBuiltProof(rc,time) @@ -877,18 +869,19 @@ module Slaves : sig val slave_main_loop : (unit -> unit) -> unit val slave_init_stdout : unit -> unit - type tasks - val dump_final : int Future.UUIDMap.t -> tasks - val dump_snapshot : int Future.UUIDMap.t -> tasks - val check_task : string -> tasks -> int -> bool - val info_tasks : tasks -> (string * float * int) list + type 'a tasks = ('a,VCS.vcs) Stateid.request list + val dump_snapshot : unit -> Future.UUID.t tasks + val check_task : string -> int tasks -> int -> bool + val info_tasks : 'a tasks -> (string * float * int) list val finish_task : string -> Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs -> - tasks -> int -> Library.seg_univ + int tasks -> int -> Library.seg_univ val cancel_worker : string -> unit + val reset_task_queue : unit -> unit + val set_perspective : Stateid.t list -> unit end = struct @@ -896,19 +889,19 @@ end = struct module TaskQueue = AsyncTaskQueue.Make(Task) let check_task_aux extra name l i = - let { r_stop; r_document; r_loc; r_name } = List.nth l i in + let { Stateid.stop; document; loc; name = r_name } = List.nth l i in Pp.msg_info( str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name)); - VCS.restore r_document; + VCS.restore document; try - !Task.reach_known_state ~cache:`No r_stop; + !Task.reach_known_state ~cache:`No stop; (* The original terminator, a hook, has not been saved in the .vi*) Proof_global.set_terminator (Lemmas.standard_proof_terminator [] (Lemmas.mk_hook (fun _ _ -> ()))); let proof = Proof_global.close_proof (fun x -> x) in - vernac_interp r_stop ~proof - { verbose = false; loc = r_loc; + vernac_interp stop ~proof + { verbose = false; loc; expr = (VernacEndProof (Proved (true,None))) }; Some proof with e -> @@ -938,7 +931,7 @@ end = struct str (Printexc.to_string e))); None let finish_task name (u,cst,_) d p l i = - let bucket = (List.nth l i).r_uuid in + let bucket = (List.nth l i).Stateid.uuid in match check_task_aux (Printf.sprintf ", bucket %d" bucket) name l i with | None -> exit 1 | Some (po,pt) -> @@ -972,14 +965,14 @@ end = struct | None -> false let info_tasks l = - CList.map_i (fun i { r_loc; r_name } -> + CList.map_i (fun i { Stateid.loc; name } -> let time1 = - try float_of_string (Aux_file.get !hints r_loc "proof_build_time") + try float_of_string (Aux_file.get !hints loc "proof_build_time") with Not_found -> 0.0 in let time2 = - try float_of_string (Aux_file.get !hints r_loc "proof_check_time") + try float_of_string (Aux_file.get !hints loc "proof_check_time") with Not_found -> 0.0 in - r_name, max (time1 +. time2) 0.0001,i) 0 l + name, max (time1 +. time2) 0.0001,i) 0 l let set_perspective idl = let open Stateid in @@ -1024,17 +1017,13 @@ end = struct let cancel_worker = TaskQueue.cancel_worker (* For external users this name is nicer than request *) - type tasks = int a_request list - let dump f2t_map = - let tasks = TaskQueue.dump () in - prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length tasks)); - List.map (function r -> { r with r_uuid = Future.UUIDMap.find r.r_uuid f2t_map }) - (CList.map_filter (Task.request_of_task `Fresh) tasks) - let dump_snapshot f2t_map = + type 'a tasks = ('a,VCS.vcs) Stateid.request list + let dump_snapshot () = let tasks = TaskQueue.snapshot () in prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length tasks)); - List.map (function r -> { r with r_uuid = Future.UUIDMap.find r.r_uuid f2t_map }) - (CList.map_filter (Task.request_of_task `Fresh) tasks) + CList.map_filter (Task.request_of_task `Fresh) tasks + + let reset_task_queue () = TaskQueue.clear () end @@ -1236,7 +1225,8 @@ let collect_proof keep cur hd brkind id = else `Sync (name,proof_using_ast last,`Policy) | `Fork (_, hd', GuaranteesOpacity, ids) when has_proof_no_using last && not (State.is_cached (parent last)) && - !Flags.compilation_mode = Flags.BuildVi -> + (!Flags.compilation_mode = Flags.BuildVi || + !Flags.async_proofs_always_delegate) -> (try let name = name ids in let hint, time = get_hint_ctx loc, get_hint_bp_time name in @@ -1602,8 +1592,9 @@ let join () = VCS.print (); VCS.print () -type tasks = Slaves.tasks * RemoteCounter.remote_counters_status -let dump x = Slaves.dump x, RemoteCounter.backup () +let dump_snapshot () = Slaves.dump_snapshot (), RemoteCounter.snapshot () +type document = VCS.vcs +type tasks = int Slaves.tasks * RemoteCounter.remote_counters_status let check_task name (tasks,rcbackup) i = RemoteCounter.restore rcbackup; let vcs = VCS.backup () in @@ -1683,6 +1674,15 @@ let handle_failure e vcs tty = VCS.print (); raise e +let snapshot_vi ldir long_f_dot_v = + finish (); + if List.length (VCS.branches ()) > 1 then + Errors.errorlabstrm "stm" (str"Cannot dump a vi with open proofs"); + Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_v + (Global.opaque_tables ()) + +let reset_task_queue = Slaves.reset_task_queue + let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = let warn_if_pos a b = if b then msg_warning(pr_ast a ++ str" should not be part of a script") in diff --git a/stm/stm.mli b/stm/stm.mli index d77c19cfb..c4664a67c 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -46,16 +46,25 @@ val stop_worker : string -> unit (* Joins the entire document. Implies finish, but also checks proofs *) val join : unit -> unit -(* To save to disk an incomplete document *) -type tasks -val dump_final : int Future.UUIDMap.t -> tasks -val dump_snapshot : int Future.UUIDMap.t -> tasks +(* Saves on the dist a .vi corresponding to the current status: + - if the worker prool is empty, all tasks are saved + - if the worker proof is not empty, then it waits until all workers + are done with their current jobs and then dumps (or fails if one + of the completed tasks is a failuere) *) +val snapshot_vi : DirPath.t -> string -> unit + +(* Empties the task queue, can be used only if the worker pool is empty (E.g. + * after having built a .vi in batch mode *) +val reset_task_queue : unit -> unit + +(* A .vi contains tasks to be completed *) +type tasks val check_task : string -> tasks -> int -> bool val info_tasks : tasks -> (string * float * int) list val finish_tasks : string -> Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs -> - tasks -> Library.seg_univ * Library.seg_proofs + tasks -> Library.seg_univ * Library.seg_proofs (* Id of the tip of the current branch *) val get_current_state : unit -> Stateid.t diff --git a/stm/tQueue.ml b/stm/tQueue.ml index fe9cf015a..04e4e81f9 100644 --- a/stm/tQueue.ml +++ b/stm/tQueue.ml @@ -103,15 +103,6 @@ let wait_until_n_are_waiting_and_queue_empty j tq = done; Mutex.unlock tq.lock -let dump { queue; lock } = - let l = ref [] in - Mutex.lock lock; - while not (PriorityQueue.is_empty queue) do - l := PriorityQueue.pop queue :: !l - done; - Mutex.unlock lock; - List.rev !l - let wait_until_n_are_waiting_then_snapshot j tq = let l = ref [] in Mutex.lock tq.lock; diff --git a/stm/tQueue.mli b/stm/tQueue.mli index abb14f969..230ce032a 100644 --- a/stm/tQueue.mli +++ b/stm/tQueue.mli @@ -15,9 +15,6 @@ val push : 'a t -> 'a -> unit val set_order : 'a t -> ('a -> 'a -> int) -> unit val wait_until_n_are_waiting_and_queue_empty : int -> 'a t -> unit -(* also empties the queue *) -val dump : 'a t -> 'a list - (* Non destructive *) val wait_until_n_are_waiting_then_snapshot : int -> 'a t -> 'a list diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index dcce58199..b56b515dc 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -333,8 +333,8 @@ let compile verbosely f = let _ = load_vernac verbosely long_f_dot_v in Stm.finish (); check_pending_proofs (); - Library.save_library_to ~todo:Stm.dump_final ldir long_f_dot_v - (Global.opaque_tables ()) + Stm.snapshot_vi ldir long_f_dot_v; + Stm.reset_task_queue () | Vi2Vo -> let open Filename in let open Library in -- cgit v1.2.3