[ProcessPool] Saturate cores evenly when possible

Summary: Experiments suggest that infer does not take advantage of hardware threads and using more CPUs than the number of physical cores actually hurts performance. On Linux, `ProcessPool` now by default uses only the same number of workers as physical CPUs and pins them evenly.

Reviewed By: ngorogiannis

Differential Revision: D20193171

fbshipit-source-id: f8b9f55bf

infer/src/base/Config.ml

@@ -437,7 +437,7 @@ let linters_def_default_file = linters_def_dir ^/ "linters.al"
 
 let wrappers_dir = lib_dir ^/ "wrappers"
 
-let ncpu = Setcore.numcores ()
+let ncpu = Utils.numcores
 
 let os_type = match Sys.os_type with "Win32" -> Win32 | "Cygwin" -> Cygwin | _ -> Unix
 

infer/src/base/ProcessPool.ml

@@ -378,7 +378,7 @@ let fork_child ~file_lock ~child_prelude ~slot (updates_r, updates_w) ~f ~epilog
       Unix.close updates_r ;
       Unix.close to_child_w ;
       (* Pin to a core. [setcore] does the modulo <number of cores> for us. *)
-      Setcore.setcore slot ;
+      Utils.set_best_cpu_for slot ;
       ProcessPoolState.in_child := true ;
       ProcessPoolState.reset_pid () ;
       child_prelude () ;

infer/src/base/Utils.ml

@@ -466,3 +466,41 @@ let iter_infer_deps ~project_root ~f infer_deps_file =
       List.iter ~f:one_line lines
   | Error error ->
       Die.die InternalError "Couldn't read deps file '%s': %s" infer_deps_file error
+
+
+let physical_cores () =
+  with_file_in "/proc/cpuinfo" ~f:(fun ic ->
+      let physical_or_core_regxp =
+        Re.Str.regexp "\\(physical id\\|core id\\)[^0-9]+\\([0-9]+\\).*"
+      in
+      let rec loop max_socket_id max_core_id =
+        match In_channel.input_line ~fix_win_eol:true ic with
+        | None ->
+            (max_socket_id + 1, max_core_id + 1)
+        | Some line when Re.Str.string_match physical_or_core_regxp line 0 -> (
+            let value = Re.Str.matched_group 2 line |> int_of_string in
+            match Re.Str.matched_group 1 line with
+            | "physical id" ->
+                loop (max value max_socket_id) max_core_id
+            | "core id" ->
+                loop max_socket_id (max value max_core_id)
+            | _ ->
+                L.die InternalError "Couldn't parse line '%s' from /proc/cpuinfo." line )
+        | Some _ ->
+            loop max_socket_id max_core_id
+      in
+      let sockets, cores_per_socket = loop 0 0 in
+      sockets * cores_per_socket )
+
+
+let cpus = Setcore.numcores ()
+
+let numcores =
+  match Version.build_platform with Darwin | Windows -> cpus / 2 | Linux -> physical_cores ()
+
+
+let set_best_cpu_for worker_id =
+  let threads_per_core = cpus / numcores in
+  let chosen_core = worker_id * threads_per_core % numcores in
+  let chosen_thread_in_core = worker_id * threads_per_core / numcores in
+  Setcore.setcore ((chosen_core * threads_per_core) + chosen_thread_in_core)

infer/src/base/Utils.mli

@@ -167,3 +167,11 @@ val get_available_memory_MB : unit -> int option
 val iter_infer_deps : project_root:string -> f:(string -> unit) -> string -> unit
 (** Parse each line of the given infer_deps.txt file (split on tabs, assume 3 elements per line) and
     run [f] on the third element. [project_root] is an argument to avoid dependency cycles. *)
+
+val numcores : int
+(** - On Linux return the number of physical cores (sockets * cores per socket).
+    - On Darwin and Windows returns half of the number of CPUs since most processors have 2 hardware
+      threads per core. *)
+
+val set_best_cpu_for : int -> unit
+(** Pins processes to CPUs aiming to saturate physical cores evenly *)

infer/src/dune.common.in

@@ -76,6 +76,7 @@ let common_libraries =
     ; "ocamlgraph"
     ; "oUnit"
     ; "parmap"
+    ; "re"
     ; "sqlite3"
     ; "str"
     ; "unix"