Copy input files to RAM before running the provers

This ensures that we don't benchmark the time it takes to load the
problem from disk, and helps minimise noise in situations of high disk
contention, and other noise from the filesystem cache.

We are still limited by the RAM bandwidth but… what can you do.

This is only effective on Unix (more precisely, on Unix systems where
`/dev/shm` is actually in RAM); on Windows the default temporary
directory will be used. To enable the same behavior on Windows, pass a
RAM disk as `--ramdisk` argument.

To disable the behavior on Linux, you can pass a directory that is not
in RAM to the `--ramdisk` argument. The files will still be copied.

Author: bclement-ocp

src/core/Misc.ml

@@ -511,6 +511,44 @@ let with_ram_file prefix suffix f =
       try Sys.remove fname with Sys_error _ -> ())
     (fun () -> f fname)
 
+let with_copy_to_ram fname f =
+  if has_ramdisk () then (
+    let suffix = Filename.basename fname in
+    let fname =
+      CCIO.with_in ~flags:[ Open_binary ] fname @@ fun ic ->
+      let fname, oc = open_ram_file "" suffix in
+      Fun.protect
+        ~finally:(fun () -> close_out oc)
+        (fun () ->
+          CCIO.with_out ~flags:[ Open_binary ] fname @@ fun oc ->
+          CCIO.copy_into ~bufsize:(64 * 1024) ic oc;
+          fname)
+    in
+    Fun.protect
+      ~finally:(fun () -> try Sys.remove fname with Sys_error _ -> ())
+      (fun () -> f fname)
+  ) else
+    f fname
+
+let with_copy_from_ram fname f =
+  if has_ramdisk () then (
+    let suffix = Filename.basename fname in
+    let ram_fname, oc = open_ram_file "" suffix in
+    Fun.protect
+      ~finally:(fun () ->
+        ( CCIO.with_in ~flags:[ Open_binary ] ram_fname @@ fun ic ->
+          CCIO.copy_into ~bufsize:(64 * 1024) ic oc );
+        close_out oc;
+        Sys.remove ram_fname)
+      (fun () -> f ram_fname)
+  ) else
+    f fname
+
+let with_copy_from_ram_opt fname f =
+  match fname with
+  | Some fname -> with_copy_from_ram fname (fun fname -> f (Some fname))
+  | None -> f None
+
 let with_affinity cpu f =
   let aff = Processor.Affinity.get_ids () in
   Processor.Affinity.set_ids [ cpu ];

src/core/Prover.ml

@@ -199,6 +199,8 @@ module Set = CCSet.Make (As_key)
 
 let run ?env ?proof_file ~limits ~file (self : t) : Run_proc_result.t =
   Log.debug (fun k -> k "(@[Prover.run %s %a@])" self.name Limit.All.pp limits);
+  Misc.with_copy_to_ram file @@ fun file ->
+  Misc.with_copy_from_ram_opt proof_file @@ fun proof_file ->
   let cmd = make_command ?env ?proof_file ~limits self ~file in
   (* Give one more second to the ulimit timeout to account for the startup
      time and the time elasped between starting ulimit and starting the prover *)