From 855cc26b25f166008594f6e225387901d6551947 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 10 Oct 2019 08:06:29 -0700 Subject: [PATCH] Fix data race in ProcessPool Summary: This diff fixes a data race in ProcessPool: out channel flush was outside of the critical section. Reviewed By: ezgicicek Differential Revision: D17853991 fbshipit-source-id: ac0fd2a69 --- infer/src/base/ProcessPool.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/infer/src/base/ProcessPool.ml b/infer/src/base/ProcessPool.ml index 51851d62b..e03f12eef 100644 --- a/infer/src/base/ProcessPool.ml +++ b/infer/src/base/ProcessPool.ml @@ -85,8 +85,9 @@ let marshal_to_pipe ?file_lock fd x = PerfEvent.log_begin_event logger ~categories:["sys"] ~name:"send to pipe" () ) ; Option.iter file_lock ~f:(fun {Utils.lock} -> lock ()) ; Marshal.to_channel fd x [] ; - Option.iter file_lock ~f:(fun {Utils.unlock} -> unlock ()) ; + (* Channel flush should be inside the critical section. *) Out_channel.flush fd ; + Option.iter file_lock ~f:(fun {Utils.unlock} -> unlock ()) ; PerfEvent.(log (fun logger -> log_end_event logger ()))