From 16a2717d25096fcbd07b252e775b66b6fbb6d2bd Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Tue, 20 Aug 2013 12:43:42 +0000
Subject: 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
---
 pretyping/termops.ml  | 8 +++-----
 pretyping/termops.mli | 1 +
 2 files changed, 4 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 8a5a828032..9d57e1c80b 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 3fe266727f..92a4d961a3 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
-- 
cgit v1.2.3