aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/univ.ml4
-rw-r--r--kernel/univ.mli1
-rw-r--r--lib/lib.mllib1
-rw-r--r--lib/remoteCounter.ml29
-rw-r--r--lib/remoteCounter.mli14
-rw-r--r--pretyping/termops.ml8
-rw-r--r--pretyping/termops.mli1
-rw-r--r--test-suite/interactive/Paral-ITP.v1
-rw-r--r--toplevel/stm.ml52
9 files changed, 99 insertions, 12 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml
index e6752bb9e..ce9d9c419 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -851,7 +851,9 @@ let fresh_level =
let n = ref 0 in
fun () -> incr n; UniverseLevel.Level (!n, Names.DirPath.empty)
-let fresh_local_univ () = Atom (fresh_level ())
+let fresh_local_univ, set_remote_fresh_local_univ =
+ RemoteCounter.new_counter 0 ~incr:((+) 1)
+ ~build:(fun n -> Atom (UniverseLevel.Level (n, Names.DirPath.empty)))
(* Miscellaneous functions to remove or test local univ assumed to
occur only in the le constraints *)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 6b64ca8e4..7511769c4 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -129,6 +129,7 @@ val sort_universes : universes -> universes
(** {6 Support for sort-polymorphic inductive types } *)
val fresh_local_univ : unit -> universe
+val set_remote_fresh_local_univ : universe RemoteCounter.installer
val solve_constraints_system : universe option array -> universe array ->
universe array
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 5f1314185..9f29613d1 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -19,5 +19,6 @@ Dnet
Unionfind
Genarg
Future
+RemoteCounter
Dag
Vcs
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
new file mode 100644
index 000000000..1983d2722
--- /dev/null
+++ b/lib/remoteCounter.ml
@@ -0,0 +1,29 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+type 'a getter = unit -> 'a
+type 'a installer = ('a getter) -> unit
+
+let new_counter a ~incr ~build =
+ let data = ref a in
+ let m = Mutex.create () in
+ let mk_thsafe_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.coq_slave_mode > 0 then
+ Errors.anomaly(Pp.str"Slave processes must install remote counters");
+ Mutex.lock m; let x = f () in Mutex.unlock m;
+ build x in
+ let getter = ref (mk_thsafe_getter (fun () -> data := incr !data; !data)) in
+ let installer f =
+ if !Flags.coq_slave_mode < 1 then
+ Errors.anomaly(Pp.str"Only slave processes can install a remote counter")
+ else getter := f in
+ (fun () -> !getter ()), installer
+
diff --git a/lib/remoteCounter.mli b/lib/remoteCounter.mli
new file mode 100644
index 000000000..f17f1be3c
--- /dev/null
+++ b/lib/remoteCounter.mli
@@ -0,0 +1,14 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+type 'a getter = unit -> 'a
+type 'a installer = ('a getter) -> unit
+
+val new_counter :
+ 'a -> incr:('a -> 'a) -> build:('a -> 'b) -> 'b getter * 'b installer
+
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 8a5a82803..9d57e1c80 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -147,11 +147,9 @@ let print_env env =
let set_module m = current_module := m*)
-let new_univ_level =
- let univ_gen = ref 0 in
- (fun sp ->
- incr univ_gen;
- Univ.UniverseLevel.make (Lib.library_dp()) !univ_gen)
+let new_univ_level, set_remote_new_univ_level =
+ RemoteCounter.new_counter 0 ~incr:((+) 1)
+ ~build:(fun n -> Univ.UniverseLevel.make (Lib.library_dp()) n)
let new_univ () = Univ.Universe.make (new_univ_level ())
let new_Type () = mkType (new_univ ())
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 3fe266727..92a4d961a 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -18,6 +18,7 @@ open Locus
(** Universes *)
val new_univ_level : unit -> Univ.universe_level
+val set_remote_new_univ_level : Univ.universe_level RemoteCounter.installer
val new_univ : unit -> Univ.universe
val new_sort_in_family : sorts_family -> sorts
val new_Type : unit -> types
diff --git a/test-suite/interactive/Paral-ITP.v b/test-suite/interactive/Paral-ITP.v
index 09ec9de17..d8961c98d 100644
--- a/test-suite/interactive/Paral-ITP.v
+++ b/test-suite/interactive/Paral-ITP.v
@@ -22,6 +22,7 @@ Qed.
Lemma b : True.
Proof.
+ do 11 (cut Type; [ intro foo; clear foo | exact Type]).
sleep time.
idtac.
(* change in semantics: Print a. *)
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index db0843c82..48e7403ce 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -565,16 +565,25 @@ end = struct (* {{{ *)
let set_reach_known_state f = reach_known_state := f
type request = ReqBuildProof of (Stateid.t * Stateid.t) * Stateid.t * VCS.vcs
+
type response =
| RespBuiltProof of Entries.proof_output list
| RespError of std_ppcmds
| RespFeedback of Interface.feedback
+ | RespGetCounterFreshLocalUniv
+ | RespGetCounterNewUnivLevel
let pr_response = function
| RespBuiltProof _ -> "Sucess"
| RespError _ -> "Error"
| RespFeedback { Interface.id = Interface.State id } ->
"Feedback on " ^ Stateid.to_string id
| RespFeedback _ -> assert false
+ | RespGetCounterFreshLocalUniv -> "GetCounterFreshLocalUniv"
+ | RespGetCounterNewUnivLevel -> "GetCounterNewUnivLevel"
+
+ type more_data =
+ | MoreDataLocalUniv of Univ.universe list
+ | MoreDataUnivLevel of Univ.universe_level list
type task =
| TaskBuildProof of (Stateid.t * Stateid.t) * Stateid.t * Stateid.t *
@@ -607,21 +616,29 @@ end = struct (* {{{ *)
exception MarshalError
- let marshal_request oc req =
+ let marshal_request oc (req : request) =
try Marshal.to_channel oc req []; flush oc
with Invalid_argument _ -> raise MarshalError
- let unmarshal_response ic =
- try (Marshal.from_channel ic : response)
- with Invalid_argument _ -> raise MarshalError
-
let unmarshal_request ic =
try (Marshal.from_channel ic : request)
with Invalid_argument _ -> raise MarshalError
- let marshal_response oc res =
+ let marshal_response oc (res : response) =
+ try Marshal.to_channel oc res []; flush oc
+ with Invalid_argument _ -> raise MarshalError
+
+ let unmarshal_response ic =
+ try (Marshal.from_channel ic : response)
+ with Invalid_argument _ -> raise MarshalError
+
+ let marshal_more_data oc (res : more_data) =
try Marshal.to_channel oc res []; flush oc
with Invalid_argument _ -> raise MarshalError
+
+ let unmarshal_more_data ic =
+ try (Marshal.from_channel ic : more_data)
+ with Invalid_argument _ -> raise MarshalError
let queue : task TQueue.t = TQueue.create ()
@@ -652,6 +669,14 @@ end = struct (* {{{ *)
assign (`Val pl)
| TaskBuildProof(_,_,_, assign), RespError e ->
assign (`Exn (RemoteException e))
+ | _, RespGetCounterFreshLocalUniv ->
+ marshal_more_data oc (MoreDataLocalUniv
+ (CList.init 10 (fun _ -> Univ.fresh_local_univ ())));
+ loop ()
+ | _, RespGetCounterNewUnivLevel ->
+ marshal_more_data oc (MoreDataUnivLevel
+ (CList.init 10 (fun _ -> Termops.new_univ_level ())));
+ loop ()
| _, RespFeedback {id = State state_id; content = msg} ->
Pp.feedback ~state_id msg;
loop ()
@@ -687,11 +712,26 @@ end = struct (* {{{ *)
set_binary_mode_in !slave_ic true;
Unix.dup2 Unix.stderr Unix.stdout
+ 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_main_loop () =
let slave_feeder oc fb =
Marshal.to_channel oc (RespFeedback fb) [];
flush oc in
Pp.set_feeder (slave_feeder !slave_oc);
+ Termops.set_remote_new_univ_level (bufferize (fun () ->
+ marshal_response !slave_oc RespGetCounterNewUnivLevel;
+ match unmarshal_more_data !slave_ic with
+ | MoreDataUnivLevel l -> l | _ -> assert false));
+ Univ.set_remote_fresh_local_univ (bufferize (fun () ->
+ marshal_response !slave_oc RespGetCounterFreshLocalUniv;
+ match unmarshal_more_data !slave_ic with
+ | MoreDataLocalUniv l -> l | _ -> assert false));
while true do
try
let request = unmarshal_request !slave_ic in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 07:35:40 +0000