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.

0 files changed, 0 insertions, 0 deletions