From d5b0260af4fcdc08d3ce89b771a8ecad0685b556 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <basile.clement@ocamlpro.com>
Date: Wed, 7 Jun 2023 18:38:15 +0200
Subject: [PATCH] Copy input files to RAM before running the provers
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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.
---
 src/core/Misc.ml   | 38 ++++++++++++++++++++++++++++++++++++++
 src/core/Prover.ml |  2 ++
 2 files changed, 40 insertions(+)

diff --git a/src/core/Misc.ml b/src/core/Misc.ml
index 5b817be..4b498cf 100644
--- a/src/core/Misc.ml
+++ b/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 ];
diff --git a/src/core/Prover.ml b/src/core/Prover.ml
index 9bcae40..f3a04d0 100644
--- a/src/core/Prover.ml
+++ b/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 *)