remote counter: avoid thread race on sockets (fix #4823)

With par: the scenario is this one:

coqide --- master ---- proof worker 1 (has no par: steps)
                  ---- proof worker 2 (has a par: step)
                          ---- tac worker 2.1
                          ---- tac worker 2.2
                          ---- tac worker 2.3

Actor 2 installs a remote counter for universe levels, that are
requested to master.  Multiple threads dealing with actors 2.x
may need to get values from that counter at the same time.

Long story short, in this complex scenario a mutex was missing
and the control threads for 2.x were accessing the counter (hence
reading/writing to the single socket connecting 2 with master at the
same time, "corrupting" the data flow).

A better solution would be to have a way to generate unique fresh universe
levels locally to a worker.

1 files changed, 5 insertions, 3 deletions

diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index 3f1982594..6cc48c874 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -20,7 +20,7 @@ let new_counter ~name a ~incr ~build =
   let data = ref (ref a) in
   counters := (name, Obj.repr data) :: !counters;
   let m = Mutex.create () in
-  let mk_thsafe_getter f () =
+  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 *)
@@ -28,11 +28,13 @@ let new_counter ~name a ~incr ~build =
       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 mk_thsafe_remote_getter f () =
+    Mutex.lock m; let x = f () in Mutex.unlock m; x 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
       Errors.anomaly(Pp.str"Only slave processes can install a remote counter");
-    getter := f in
+    getter := mk_thsafe_remote_getter f in
   (fun () -> !getter ()), installer
 
 let backup () = !counters