diff options
| -rw-r--r-- | engine/univGen.ml | 7 | ||||
| -rw-r--r-- | engine/univGen.mli | 6 | ||||
| -rw-r--r-- | lib/remoteCounter.ml | 52 | ||||
| -rw-r--r-- | lib/remoteCounter.mli | 31 | ||||
| -rw-r--r-- | stm/asyncTaskQueue.ml | 31 | ||||
| -rw-r--r-- | stm/stm.ml | 19 | ||||
| -rw-r--r-- | test-suite/success/RemoteUnivs.v | 31 | ||||
| -rw-r--r-- | vernac/library.ml | 10 | ||||
| -rw-r--r-- | vernac/library.mli | 6 |
9 files changed, 50 insertions, 143 deletions
diff --git a/engine/univGen.ml b/engine/univGen.ml index b98c15f245..b917d91512 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -13,11 +13,10 @@ open Names open Constr open Univ -type univ_unique_id = int (* Generator of levels *) -let new_univ_id, set_remote_new_univ_id = - RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1) - ~build:(fun n -> n) +let new_univ_id = + let cnt = ref 0 in + fun () -> incr cnt; !cnt let new_univ_global () = let s = if Flags.async_proofs_is_worker() then !Flags.async_proofs_worker_id else "" in diff --git a/engine/univGen.mli b/engine/univGen.mli index 05737411f5..743d819747 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -13,12 +13,6 @@ open Constr open Environ open Univ - -(** The global universe counter *) -type univ_unique_id -val set_remote_new_univ_id : univ_unique_id RemoteCounter.installer -val new_univ_id : unit -> univ_unique_id (** for the stm *) - (** Side-effecting functions creating new universe levels. *) val new_univ_global : unit -> Level.UGlobal.t diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml deleted file mode 100644 index 9ea751eef9..0000000000 --- a/lib/remoteCounter.ml +++ /dev/null @@ -1,52 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type 'a getter = unit -> 'a -type 'a installer = ('a getter) -> unit - -type remote_counters_status = (string * Obj.t) list - -let counters : remote_counters_status ref = ref [] - -let (!!) x = !(!x) - -let new_counter ~name a ~incr ~build = - assert(not (List.mem_assoc name !counters)); - let data = ref (ref a) in - counters := (name, Obj.repr data) :: !counters; - let m = Mutex.create () in - let mk_thsafe_local_getter f () = - (* - slaves must use a remote counter getter, not this one! *) - (* - in the main process there is a race condition between slave - managers (that are threads) and the main thread, hence the mutex *) - if Flags.async_proofs_is_worker () then - CErrors.anomaly(Pp.str"Slave processes must install remote counters."); - let x = CThread.with_lock m ~scope:f in - build x in - let mk_thsafe_remote_getter f () = - CThread.with_lock m ~scope:f in - let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in - let installer f = - if not (Flags.async_proofs_is_worker ()) then - CErrors.anomaly(Pp.str"Only slave processes can install a remote counter."); - getter := mk_thsafe_remote_getter f in - (fun () -> !getter ()), installer - -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); - let dataref = Obj.obj (List.assoc name !counters) in - !dataref := !!(Obj.obj data)) - l diff --git a/lib/remoteCounter.mli b/lib/remoteCounter.mli deleted file mode 100644 index 42d1f8a8d1..0000000000 --- a/lib/remoteCounter.mli +++ /dev/null @@ -1,31 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* Remote counters are *global* counters for fresh ids. In the master/slave - * scenario, the slave installs a getter that asks the master for a fresh - * value. In the scenario of a slave that runs after the death of the master - * on some marshalled data, a backup of all counters status should be taken and - * restored to avoid reusing ids. - * Counters cannot be created by threads, they must be created once and forall - * as toplevel module declarations. *) - - -type 'a getter = unit -> 'a -type 'a installer = ('a getter) -> unit - -val new_counter : name:string -> - 'a -> incr:('a -> 'a) -> build:('a -> 'b) -> 'b getter * 'b installer - -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/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index dd80ff21aa..a9f203014f 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -56,12 +56,8 @@ module Make(T : Task) () = struct type response = | Response of T.response | RespFeedback of Feedback.feedback - | RespGetCounterNewUnivLevel type request = Request of T.request - type more_data = - | MoreDataUnivLevel of UnivGen.univ_unique_id list - let slave_respond (Request r) = let res = T.perform r in Response res @@ -94,16 +90,6 @@ module Make(T : Task) () = struct with Failure s | Invalid_argument s | Sys_error s -> marshal_err ("unmarshal_response: "^s) - let marshal_more_data oc (res : more_data) = - try marshal_to_channel oc res - with Failure s | Invalid_argument s | Sys_error s -> - marshal_err ("marshal_more_data: "^s) - - let unmarshal_more_data ic = - try (CThread.thread_friendly_input_value ic : more_data) - with Failure s | Invalid_argument s | Sys_error s -> - marshal_err ("unmarshal_more_data: "^s) - let report_status ?(id = !Flags.async_proofs_worker_id) s = let open Feedback in feedback ~id:Stateid.initial (WorkerStatus(id, s)) @@ -198,8 +184,6 @@ module Make(T : Task) () = struct | Unix.WEXITED i -> Printf.sprintf "exit(%d)" i | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in - let more_univs n = - CList.init n (fun _ -> UnivGen.new_univ_id ()) in let rec kill_if () = if not (Worker.is_alive proc) then () @@ -231,9 +215,6 @@ module Make(T : Task) () = struct marshal_request oc (Request req); let rec continue () = match unmarshal_response ic with - | RespGetCounterNewUnivLevel -> - marshal_more_data oc (MoreDataUnivLevel (more_univs 10)); - continue () | RespFeedback fbk -> T.forward_feedback fbk; continue () | Response resp -> match T.use_response !worker_age task resp with @@ -315,13 +296,6 @@ module Make(T : Task) () = struct let ic, oc = Spawned.get_channels () in slave_oc := Some oc; slave_ic := Some ic - let bufferize f = - let l = ref [] in - fun () -> - match !l with - | [] -> let data = f () in l := List.tl data; List.hd data - | x::tl -> l := tl; x - let slave_handshake () = Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc) @@ -339,11 +313,6 @@ module Make(T : Task) () = struct Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc) () in ignore (Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x)); - (* We ask master to allocate universe identifiers *) - UnivGen.set_remote_new_univ_id (bufferize @@ Control.protect_sigalrm (fun () -> - marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; - match unmarshal_more_data (Option.get !slave_ic) with - | MoreDataUnivLevel l -> l)); let working = ref false in slave_handshake (); while true do diff --git a/stm/stm.ml b/stm/stm.ml index f5768726c3..6287943cee 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2447,24 +2447,21 @@ let join ~doc = VCS.print (); doc -let dump_snapshot () = Slaves.dump_snapshot (), RemoteCounter.snapshot () - -type tasks = int Slaves.tasks * RemoteCounter.remote_counters_status -let check_task name (tasks,rcbackup) i = - RemoteCounter.restore rcbackup; +type tasks = int Slaves.tasks +let check_task name tasks i = let vcs = VCS.backup () in try let rc = State.purify (Slaves.check_task name tasks) i in VCS.restore vcs; rc with e when CErrors.noncritical e -> VCS.restore vcs; false -let info_tasks (tasks,_) = Slaves.info_tasks tasks -let finish_tasks name u p (t,rcbackup as tasks) = - RemoteCounter.restore rcbackup; +let info_tasks = Slaves.info_tasks + +let finish_tasks name u p tasks = let finish_task u (_,_,i) = let vcs = VCS.backup () in - let u = State.purify (Slaves.finish_task name u p t) i in + let u = State.purify (Slaves.finish_task name u p tasks) i in VCS.restore vcs; u in try @@ -2515,13 +2512,13 @@ let snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_vo = CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs"); (* LATER: when create_vos is true, it could be more efficient to not allocate the futures; but for now it seems useful for synchronization of the workers, below, [snapshot] gets computed even if [create_vos] is true. *) - let (tasks,counters) = dump_snapshot() in + let tasks = Slaves.dump_snapshot() in let except = List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty tasks in let todo_proofs = if create_vos then Library.ProofsTodoSomeEmpty except - else Library.ProofsTodoSome (except,tasks,counters) + else Library.ProofsTodoSome (except,tasks) in Library.save_library_to todo_proofs ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ()); doc diff --git a/test-suite/success/RemoteUnivs.v b/test-suite/success/RemoteUnivs.v new file mode 100644 index 0000000000..5ab4937dda --- /dev/null +++ b/test-suite/success/RemoteUnivs.v @@ -0,0 +1,31 @@ + + +Goal Type * Type. +Proof. + split. + par: exact Type. +Qed. + +Goal Type. +Proof. + exact Type. +Qed. + +(* (* coqide test, note the delegated proofs seem to get an empty dirpath? + or I got confused because I had lemma foo in file foo + *) +Definition U := Type. + +Lemma foo : U. +Proof. + exact Type. +Qed. + + +Lemma foo1 : Type. +Proof. + exact (U:Type). +Qed. + +Print foo. +*) diff --git a/vernac/library.ml b/vernac/library.ml index cc9e3c3c44..eedf8aa670 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -448,10 +448,10 @@ let save_library_base f sum lib univs tasks proofs = Sys.remove f; Exninfo.iraise reraise -type ('document,'counters) todo_proofs = +type 'document todo_proofs = | ProofsTodoNone (* for .vo *) | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *) - | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *) + | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list (* for .vio *) let save_library_to todo_proofs ~output_native_objects dir f otab = assert( @@ -464,7 +464,7 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = let except = match todo_proofs with | ProofsTodoNone -> Future.UUIDSet.empty | ProofsTodoSomeEmpty except -> except - | ProofsTodoSome (except,l,_) -> except + | ProofsTodoSome (except,l) -> except in let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in let opaque_table, f2t_map = Opaqueproof.dump ~except otab in @@ -473,13 +473,13 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = | ProofsTodoNone -> None, None | ProofsTodoSomeEmpty _except -> None, Some (Univ.ContextSet.empty,false) - | ProofsTodoSome (_except, tasks, rcbackup) -> + | ProofsTodoSome (_except, tasks) -> let tasks = List.map Stateid.(fun (r,b) -> try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b with Not_found -> assert b; { r with uuid = -1 }, b) tasks in - Some (tasks,rcbackup), + Some tasks, Some (Univ.ContextSet.empty,false) in let sd = { diff --git a/vernac/library.mli b/vernac/library.mli index d0e9f84691..4c6c654c58 100644 --- a/vernac/library.mli +++ b/vernac/library.mli @@ -41,13 +41,13 @@ type seg_proofs = Opaqueproof.opaque_proofterm array argument. [output_native_objects]: when producing vo objects, also compile the native-code version. *) -type ('document,'counters) todo_proofs = +type 'document todo_proofs = | ProofsTodoNone (* for .vo *) | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *) - | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *) + | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list (* for .vio *) val save_library_to : - ('document,'counters) todo_proofs -> + 'document todo_proofs -> output_native_objects:bool -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit |