Skip to content

Commit

Permalink
remote counter: avoid thread race on sockets (fix coq#4823)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
gares committed Jun 17, 2016
1 parent 8a45a3a commit 905e82c
Showing 1 changed file with 5 additions and 3 deletions.
8 changes: 5 additions & 3 deletions lib/remoteCounter.ml
Expand Up @@ -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");
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
Expand Down

0 comments on commit 905e82c

Please sign in to comment.