diff --git a/doc/src/hacking/benchmarking.md b/doc/src/hacking/benchmarking.md index 897cac202..0d7e06392 100644 --- a/doc/src/hacking/benchmarking.md +++ b/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 diff --git a/doc/src/manpages/owi-c.md b/doc/src/manpages/owi-c.md index 295cc7fb8..56d4783e5 100644 --- a/doc/src/manpages/owi-c.md +++ b/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 diff --git a/doc/src/manpages/owi-cpp.md b/doc/src/manpages/owi-cpp.md index 088aed0fb..34ade695e 100644 --- a/doc/src/manpages/owi-cpp.md +++ b/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 diff --git a/doc/src/manpages/owi-iso.md b/doc/src/manpages/owi-iso.md index b9d48ac50..8c74fee57 100644 --- a/doc/src/manpages/owi-iso.md +++ b/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 diff --git a/doc/src/manpages/owi-rust.md b/doc/src/manpages/owi-rust.md index e00017fc2..9c25d3f59 100644 --- a/doc/src/manpages/owi-rust.md +++ b/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 diff --git a/doc/src/manpages/owi-sym.md b/doc/src/manpages/owi-sym.md index d46321e85..8173264af 100644 --- a/doc/src/manpages/owi-sym.md +++ b/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 diff --git a/doc/src/manpages/owi-zig.md b/doc/src/manpages/owi-zig.md index e011011ca..24832bf9c 100644 --- a/doc/src/manpages/owi-zig.md +++ b/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 diff --git a/dune-project b/dune-project index 7ed58e996..21a8aab23 100644 --- a/dune-project +++ b/dune-project @@ -80,6 +80,7 @@ (>= 1.0.3)) (xmlm (>= 1.4.0)) + domainpc ;; doc (odoc (and diff --git a/owi.opam b/owi.opam index c71d9ab67..2a5a7d73f 100644 --- a/owi.opam +++ b/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"] +] diff --git a/owi.opam.template b/owi.opam.template index abe9a436a..e60187165 100644 --- a/owi.opam.template +++ b/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"] +] diff --git a/shell.nix b/shell.nix index df8ca9a6c..492054a75 100644 --- a/shell.nix +++ b/shell.nix @@ -4,6 +4,22 @@ }: let + domainpc = pkgs.ocamlPackages.buildDunePackage (finalAttrs: { + + pname = "domainpc"; + version = "0.19.0"; + + src = pkgs.fetchFromGitHub { + owner = "redianthus"; + repo = "domainpc"; + rev = "289d4940a8f95f31defb3594be28f44749ff6afd"; + hash = "sha256-v5FpsHvXCLKEpn0c2gEBGK15yPJQE5ZzwSq5foXv8VE="; + }; + + propagatedBuildInputs = [ + pkgs.ocamlPackages.processor + ]; + }); synchronizer = pkgs.ocamlPackages.synchronizer.overrideAttrs (old: { src = pkgs.fetchFromGitHub { owner = "ocamlpro"; @@ -12,6 +28,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 { @@ -22,6 +55,8 @@ pkgs.mkShell { findlib bisect_ppx pkgs.framac + landmarks + landmarks-ppx pkgs.mdbook pkgs.mdbook-plugins mdx @@ -48,6 +83,7 @@ pkgs.mkShell { crowbar digestif dolmen_type + domainpc dune-build-info dune-site hc diff --git a/src/bin/owi.ml b/src/bin/owi.ml index c60dc810d..76e941bef 100644 --- a/src/bin/owi.ml +++ b/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 *) diff --git a/src/cmd/cmd_iso.ml b/src/cmd/cmd_iso.ml index 7c7d7f470..c9f8c0ca2 100644 --- a/src/cmd/cmd_iso.ml +++ b/src/cmd/cmd_iso.ml @@ -299,8 +299,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 @@ -409,7 +409,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 diff --git a/src/cmd/cmd_iso.mli b/src/cmd/cmd_iso.mli index 0320e81cd..a5a54d97d 100644 --- a/src/cmd/cmd_iso.mli +++ b/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 diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml index 05cdfe9c4..b97ca3035 100644 --- a/src/cmd/cmd_sym.ml +++ b/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 diff --git a/src/compile/binary_to_text.ml b/src/compile/binary_to_text.ml index 47c50d405..30e43a6f7 100644 --- a/src/compile/binary_to_text.ml +++ b/src/compile/binary_to_text.ml @@ -2,18 +2,18 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -let convert_indice : Binary.indice -> Text.indice = function i -> Raw i +let convert_indice : Binary.indice -> Text.indice = function i -> Text.Raw i let convert_block_type : Binary.block_type -> Text.block_type = function - | Bt_raw (opt, ft) -> + | Binary.Bt_raw (opt, ft) -> let opt = Option.map convert_indice opt in - Bt_raw (opt, ft) + Text.Bt_raw (opt, ft) let rec convert_instr : Binary.instr -> Text.instr = function - | Br_table (ids, id) -> + | Binary.Br_table (ids, id) -> let ids = Array.map convert_indice ids in let id = convert_indice id in - Br_table (ids, id) + Text.Br_table (ids, id) | Br_if id -> let id = convert_indice id in Br_if id @@ -169,7 +169,7 @@ and convert_expr (e : Binary.expr Annotated.t) : Text.expr Annotated.t = e let convert_elem_mode : Binary.Elem.Mode.t -> Text.Elem.Mode.t = function - | Passive -> Passive + | Binary.Elem.Mode.Passive -> Text.Elem.Mode.Passive | Declarative -> Declarative | Active (opt, e) -> let opt = Option.map (fun i -> Text.Raw i) opt in @@ -177,21 +177,21 @@ let convert_elem_mode : Binary.Elem.Mode.t -> Text.Elem.Mode.t = function Active (opt, e) let convert_elem : Binary.Elem.t -> Text.Elem.t = function - | { id; typ; init; mode } -> + | { Binary.Elem.id; typ; init; mode } -> let init = List.map convert_expr init in let mode = convert_elem_mode mode in - { id; typ; init; mode } + { Text.Elem.id; typ; init; mode } let convert_data_mode : Binary.Data.Mode.t -> Text.Data.Mode.t = function - | Passive -> Passive + | Binary.Data.Mode.Passive -> Text.Data.Mode.Passive | Active (i, e) -> let e = convert_expr e in Active (Some (Raw i), e) let convert_data : Binary.Data.t -> Text.Data.t = function - | { id; init; mode } -> + | { Binary.Data.id; init; mode } -> let mode = convert_data_mode mode in - { id; init; mode } + { Text.Data.id; init; mode } let from_types types : Text.Module.Field.t list = Array.map (fun (t : Text.Typedef.t) -> Text.Module.Field.Typedef t) types diff --git a/src/dune b/src/dune index b3d1da268..eebcd5453 100644 --- a/src/dune +++ b/src/dune @@ -136,6 +136,7 @@ (libraries bos digestif + domainpc dune-build-info dune-site fmt diff --git a/src/intf/symbolic_choice_intf.ml b/src/intf/symbolic_choice_intf.ml index 62afe458f..61817b2a6 100644 --- a/src/intf/symbolic_choice_intf.ml +++ b/src/intf/symbolic_choice_intf.ml @@ -70,7 +70,8 @@ module type S = sig val run : Symbolic_parameters.Exploration_strategy.t - -> workers:int + -> workers:Int.t Option.t + -> no_worker_isolation:Bool.t -> Smtml.Solver_type.t -> 'a t -> thread diff --git a/src/ir/extern.ml b/src/ir/extern.ml index 4f4c4908e..1a74d2ce3 100644 --- a/src/ir/extern.ml +++ b/src/ir/extern.ml @@ -172,12 +172,15 @@ module Func = struct | R3 (a, b, c) -> [ elt_type a; elt_type b; elt_type c ] | R4 (a, b, c, d) -> [ elt_type a; elt_type b; elt_type c; elt_type d ] - let rec arg_type : type t r. (t, r) atype -> Text.param_type = function - | Mem (_, tl) -> arg_type tl - | UArg tl -> arg_type tl - | Arg (hd, tl) -> (None, elt_type hd) :: arg_type tl - | NArg (name, hd, tl) -> (Some name, elt_type hd) :: arg_type tl - | Res -> [] + let arg_type = + let rec aux : type t r. (t, r) atype -> Text.param_type = function + | Mem (_, tl) -> aux tl + | UArg tl -> aux tl + | Arg (hd, tl) -> (None, elt_type hd) :: aux tl + | NArg (name, hd, tl) -> (Some name, elt_type hd) :: aux tl + | Res -> [] + in + aux (* TODO: we could move this out, as it does not really depend on the functor's parameters *) let extern_type (Extern_func (Func (arg, res), _)) : Text.func_type = @@ -234,18 +237,24 @@ module Func = struct let label s (Elt v) = Elt_labeled (s, v) - let ( ^-> ) : type lr k a b. - (lr, k, a) t -> b func_type -> (a -> b) func_type = - fun a (Func (b, r)) -> - match a with - | Elt a -> Func (Arg (a, b), r) - | Elt_labeled (label, a) -> Func (NArg (label, a, b), r) - | Unit -> Func (UArg b, r) - | Memory id -> Func (Mem (id, b), r) - - let ( ^->. ) : type ll k kk a b. - (ll, k, a) t -> (lr, kk, b) t -> (a -> b m) func_type = - fun a b -> match b with Elt _ -> a ^-> r1 b | Unit -> a ^-> r0 + let ( ^-> ) = + let aux : type lr k a b. + (lr, k, a) t -> b func_type -> (a -> b) func_type = + fun a (Func (b, r)) -> + match a with + | Elt a -> Func (Arg (a, b), r) + | Elt_labeled (label, a) -> Func (NArg (label, a, b), r) + | Unit -> Func (UArg b, r) + | Memory id -> Func (Mem (id, b), r) + in + aux + + let ( ^->. ) = + let aux : type ll k kk a b. + (ll, k, a) t -> (lr, kk, b) t -> (a -> b m) func_type = + fun a b -> match b with Elt _ -> a ^-> r1 b | Unit -> a ^-> r0 + in + aux let ( ^->.. ) : type ll k a b1 b2. (ll, k, a) t diff --git a/src/owi.mli b/src/owi.mli index 2d27a997b..7ddc6bd84 100644 --- a/src/owi.mli +++ b/src/owi.mli @@ -1118,7 +1118,8 @@ module Symbolic_parameters : sig type t = { unsafe : bool - ; workers : int + ; workers : Int.t Option.t + ; no_worker_isolation : Bool.t ; no_stop_at_failure : bool ; no_value : bool ; no_assert_failure_expression_printing : bool @@ -1139,7 +1140,8 @@ end module Symbolic_driver : sig val handle_result : exploration_strategy:Symbolic_parameters.Exploration_strategy.t - -> workers:int + -> workers:Int.t Option.t + -> no_worker_isolation:Bool.t -> no_stop_at_failure:bool -> no_value:bool -> no_assert_failure_expression_printing:bool @@ -1225,7 +1227,8 @@ module Cmd_iso : sig -> 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 diff --git a/src/script/script.ml b/src/script/script.ml index 030af832b..bb6bd44f7 100644 --- a/src/script/script.ml +++ b/src/script/script.ml @@ -115,7 +115,7 @@ let compare_result_const result (const : Concrete_value.t) = assert false let value_of_const : Wast.const -> Concrete_value.t = function - | Const_I32 v -> Concrete_value.I32 v + | Wast.Const_I32 v -> Concrete_value.I32 v | Const_I64 v -> Concrete_value.I64 v | Const_F32 v -> Concrete_value.F32 v | Const_F64 v -> Concrete_value.F64 v diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml index 958dc6e24..59079e4e2 100644 --- a/src/symbolic/symbolic_choice.ml +++ b/src/symbolic/symbolic_choice.ml @@ -92,29 +92,26 @@ module CoreImpl = struct (fun f write_back -> handle_status (Schedulable.run f wls) write_back) sched.work_queue - let spawn_worker sched wls_init ~at_worker_value ~at_worker_init - ~at_worker_end = - at_worker_init (); - Domain.spawn (fun () -> - Fun.protect ~finally:at_worker_end (fun () -> - try - let wls = wls_init () in - work wls sched - (at_worker_value ~close_work_queue:(fun () -> - Work_datastructure.close sched.work_queue ) ) - with e -> - let e_s = Printexc.to_string e in - let bt = Printexc.get_raw_backtrace () in - let bt_s = Printexc.raw_backtrace_to_string bt in - let bt_s = - if String.equal "" bt_s then - "use OCAMLRUNPARAM=b to get the backtrace" - else bt_s - in - Log.err (fun m -> - m "a worker ended with exception %s, backtrace is: @\n@[%s@]" - e_s bt_s ); - Printexc.raise_with_backtrace e bt ) ) + let run_worker sched wls_init ~at_worker_value ~at_worker_end () = + Fun.protect ~finally:at_worker_end (fun () -> + try + let wls = wls_init () in + work wls sched + (at_worker_value ~close_work_queue:(fun () -> + Work_datastructure.close sched.work_queue ) ) + with e -> + let e_s = Printexc.to_string e in + let bt = Printexc.get_raw_backtrace () in + let bt_s = Printexc.raw_backtrace_to_string bt in + let bt_s = + if String.equal "" bt_s then + "use OCAMLRUNPARAM=b to get the backtrace" + else bt_s + in + Log.err (fun m -> + m "a worker ended with exception %s, backtrace is: @\n@[%s@]" e_s + bt_s ); + Printexc.raise_with_backtrace e bt ) end module State = struct @@ -260,7 +257,8 @@ module CoreImpl = struct val run : Symbolic_parameters.Exploration_strategy.t - -> workers:int + -> workers:Int.t Option.t + -> no_worker_isolation:Bool.t -> Smtml.Solver_type.t -> 'a t -> thread @@ -311,8 +309,13 @@ module CoreImpl = struct type 'a run_result = ('a eval * Thread.t) Seq.t - let run exploration_strategy ~workers solver t thread ~at_worker_value - ~at_worker_init ~at_worker_end = + let rec repeat n f = + if n > 0 then ( + f (); + repeat (n - 1) f ) + + let run exploration_strategy ~workers ~no_worker_isolation solver t thread + ~at_worker_value ~at_worker_init ~at_worker_end = let module M = ( val Symbolic_parameters.Exploration_strategy.to_work_ds_module exploration_strategy ) @@ -321,10 +324,29 @@ module CoreImpl = struct let open Scheduler in let sched = init_scheduler () in add_init_task sched (State.run t thread); - if workers > 1 then Logs_threaded.enable (); - Array.init workers (fun _i -> - spawn_worker sched (Solver.fresh solver) ~at_worker_value - ~at_worker_init ~at_worker_end ) + begin match workers with + | Some (0 | 1) -> () + | None | Some _ -> Logs_threaded.enable () + end; + + let spawn_one_worker () = + run_worker sched (Solver.fresh solver) ~at_worker_value ~at_worker_end + () + in + + if no_worker_isolation then begin + let workers = + match workers with None -> Processor.Query.core_count | Some v -> v + in + Array.init workers (fun _i -> + at_worker_init (); + Domain.spawn spawn_one_worker ) + end + else begin + let n = Domainpc.get_available_cores () in + repeat n at_worker_init; + Domainpc.spawn_n ?n:workers spawn_one_worker + end let trap t = let* thread in @@ -339,7 +361,7 @@ module CoreImpl = struct | None -> (* It can happen when the solver is interrupted *) (* TODO: once https://github.com/formalsec/smtml/pull/479 is merged - if solver was interrupted then stop else assert false *) + if solver was interrupted then stop else assert false *) stop in let labels = Thread.labels thread in @@ -483,7 +505,7 @@ module Make (Thread : Thread_intf.S) = struct | `Unknown -> (* It can happen when the solver is interrupted *) (* TODO: once https://github.com/formalsec/smtml/pull/479 is merged - if solver was interrupted then stop else assert false *) + if solver was interrupted then stop else assert false *) stop end end diff --git a/src/symbolic/symbolic_driver.ml b/src/symbolic/symbolic_driver.ml index c28b55115..0ca7c9dd8 100644 --- a/src/symbolic/symbolic_driver.ml +++ b/src/symbolic/symbolic_driver.ml @@ -73,9 +73,10 @@ let mk_callback no_stop_at_failure fail_mode res_stack path_count = end | (Trap_only | Assertion_only), _ -> () -let handle_result ~exploration_strategy ~workers ~no_stop_at_failure ~no_value - ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode - ~workspace ~solver ~model_format ~model_out_file ~with_breadcrumbs ~run_time +let handle_result ~exploration_strategy ~workers ~no_worker_isolation + ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing + ~deterministic_result_order ~fail_mode ~workspace ~solver ~model_format + ~model_out_file ~with_breadcrumbs ~run_time (result : unit Symbolic_choice_with_memory.t) = let thread = Thread_with_memory.init () in let res_stack = Outcome.make () in @@ -85,8 +86,8 @@ let handle_result ~exploration_strategy ~workers ~no_stop_at_failure ~no_value in let time_before = (Unix.times ()).tms_utime in let domains : unit Domain.t Array.t = - Symbolic_choice_with_memory.run exploration_strategy ~workers solver result - thread ~at_worker_value + Symbolic_choice_with_memory.run exploration_strategy ~workers + ~no_worker_isolation solver result thread ~at_worker_value ~at_worker_init:(fun () -> Outcome.new_pledge res_stack) ~at_worker_end:(fun () -> Outcome.end_pledge res_stack) in @@ -127,8 +128,14 @@ let handle_result ~exploration_strategy ~workers ~no_stop_at_failure ~no_value Benchmark.print_final ~bench_stats ~execution_time_a:run_time ~execution_time_b ~wait_for_all_domains end - else if Log.is_debug_enabled () then begin - (* we only do this in debug mode because otherwise it makes performances very bad *) + else if + let landmark_profiling_enabled = + Option.is_some @@ Bos.OS.Env.var "OCAML_LANDMARKS" + in + Log.is_debug_enabled () || landmark_profiling_enabled + then begin + (* we only do this in debug mode or when landmarks profiling is on because + otherwise it makes performances very bad *) wait_for_all_domains () end; diff --git a/src/symbolic/symbolic_driver.mli b/src/symbolic/symbolic_driver.mli index 555ae7eb8..39c925949 100644 --- a/src/symbolic/symbolic_driver.mli +++ b/src/symbolic/symbolic_driver.mli @@ -4,7 +4,8 @@ val handle_result : exploration_strategy:Symbolic_parameters.Exploration_strategy.t - -> workers:int + -> workers:Int.t Option.t + -> no_worker_isolation:Bool.t -> no_stop_at_failure:bool -> no_value:bool -> no_assert_failure_expression_printing:bool diff --git a/src/symbolic/symbolic_parameters.ml b/src/symbolic/symbolic_parameters.ml index 15f9cb147..ff768b364 100644 --- a/src/symbolic/symbolic_parameters.ml +++ b/src/symbolic/symbolic_parameters.ml @@ -17,7 +17,7 @@ module Exploration_strategy = struct | Rarity_depth_loop_aging_random let to_priority_module : t -> (module Prio.T) = function - | LIFO -> (module Prio.LIFO) + | LIFO -> (module Prio.LIFO : Prio.T) | FIFO -> (module Prio.FIFO) | Random -> (module Prio.Random_prio) | Random_unseen_then_random -> (module Prio.Random_unseen_then_random) @@ -65,7 +65,8 @@ end type t = { unsafe : bool - ; workers : int + ; workers : Int.t Option.t + ; no_worker_isolation : Bool.t ; no_stop_at_failure : bool ; no_value : bool ; no_assert_failure_expression_printing : bool diff --git a/src/symbolic/symbolic_parameters.mli b/src/symbolic/symbolic_parameters.mli index e433e5df7..dd07c9fc0 100644 --- a/src/symbolic/symbolic_parameters.mli +++ b/src/symbolic/symbolic_parameters.mli @@ -25,7 +25,8 @@ end type t = { unsafe : bool - ; workers : int + ; workers : Int.t Option.t + ; no_worker_isolation : Bool.t ; no_stop_at_failure : bool ; no_value : bool ; no_assert_failure_expression_printing : bool