Parallelism support: PoC/Suggestion

dune-project

@@ -42,6 +42,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     (zarith (>= 1.10))
     (yojson (>= 2.0.0))
     (qcheck-core (>= 0.19))
+    ppx_optcomp
     (ppx_deriving (>= 6.0.2))
     (ppx_deriving_hash (>= 0.1.2))
     (ppx_deriving_yojson (>= 3.7.0))
@@ -67,6 +68,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     (conf-ruby :with-test)
     (benchmark :with-test) ; TODO: make this optional somehow, (optional) on bench executable doesn't work
     conf-gcc ; ensures opam-repository CI installs real gcc from homebrew on MacOS
+    domain-local-await
   )
   (depopts
     (apron (>= v0.9.15))

goblint.opam

@@ -42,6 +42,7 @@ depends: [
   "zarith" {>= "1.10"}
   "yojson" {>= "2.0.0"}
   "qcheck-core" {>= "0.19"}
+  "ppx_optcomp" 
   "ppx_deriving" {>= "6.0.2"}
   "ppx_deriving_hash" {>= "0.1.2"}
   "ppx_deriving_yojson" {>= "3.7.0"}
@@ -67,6 +68,7 @@ depends: [
   "conf-ruby" {with-test}
   "benchmark" {with-test}
   "conf-gcc"
+  "domain-local-await"
 ]
 depopts: [
   "apron" {>= "v0.9.15"}

src/util/parallel/dune

@@ -0,0 +1,12 @@
+(include_subdirs no)
+
+(library
+ (name goblint_parallel)
+ (public_name goblint.parallel)
+ (libraries
+   domain-local-await)
+ (preprocess
+  (pps
+   ppx_optcomp
+   ))
+ )

src/util/parallel/gobMutex.ml

@@ -0,0 +1,62 @@
+[%%if ocaml_version >= (5, 0, 0)]
+(* Simple Mutex Implementation using Domain-Local Await (https://github.com/ocaml-multicore/domain-local-await)
+   Copyright © 2023 Vesa Karvonen
+
+   Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted,
+   provided that the above copyright notice and this permission notice appear in all copies.
+
+   THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES
+   OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY
+   DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION,
+   ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. *)
+
+type state =
+  | Unlocked
+  | Locked of (unit -> unit) list
+
+type t = state Atomic.t
+
+let create () = Atomic.make Unlocked
+
+let unlock t =
+  match Atomic.exchange t Unlocked with
+  | Unlocked -> invalid_arg "mutex: already unlocked"
+  | Locked awaiters -> List.iter ((|>) ()) awaiters
+
+let rec lock t =
+  match Atomic.get t with
+  | Unlocked ->
+    if not (Atomic.compare_and_set t Unlocked (Locked [])) then
+      lock t
+  | Locked awaiters as before ->
+    let dla = Domain_local_await.prepare_for_await () in
+    let after = Locked (dla.release :: awaiters) in
+    if Atomic.compare_and_set t before after then
+      match dla.await () with
+      | () -> lock t
+      | exception cancellation_exn ->
+        let rec cleanup () =
+          match Atomic.get t with
+          | Unlocked -> ()
+          | Locked awaiters as before ->
+            if List.for_all ((==) dla.release) awaiters then
+              let after =
+                Locked (List.filter ((!=) dla.release) awaiters)
+              in
+              if not (Atomic.compare_and_set t before after) then
+                cleanup ()
+        in
+        cleanup ();
+        raise cancellation_exn
+    else
+      lock t
+
+[%%else]
+
+type state = NoOp
+
+let create () = NoOp 
+let unlock _ = ()
+let lock _ = ()
+
+[%%endif]

src/util/tracing/dune

@@ -4,6 +4,7 @@
  (name goblint_tracing)
  (public_name goblint.tracing)
  (libraries
+   goblint_parallel
    goblint_std
    goblint_logs
    goblint-cil

src/util/tracing/goblint_tracing.ml

@@ -5,6 +5,7 @@
  * even when the subsystem is not activated. *)
 
 open Goblint_std
+open Goblint_parallel
 open GoblintCil
 open Pretty
 
@@ -38,9 +39,13 @@ let traceTag (sys : string) : Pretty.doc =
   let rec ind (i : int) : string = if (i <= 0) then "" else " " ^ (ind (i-1)) in
   (text ((ind !indent_level) ^ "%%% " ^ sys ^ ": "))
 
+let trace_mutex = GobMutex.create ()
+
 let printtrace sys d: unit =
+  GobMutex.lock trace_mutex;
   fprint stderr ~width:max_int ((traceTag sys) ++ d ++ line);
-  flush stderr
+  flush stderr;
+  GobMutex.unlock trace_mutex
 
 let gtrace always f sys var ?loc do_subsys fmt =
   let cond =