Add --chunk to set per-procedure-parallelism chunk size

Summary:
Currently --per-procedure-parallelism defaults to a chunk size of 1
procedure, which has a high overhead.  Add a command line option to
control it, and raise the default value.

Reviewed By: jvillard

Differential Revision: D4794692

fbshipit-source-id: 7715a40

infer/src/backend/InferAnalyze.re

@@ -150,36 +150,30 @@ let main makefile => {
       (List.length clusters_to_analyze)
       (List.length all_clusters)
       Config.results_dir;
-    if (makefile != "" || Config.per_procedure_parallelism) {
+    let is_java () =>
-      let is_java () =>
+      List.exists
-        List.exists
+        f::(fun cl => SourceFile.string_crc_has_extension ext::"java" (DB.source_dir_to_string cl))
-          f::(
+        all_clusters;
-            fun cl => SourceFile.string_crc_has_extension ext::"java" (DB.source_dir_to_string cl)
+    if (Config.per_procedure_parallelism && not (is_java ())) {
-          )
+      /* Java uses ZipLib which is incompatible with forking */
-          all_clusters;
+      /* per-procedure parallelism */
-      if (not Config.per_procedure_parallelism) {
+      L.stdout "per-procedure parallelism jobs:%d@." Config.jobs;
-        ClusterMakefile.create_cluster_makefile clusters_to_analyze makefile
+      if (makefile != "") {
-      } else {
+        ClusterMakefile.create_cluster_makefile [] makefile
-        /* per-procedure parallelism */
+      };
-        if (is_java ()) {
+      /* Prepare tasks one cluster at a time while executing in parallel */
-          /* Java uses ZipLib which is incompatible with forking */
+      let runner = Tasks.Runner.create jobs::Config.jobs;
-          L.stderr "Error: option --per-procedure-parallelism not supported with Java@.";
+      let cluster_start_tasks i cluster => {
-          exit 1
+        let tasks = analyze_cluster_tasks i cluster;
-        };
+        let aggregate_tasks = Tasks.aggregate size::Config.procedures_per_process tasks;
-        L.stdout "per-procedure parallelism jobs:%d@." Config.jobs;
+        Tasks.Runner.start runner tasks::aggregate_tasks
-        if (makefile != "") {
+      };
-          ClusterMakefile.create_cluster_makefile [] makefile
+      List.iteri f::cluster_start_tasks clusters_to_analyze;
-        };
+      Tasks.Runner.complete runner
-        /* Prepare tasks one cluster at a time while executing in parallel */
+    } else if (
-        let runner = Tasks.Runner.create jobs::Config.jobs;
+      makefile != ""
-        let cluster_start_tasks i cluster => {
+    ) {
-          let tasks = analyze_cluster_tasks i cluster;
+      ClusterMakefile.create_cluster_makefile clusters_to_analyze makefile
-          let aggregate_tasks = Tasks.aggregate size::1 tasks;
-          Tasks.Runner.start runner tasks::aggregate_tasks
-        };
-        List.iteri f::cluster_start_tasks clusters_to_analyze;
-        Tasks.Runner.complete runner
-      }
     } else {
       /* This branch is reached when -j 1 is used */
       List.iteri f::analyze_cluster clusters_to_analyze;

infer/src/backend/Tasks.ml

@@ -35,9 +35,10 @@ let empty = { closures = []; continuations = Queue.create () }
 let aggregate ~size t =
   let group_to_closure group =
     fun () -> List.iter ~f:(fun closure -> closure ()) group in
-  if size > 1
+  let group_size = if size > 0 then size else (List.length t.closures) / Config.jobs in
+  if group_size > 1
   then
-    let groups = List.groupi ~break:(fun n _ _ -> Int.equal (n mod size) 0) t.closures in
+    let groups = List.groupi ~break:(fun n _ _ -> Int.equal (n mod group_size) 0) t.closures in
     let closures = List.map ~f:group_to_closure groups in
     { t with closures }
   else

infer/src/base/Config.ml

@@ -1105,7 +1105,7 @@ and patterns_skip_translation =
      "Matcher or list of matchers for names of files that should not be analyzed at all.")
 
 and per_procedure_parallelism =
-  CLOpt.mk_bool ~deprecated:["per-procedure-parallelism"] ~long:"per-procedure-parallelism"
+  CLOpt.mk_bool ~long:"per-procedure-parallelism" ~default:true
     "Perform analysis with per-procedure parallelism.\n\
      Java is not supported."
 
@@ -1130,6 +1130,12 @@ and print_using_diff =
   CLOpt.mk_bool ~deprecated_no:["noprintdiff"] ~long:"print-using-diff" ~default:true
     "Highlight the difference w.r.t. the previous prop when printing symbolic execution debug info"
 
+and procedures_per_process =
+  CLOpt.mk_int ~long:"procedures-per-process" ~default:1000 ~meta:"int"
+    "Specify the number of procedures to analyze per process when using \
+     --per-procedure-parallelism.  If 0 is specified, each file is divided into --jobs groups of \
+     procedures."
+
 and procs_csv =
   CLOpt.mk_path_opt ~deprecated:["procs"] ~long:"procs-csv"
     ~meta:"file" "Write statistics for each procedure in CSV format to a file"
@@ -1672,6 +1678,7 @@ and print_logs = !print_logs
 and print_builtins = !print_builtins
 and print_types = !print_types
 and print_using_diff = !print_using_diff
+and procedures_per_process = !procedures_per_process
 and procs_csv = !procs_csv
 and procs_xml = !procs_xml
 and quandary = !quandary

infer/src/base/Config.mli

@@ -287,6 +287,7 @@ val print_logs : bool
 val print_builtins : bool
 val print_types : bool
 val print_using_diff : bool
+val procedures_per_process : int
 val procs_csv : string option
 val procs_xml : string option
 val project_root : string