From 3efee577b4c92b38a987b40e555fae2c0a2023c4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 26 Mar 2021 15:34:59 +0100
Subject: Remove remote counter system

---
 lib/remoteCounter.ml  | 52 ---------------------------------------------------
 lib/remoteCounter.mli | 31 ------------------------------
 2 files changed, 83 deletions(-)
 delete mode 100644 lib/remoteCounter.ml
 delete mode 100644 lib/remoteCounter.mli

(limited to 'lib')

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
-- 
cgit v1.2.3