Parallel preprocessing

dune-project

@@ -42,6 +42,7 @@
     json-data-encoding
     jsonrpc
     (sha (>= 1.12))
+    cpu
     (conf-gmp (>= 3)) ; only needed transitively, but they don't have lower bound, which is needed on MacOS
     (conf-ruby :with-test)
     (benchmark :with-test) ; TODO: make this optional somehow, (optional) on bench executable doesn't work

goblint.opam

@@ -38,6 +38,7 @@ depends: [
   "json-data-encoding"
   "jsonrpc"
   "sha" {>= "1.12"}
+  "cpu"
   "conf-gmp" {>= "3"}
   "conf-ruby" {with-test}
   "benchmark" {with-test}

goblint.opam.locked

@@ -32,12 +32,15 @@ depends: [
   "biniou" {= "1.2.1"}
   "camlidl" {= "1.09"}
   "cmdliner" {= "1.0.4" & with-doc}
+  "conf-autoconf" {= "0.1"}
   "conf-gmp" {= "3"}
   "conf-mpfr" {= "2"}
   "conf-perl" {= "1"}
   "conf-pkg-config" {= "2"}
   "conf-ruby" {= "1.0.0" & with-test}
+  "conf-which" {= "1"}
   "cppo" {= "1.6.7"}
+  "cpu" {= "2.0.0"}
   "dune" {= "2.9.1"}
   "dune-private-libs" {= "2.9.1"}
   "dune-site" {= "2.9.1"}

src/dune

@@ -8,7 +8,7 @@
   (public_name goblint.lib)
   (wrapped false)
   (modules :standard \ goblint mainarinc mainspec privPrecCompare apronPrecCompare)
-  (libraries goblint.sites goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc
+  (libraries goblint.sites goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
     ; See: https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies.

src/maingoblint.ml

@@ -90,6 +90,7 @@ let option_spec_list =
   let tmp_arg = ref "" in
   [ "-o"                   , Arg.String (set_string "outfile"), ""
   ; "-v"                   , Arg.Unit (fun () -> set_bool "dbg.verbose" true; set_bool "printstats" true), ""
+  ; "-j"                   , Arg.Int (set_int "jobs"), ""
   ; "-I"                   , Arg.String (set_string "includes[+]"), ""
   ; "-IK"                  , Arg.String (set_string "kernel_includes[+]"), ""
   ; "--set"                , Arg.Tuple [Arg.Set_string tmp_arg; Arg.String (fun x -> set_auto !tmp_arg x)], ""
@@ -155,18 +156,13 @@ let basic_preprocess ~all_cppflags fname =
   (* The actual filename of the preprocessed sourcefile *)
   let nname =  Filename.concat !Goblintutil.tempDirName (Filename.basename fname) in
   if Sys.file_exists (get_string "tempDir") then
-    nname
+    (nname, None)
   else
     (* Preprocess using cpp. *)
     (* ?? what is __BLOCKS__? is it ok to just undef? this? http://en.wikipedia.org/wiki/Blocks_(C_language_extension) *)
     let command = (Preprocessor.get_cpp ()) ^ " --undef __BLOCKS__ " ^ String.join " " (List.map Filename.quote all_cppflags) ^ " \"" ^ fname ^ "\" -o \"" ^ nname ^ "\"" in
     if get_bool "dbg.verbose" then print_endline command;
-
-    try match Unix.system command with
-      | Unix.WEXITED 0 -> nname
-      | _ -> eprintf "Goblint: Preprocessing failed."; raise Exit
-    with Unix.Unix_error (e, f, a) ->
-      eprintf "%s at syscall %s with argument \"%s\".\n" (Unix.error_message e) f a; raise Exit
+    (nname, Some {ProcessPool.command; cwd = None})
 
 (** Preprocess all files. Return list of preprocessed files and the temp directory name. *)
 let preprocess_files () =
@@ -282,7 +278,14 @@ let preprocess_files () =
   if get_bool "ana.sv-comp.functions" then
     extra_arg_files := find_custom_include "sv-comp.c" :: !extra_arg_files;
 
-  List.concat_map preprocess_arg_file (!extra_arg_files @ !arg_files)
+  let preprocessed = List.concat_map preprocess_arg_file (!extra_arg_files @ !arg_files) in
+  let preprocess_tasks = List.filter_map snd preprocessed in
+  let terminated task = function
+    | Unix.WEXITED 0 -> ()
+    | process_status -> failwith (GobUnix.string_of_process_status process_status)
+  in
+  ProcessPool.run ~jobs:(Goblintutil.jobs ()) ~terminated preprocess_tasks;
+  List.map fst preprocessed
 
 (** Possibly merge all postprocessed files *)
 let merge_preprocessed cpp_file_names =

src/util/compilationDatabase.ml

@@ -18,17 +18,6 @@ let parse_file filename =
 let command_o_regexp = Str.regexp "-o +[^ ]+"
 let command_program_regexp = Str.regexp "^ *\\([^ ]+\\)"
 
-let system ~cwd command =
-  let old_cwd = Sys.getcwd () in
-  Fun.protect ~finally:(fun () ->
-      Sys.chdir old_cwd
-    ) (fun () ->
-      Sys.chdir cwd;
-      match Unix.system command with
-      | WEXITED 0 -> ()
-      | process_status -> failwith (GobUnix.string_of_process_status process_status)
-    )
-
 let load_and_preprocess ~all_cppflags filename =
   let database_dir = Filename.dirname (GobFilename.absolute filename) in (* absolute before dirname to avoid . *)
   let reroot =
@@ -93,8 +82,8 @@ let load_and_preprocess ~all_cppflags filename =
       let cwd = reroot obj.directory in
       if GobConfig.get_bool "dbg.verbose" then
         Printf.printf "Preprocessing %s\n  to %s\n  using %s\n  in %s\n" file preprocessed_file preprocess_command cwd;
-      system ~cwd preprocess_command; (* command/arguments might have paths relative to directory *)
-      Some preprocessed_file
+      let preprocess_task = {ProcessPool.command = preprocess_command; cwd = Some cwd} in (* command/arguments might have paths relative to directory *)
+      Some (preprocessed_file, Some preprocess_task)
   in
   parse_file filename
   |> BatList.filter_map preprocess

src/util/goblintutil.ml

@@ -183,3 +183,8 @@ let rec for_all_in_range (a, b) f =
   else f a && (for_all_in_range (BI.add a (BI.one), b) f)
 
 let dummy_obj = Obj.repr ()
+
+let jobs () =
+  match get_int "jobs" with
+  | 0 -> Cpu.numcores ()
+  | n -> n

src/util/options.schema.json

@@ -217,6 +217,12 @@
       "type": "boolean",
       "default": false
     },
+    "jobs": {
+      "title": "jobs",
+      "description": "Maximum number of parallel jobs. If 0, then number of cores is used. Currently used for preprocessing.",
+      "type": "integer",
+      "default": 1
+    },
     "server": {
       "title": "Server",
       "description": "Server mode",

src/util/processPool.ml

@@ -0,0 +1,44 @@
+type task = {
+  command: string;
+  cwd: string option;
+}
+
+let run ~jobs ?(terminated=fun _ _ -> ()) tasks =
+  let procs = Hashtbl.create jobs in
+  let rec run tasks =
+    match tasks with
+    | task :: tasks when Hashtbl.length procs < jobs ->
+      let old_cwd = Sys.getcwd () in
+      let proc =
+        match task.cwd with
+        | Some cwd ->
+          Fun.protect ~finally:(fun () ->
+              Sys.chdir old_cwd
+            ) (fun () ->
+              Sys.chdir cwd;
+              Unix.open_process task.command
+            )
+        | None ->
+          Unix.open_process task.command
+      in
+      let pid = Unix.process_pid proc in
+      Hashtbl.replace procs pid (task, proc);
+      run tasks
+    | [] when Hashtbl.length procs = 0 ->
+      ()
+    | _ ->
+      let (pid, status) = Unix.wait () in (* wait for any child process to terminate *)
+      begin match Hashtbl.find_opt procs pid with
+        | Some (task, (proc_in, proc_out)) ->
+          (* Unix.close_process proc; *)
+          (* only part of close_process, no need to wait *)
+          close_in proc_in;
+          close_out proc_out;
+          Hashtbl.remove procs pid;
+          terminated task status
+        | None -> (* unrelated process *)
+          ()
+      end;
+      run tasks
+  in
+  run tasks