A handful of tentative performance improvements

dune-project

@@ -74,5 +74,6 @@
   digestif
   xmlm
   (hc (>= 0.3))
+  (processor (>= 0.1))
   dune-site)
  (sites (share pyc) (share binc) (share libc)))

owi.opam

@@ -42,6 +42,7 @@ depends: [
   "digestif"
   "xmlm"
   "hc" {>= "0.3"}
+  "processor" {>= "0.1"}
   "dune-site"
 ]
 build: [

src/bin/owi.ml

@@ -60,12 +60,12 @@ let unsafe =
 
 let workers =
   let doc =
-    "number of workers for symbolic execution. Defaults to a machine-specific \
-     value given by the OCaml Domain.recommended_domain_count function."
+    "number of workers for symbolic execution. Defaults to the number of \
+     physical cores."
   in
   Cmdliner.Arg.(
     value
-    & opt int (Domain.recommended_domain_count ())
+    & opt int Processor.Query.core_count
     & info [ "workers"; "w" ] ~doc ~absent:"n" )
 
 let workspace =

src/cmd/cmd_sym.ml

@@ -244,7 +244,20 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
   let pc = Choice.return (Ok ()) in
   let result = List.fold_left (run_file ~unsafe ~optimize) pc files in
   let thread : Thread.t = Thread.create () in
-  let results = Symbolic_choice.run ~workers result thread in
+  let res_queue = Wq.init () in
+  let callback = function
+    | Symbolic_choice.EVal (Ok ()), _ -> ()
+    | v -> Wq.push v res_queue
+  in
+  let join_handles =
+    Symbolic_choice.run ~workers result thread ~callback
+      ~callback_init:(fun () -> Wq.make_pledge res_queue)
+      ~callback_end:(fun () -> Wq.end_pledge res_queue)
+  in
+  let results =
+    Wq.read_as_seq res_queue ~finalizer:(fun () ->
+        Array.iter Domain.join join_handles )
+  in
   let print_bug = function
     | `ETrap (tr, model) ->
       Format.pp_std "Trap: %s@\n" (Trap.to_string tr);

src/data_structures/wq.ml

@@ -36,7 +36,7 @@ let make_pledge q =
 let end_pledge q =
   Mutex.lock q.mutex;
   q.pledges <- q.pledges - 1;
-  Condition.broadcast q.cond;
+  if q.pledges = 0 then Condition.broadcast q.cond;
   Mutex.unlock q.mutex
 
 let rec read_as_seq (q : 'a t) ~finalizer : 'a Seq.t =
@@ -49,9 +49,8 @@ let rec read_as_seq (q : 'a t) ~finalizer : 'a Seq.t =
 
 let push v q =
   Mutex.lock q.mutex;
-  let was_empty = Queue.is_empty q.queue in
   Queue.push v q.queue;
-  if was_empty then Condition.broadcast q.cond;
+  Condition.signal q.cond;
   Mutex.unlock q.mutex
 
 let fail q =

src/dune

@@ -98,6 +98,7 @@
   menhirLib
   ocaml_intrinsics
   ppxlib
+  processor
   sedlex
   uutf
   runtime_events

src/symbolic/symbolic_choice.ml

@@ -65,7 +65,14 @@ module CoreImpl : sig
 
   type 'a run_result = ('a eval * Thread.t) Seq.t
 
-  val run : workers:int -> 'a t -> Thread.t -> 'a run_result
+  val run :
+       workers:int
+    -> 'a t
+    -> Thread.t
+    -> callback:('a eval * Thread.t -> unit)
+    -> callback_init:(unit -> unit)
+    -> callback_end:(unit -> unit)
+    -> unit Domain.t array
 end = struct
   module Schedulable = struct
     (*
@@ -127,25 +134,19 @@ end = struct
       *)
     type ('a, 'wls) work_queue = ('a, 'wls) Schedulable.t Wq.t
 
-    type 'a res_queue = 'a Wq.t
-
-    type ('a, 'wls) t =
-      { work_queue : ('a, 'wls) work_queue
-      ; res_writer : 'a res_queue
-      }
+    type ('a, 'wls) t = { work_queue : ('a, 'wls) work_queue }
 
     let init_scheduler () =
       let work_queue = Wq.init () in
-      let res_writer = Wq.init () in
-      { work_queue; res_writer }
+      { work_queue }
 
     let add_init_task sched task = Wq.push task sched.work_queue
 
-    let rec work wls sched =
+    let rec work wls sched callback =
       let rec handle_status (t : _ Schedulable.status) sched =
         match t with
         | Stop -> ()
-        | Now x -> Wq.push x sched.res_writer
+        | Now x -> callback x
         | Yield (_prio, f) -> Wq.push f sched.work_queue
         | Choice (m1, m2) ->
           handle_status m1 sched;
@@ -156,17 +157,17 @@ end = struct
       | Some f -> begin
         handle_status (Schedulable.run f wls) sched;
         Wq.end_pledge sched.work_queue;
-        work wls sched
+        work wls sched callback
       end
 
-    let spawn_worker sched wls_init =
-      Wq.make_pledge sched.res_writer;
+    let spawn_worker sched wls_init callback callback_init callback_close =
+      callback_init ();
       Domain.spawn (fun () ->
           let wls = wls_init () in
           Fun.protect
-            ~finally:(fun () -> Wq.end_pledge sched.res_writer)
+            ~finally:(fun () -> callback_close ())
             (fun () ->
-              try work wls sched
+              try work wls sched callback
               with e ->
                 let bt = Printexc.get_raw_backtrace () in
                 Wq.fail sched.work_queue;
@@ -295,17 +296,15 @@ end = struct
 
   type 'a run_result = ('a eval * Thread.t) Seq.t
 
-  let run ~workers t thread =
+  let run ~workers t thread ~callback ~callback_init ~callback_end =
     let open Scheduler in
     let sched = init_scheduler () in
     add_init_task sched (State.run t thread);
     let join_handles =
-      Array.map
-        (fun () -> spawn_worker sched Solver.fresh)
-        (Array.init workers (Fun.const ()))
+      Array.init workers (fun _i ->
+          spawn_worker sched Solver.fresh callback callback_init callback_end )
     in
-    Wq.read_as_seq sched.res_writer ~finalizer:(fun () ->
-        Array.iter Domain.join join_handles )
+    join_handles
 
   let trap t =
     let* thread in
@@ -367,7 +366,7 @@ let get_model_or_stop symbol =
     | Some v -> return v
   end
 
-let select (cond : Symbolic_value.vbool) =
+let select_inner ~explore_first (cond : Symbolic_value.vbool) =
   let v = Smtml.Expr.simplify cond in
   match Smtml.Expr.view v with
   | Val True -> return true
@@ -386,7 +385,11 @@ let select (cond : Symbolic_value.vbool) =
       let+ () = check_reachability in
       false
     in
-    choose true_branch false_branch
+    if explore_first then choose true_branch false_branch
+    else choose false_branch true_branch
+[@@inline]
+
+let select (cond : Symbolic_value.vbool) = select_inner cond ~explore_first:true
 [@@inline]
 
 let summary_symbol (e : Smtml.Expr.t) =
@@ -441,7 +444,7 @@ let select_i32 (i : Symbolic_value.int32) =
     generator ()
 
 let assertion c =
-  let* assertion_true = select c in
+  let* assertion_true = select_inner c ~explore_first:false in
   if assertion_true then return ()
   else
     let* thread in

src/symbolic/symbolic_choice.mli

@@ -13,4 +13,11 @@ include
      and type 'a run_result = ('a eval * Thread.t) Seq.t
      and module V := Symbolic_value
 
-val run : workers:int -> 'a t -> Thread.t -> 'a run_result
+val run :
+     workers:int
+  -> 'a t
+  -> Thread.t
+  -> callback:('a eval * Thread.t -> unit)
+  -> callback_init:(unit -> unit)
+  -> callback_end:(unit -> unit)
+  -> unit Domain.t array

src/text_to_binary/rewrite.ml

@@ -351,7 +351,7 @@ let rewrite_const_expr (modul : Assigned.t) (expr : text expr) :
       match mut with
       | Const -> ok @@ Global_get (Raw idx)
       | Var -> Error `Constant_expression_required
-      end
+    end
     | Ref_null v ->
       let+ v = Binary_types.convert_heap_type None v in
       Ref_null v
@@ -364,7 +364,8 @@ let rewrite_const_expr (modul : Assigned.t) (expr : text expr) :
     | Array_new_default t ->
       let+ t = find "unknown type" modul.typ (Some t) in
       Array_new_default t
-    | (I32_const _ | I64_const _ | F32_const _ | F64_const _ | Ref_i31) | I_binop (_, (Add | Sub | Mul)) as i ->
+    | ( I32_const _ | I64_const _ | F32_const _ | F64_const _ | Ref_i31
+      | I_binop (_, (Add | Sub | Mul)) ) as i ->
       Ok i
     | _i -> Error `Constant_expression_required
   in