diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 18:33:25 +0100 |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /lib/remoteCounter.ml | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
Diffstat (limited to 'lib/remoteCounter.ml')
-rw-r--r-- | lib/remoteCounter.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml index 3f198259..e7646fb7 100644 --- a/lib/remoteCounter.ml +++ b/lib/remoteCounter.ml @@ -20,19 +20,21 @@ 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 *) if Flags.async_proofs_is_worker () then - Errors.anomaly(Pp.str"Slave processes must install remote counters"); + CErrors.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 + 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 |