use domainpc

doc/src/hacking/benchmarking.md

@@ -6,10 +6,11 @@
 OCAML_LANDMARKS=on dune exec --instrument-with landmarks --profile release -- owi run test/run/binary_loop.wasm
 ```
 
-Note: it seems landmarks is not compatible with domains and thus won't work with most sub-commands.
+See the discussion in [#871] to understand landmarks limitations in Owi.
 
 ## Test-comp
 
 See [Symbocalypse].
 
+[#871]: https://github.com/OCamlPro/owi/pull/871
 [Symbocalypse]: https://github.com/OCamlPro/symbocalypse

doc/src/manpages/owi-c.md

@@ -68,6 +68,9 @@ OPTIONS
        --no-value
            do not display a value for each symbol
 
+       --no-worker-isolation
+           Do not force each worker to run on an isolated physical core.
+
        -o FILE, --output=FILE
            Output the generated .wasm or .wat to FILE.
 
@@ -88,7 +91,7 @@ OPTIONS
            skip typechecking pass
 
        -w VAL, --workers=VAL (absent=n)
-           number of workers for symbolic execution. Defaults to the number
+           Number of workers for symbolic execution. Defaults to the number
            of physical cores.
 
        --with-breadcrumbs

doc/src/manpages/owi-cpp.md

@@ -63,6 +63,9 @@ OPTIONS
        --no-value
            do not display a value for each symbol
 
+       --no-worker-isolation
+           Do not force each worker to run on an isolated physical core.
+
        -o FILE, --output=FILE
            Output the generated .wasm or .wat to FILE.
 
@@ -77,7 +80,7 @@ OPTIONS
            skip typechecking pass
 
        -w VAL, --workers=VAL (absent=n)
-           number of workers for symbolic execution. Defaults to the number
+           Number of workers for symbolic execution. Defaults to the number
            of physical cores.
 
        --with-breadcrumbs

doc/src/manpages/owi-iso.md

@@ -47,6 +47,9 @@ OPTIONS
        --no-value
            do not display a value for each symbol
 
+       --no-worker-isolation
+           Do not force each worker to run on an isolated physical core.
+
        -s VALUE, --solver=VALUE (absent=Z3)
            SMT solver to use. VALUE must be one of the 5 available solvers:
            Z3, Bitwuzla, Colibri2, cvc5, Alt-Ergo
@@ -55,7 +58,7 @@ OPTIONS
            skip typechecking pass
 
        -w VAL, --workers=VAL (absent=n)
-           number of workers for symbolic execution. Defaults to the number
+           Number of workers for symbolic execution. Defaults to the number
            of physical cores.
 
        --with-breadcrumbs

doc/src/manpages/owi-rust.md

@@ -63,6 +63,9 @@ OPTIONS
        --no-value
            do not display a value for each symbol
 
+       --no-worker-isolation
+           Do not force each worker to run on an isolated physical core.
+
        -o FILE, --output=FILE
            Output the generated .wasm or .wat to FILE.
 
@@ -77,7 +80,7 @@ OPTIONS
            skip typechecking pass
 
        -w VAL, --workers=VAL (absent=n)
-           number of workers for symbolic execution. Defaults to the number
+           Number of workers for symbolic execution. Defaults to the number
            of physical cores.
 
        --with-breadcrumbs

doc/src/manpages/owi-sym.md

@@ -56,6 +56,9 @@ OPTIONS
        --no-value
            do not display a value for each symbol
 
+       --no-worker-isolation
+           Do not force each worker to run on an isolated physical core.
+
        -s VALUE, --solver=VALUE (absent=Z3)
            SMT solver to use. VALUE must be one of the 5 available solvers:
            Z3, Bitwuzla, Colibri2, cvc5, Alt-Ergo
@@ -64,7 +67,7 @@ OPTIONS
            skip typechecking pass
 
        -w VAL, --workers=VAL (absent=n)
-           number of workers for symbolic execution. Defaults to the number
+           Number of workers for symbolic execution. Defaults to the number
            of physical cores.
 
        --with-breadcrumbs

doc/src/manpages/owi-zig.md

@@ -60,6 +60,9 @@ OPTIONS
        --no-value
            do not display a value for each symbol
 
+       --no-worker-isolation
+           Do not force each worker to run on an isolated physical core.
+
        -o FILE, --output=FILE
            Output the generated .wasm or .wat to FILE.
 
@@ -71,7 +74,7 @@ OPTIONS
            skip typechecking pass
 
        -w VAL, --workers=VAL (absent=n)
-           number of workers for symbolic execution. Defaults to the number
+           Number of workers for symbolic execution. Defaults to the number
            of physical cores.
 
        --with-breadcrumbs

dune-project

@@ -80,6 +80,7 @@
    (>= 1.0.3))
   (xmlm
    (>= 1.4.0))
+  domainpc
   ;; doc
   (odoc
    (and

owi.opam

@@ -42,6 +42,7 @@ depends: [
   "synchronizer" {>= "0.2"}
   "uutf" {>= "1.0.3"}
   "xmlm" {>= "1.4.0"}
+  "domainpc"
   "odoc" {>= "3.0.0" & with-doc}
   "mdx" {with-test & >= "2.1"}
   "frama-c" {>= "29.0" & with-test}
@@ -82,3 +83,8 @@ post-messages: [
   "Join our community on Zulip: https://owi.zulipchat.com/"
   "Explore tutorials and documentation here: https://ocamlpro.github.io/owi/"
 ]
+pin-depends: [
+  ["domainpc.dev" "git+https://github.com/ocamlpro/domainpc.git"]
+  ["landmarks.1.5" "git+https://github.com/hra687261/landmarks.git#cfc017b604f2c41ac0d8841f30a0b55b0d89cbaf"]
+  ["landmarks-ppx.1.5" "git+https://github.com/hra687261/landmarks.git#cfc017b604f2c41ac0d8841f30a0b55b0d89cbaf"]
+]

owi.opam.template

@@ -11,3 +11,8 @@ post-messages: [
   "Join our community on Zulip: https://owi.zulipchat.com/"
   "Explore tutorials and documentation here: https://ocamlpro.github.io/owi/"
 ]
+pin-depends: [
+  ["domainpc.dev" "git+https://github.com/ocamlpro/domainpc.git"]
+  ["landmarks.1.5" "git+https://github.com/hra687261/landmarks.git#cfc017b604f2c41ac0d8841f30a0b55b0d89cbaf"]
+  ["landmarks-ppx.1.5" "git+https://github.com/hra687261/landmarks.git#cfc017b604f2c41ac0d8841f30a0b55b0d89cbaf"]
+]

shell.nix

@@ -8,11 +8,27 @@ let
     src = pkgs.fetchFromGitHub {
       owner = "formalsec";
       repo = "smtml";
-      rev = "3b08a5368718068fa46547e60df4e44caa51db78";
-      hash = "sha256-iD2UGddGYvE/jn+KM5jj05DHcNPjSq9IiH1BlnfO+Sg=";
+      rev = "e259d5b7d108cb2d1102c188132a6c86bbf7705e";
+      hash = "sha256-8OzNJIyJhfqgDw3ioINN0D0WVTSliG9TP4cUNlrm4s8=";
     };
     doCheck = false;
   });
+  domainpc = pkgs.ocamlPackages.buildDunePackage (finalAttrs: {
+
+    pname = "domainpc";
+    version = "0.1";
+
+    src = pkgs.fetchFromGitHub {
+      owner = "ocamlpro";
+      repo = "domainpc";
+      rev = "9d5596c57154d925c6d7f17fe37dc2b9da0434bc";
+      hash = "sha256-ttuv/G2J+7DsmDMMRtUOT1jITUtCoj9qQUXzfJ/yRfc=";
+    };
+
+    propagatedBuildInputs = [
+      pkgs.ocamlPackages.processor
+    ];
+  });
   synchronizer = pkgs.ocamlPackages.synchronizer.overrideAttrs (old: {
     src = pkgs.fetchFromGitHub {
       owner = "ocamlpro";
@@ -21,6 +37,23 @@ let
       hash = "sha256-0XtPHpDlyH1h8W2ZlRvJbZjCN9WP5mzk2N01WFd8eLQ=";
     };
   });
+  landmarks = pkgs.ocamlPackages.landmarks.overrideAttrs (old: {
+    src = pkgs.fetchFromGitHub {
+      owner = "hra687261";
+      repo = "landmarks";
+      rev = "17be3567a63650090f9cf94654fcc8d99f946e27";
+      hash = "sha256-3ui4uvSAvUgzk2UMVtH9A4BhAX6nWbwx7q0YwkANNv8=";
+    };
+  });
+  landmarks-ppx = pkgs.ocamlPackages.landmarks-ppx.overrideAttrs (old: {
+    src = pkgs.fetchFromGitHub {
+      owner = "hra687261";
+      repo = "landmarks";
+      rev = "17be3567a63650090f9cf94654fcc8d99f946e27";
+      hash = "sha256-3ui4uvSAvUgzk2UMVtH9A4BhAX6nWbwx7q0YwkANNv8=";
+    };
+    meta.broken = false;
+  });
 in
 
 pkgs.mkShell {
@@ -31,6 +64,8 @@ pkgs.mkShell {
     findlib
     bisect_ppx
     pkgs.framac
+    landmarks
+    landmarks-ppx
     pkgs.mdbook
     pkgs.mdbook-plugins
     mdx
@@ -57,6 +92,7 @@ pkgs.mkShell {
     crowbar
     digestif
     dolmen_type
+    domainpc
     dune-build-info
     dune-site
     hc

src/bin/owi.ml

@@ -173,6 +173,10 @@ let no_value =
   let doc = "do not display a value for each symbol" in
   Arg.(value & flag & info [ "no-value" ] ~doc)
 
+let no_worker_isolation =
+  let doc = "Do not force each worker to run on an isolated physical core." in
+  Arg.(value & flag & info [ "no-worker-isolation" ] ~doc)
+
 let opt_lvl =
   let doc = "specify which optimization level to use" in
   Arg.(value & opt string "3" & info [ "O" ] ~doc)
@@ -234,13 +238,10 @@ let unsafe =
 
 let workers =
   let doc =
-    "number of workers for symbolic execution. Defaults to the number of \
+    "Number of workers for symbolic execution. Defaults to the number of \
      physical cores."
   in
-  Arg.(
-    value
-    & opt int Processor.Query.core_count
-    & info [ "workers"; "w" ] ~doc ~absent:"n" )
+  Arg.(value & opt (some int) None & info [ "workers"; "w" ] ~doc ~absent:"n")
 
 let workspace =
   let doc = "write results and intermediate compilation artifacts to dir" in
@@ -259,6 +260,7 @@ let no_ite_for_select =
 let symbolic_parameters default_entry_point =
   let+ unsafe
   and+ workers
+  and+ no_worker_isolation
   and+ no_stop_at_failure
   and+ no_value
   and+ no_assert_failure_expression_printing
@@ -276,6 +278,7 @@ let symbolic_parameters default_entry_point =
   let use_ite_for_select = not no_ite_for_select in
   { Symbolic_parameters.unsafe
   ; workers
+  ; no_worker_isolation
   ; no_stop_at_failure
   ; no_value
   ; no_assert_failure_expression_printing
@@ -446,14 +449,15 @@ let iso_cmd =
   and+ solver
   and+ unsafe
   and+ workers
+  and+ no_worker_isolation
   and+ model_out_file
   and+ with_breadcrumbs
   and+ workspace in
 
   Cmd_iso.cmd ~deterministic_result_order ~fail_mode ~exploration_strategy
     ~files ~model_format ~no_assert_failure_expression_printing
-    ~no_stop_at_failure ~no_value ~solver ~unsafe ~workers ~workspace
-    ~model_out_file ~with_breadcrumbs
+    ~no_stop_at_failure ~no_value ~solver ~unsafe ~workers ~no_worker_isolation
+    ~workspace ~model_out_file ~with_breadcrumbs
 
 (* owi replay *)
 

src/cmd/cmd_iso.ml

@@ -297,8 +297,8 @@ module String_set = Set.Make (String)
 
 let cmd ~deterministic_result_order ~fail_mode ~exploration_strategy ~files
   ~model_format ~no_assert_failure_expression_printing ~no_stop_at_failure
-  ~no_value ~solver ~unsafe ~workers ~workspace ~model_out_file
-  ~with_breadcrumbs =
+  ~no_value ~solver ~unsafe ~workers ~no_worker_isolation ~workspace
+  ~model_out_file ~with_breadcrumbs =
   let* workspace =
     match workspace with
     | Some path -> Ok path
@@ -407,7 +407,7 @@ let cmd ~deterministic_result_order ~fail_mode ~exploration_strategy ~files
       let run_time = if Log.is_bench_enabled () then Some 0. else None in
 
       Symbolic_driver.handle_result ~exploration_strategy ~fail_mode ~workers
-        ~solver ~deterministic_result_order ~model_format ~no_value
-        ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure
-        ~model_out_file ~with_breadcrumbs ~run_time result )
+        ~no_worker_isolation ~solver ~deterministic_result_order ~model_format
+        ~no_value ~no_assert_failure_expression_printing ~workspace
+        ~no_stop_at_failure ~model_out_file ~with_breadcrumbs ~run_time result )
     () common_exports

src/cmd/cmd_iso.mli

@@ -9,7 +9,8 @@ val cmd :
   -> no_value:bool
   -> solver:Smtml.Solver_type.t
   -> unsafe:bool
-  -> workers:int
+  -> workers:Int.t Option.t
+  -> no_worker_isolation:Bool.t
   -> workspace:Fpath.t option
   -> model_out_file:Fpath.t option
   -> with_breadcrumbs:bool

src/cmd/cmd_sym.ml

@@ -54,6 +54,7 @@ let cmd ~parameters ~source_file =
   let { Symbolic_parameters.exploration_strategy
       ; fail_mode
       ; workers
+      ; no_worker_isolation
       ; solver
       ; deterministic_result_order
       ; model_format
@@ -82,6 +83,6 @@ let cmd ~parameters ~source_file =
   let* result, run_time = run_file ~parameters ~source_file in
 
   Symbolic_driver.handle_result ~exploration_strategy ~fail_mode ~workers
-    ~solver ~deterministic_result_order ~model_format ~no_value
-    ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure
-    ~model_out_file ~with_breadcrumbs ~run_time result
+    ~no_worker_isolation ~solver ~deterministic_result_order ~model_format
+    ~no_value ~no_assert_failure_expression_printing ~workspace
+    ~no_stop_at_failure ~model_out_file ~with_breadcrumbs ~run_time result