Universe counters on slaves are in sync with master

Simple framework for remote counters.  The slaves ask
the master for a fresh value.  On the master the thread
manager answers with a bunch of fresh values (so that further
requests can be immediately satisfied).
Remote counters are guarded with a mutex on the master,
because all slave managers as well as the master thread
can access the counter at the same time.

I know the name sucks.  These counters are remote for the slaves,
and local for the master.  I'm open to suggestions...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16713 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 46 insertions, 6 deletions

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index db0843c823..48e7403ce6 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