Introduce backwards compatible infrastructure for parallelism

.github/workflows/locked.yml

@@ -105,55 +105,3 @@ jobs:
 
       - name: Test extraction
         run: opam exec -- dune runtest tests/extraction
-
-
-  gobview:
-    strategy:
-      fail-fast: false
-      matrix:
-        os:
-          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
-        ocaml-compiler:
-          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
-          # don't add any other because they won't be used
-        node-version:
-          - 14
-
-    runs-on: ${{ matrix.os }}
-
-    steps:
-      - name: Checkout code
-        uses: actions/checkout@v4
-
-      - name: Set up OCaml ${{ matrix.ocaml-compiler }}
-        env:
-          # otherwise setup-ocaml pins non-locked dependencies
-          # https://github.com/ocaml/setup-ocaml/issues/166
-          OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v3
-        with:
-          ocaml-compiler: ${{ matrix.ocaml-compiler }}
-
-      - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v4
-        with:
-          node-version: ${{ matrix.node-version }}
-
-      - name: Install dependencies
-        run: opam install . --deps-only --locked
-
-      - name: Setup Gobview
-        run: ./make.sh setup_gobview
-
-      - name: Build
-        run: ./make.sh nat
-
-      - name: Build Gobview
-        run: ./make.sh view
-
-      - name: Install selenium
-        run: pip3 install selenium webdriver-manager
-
-      - name: Test Gobview
-        run: |
-          python3 scripts/test-gobview.py

.github/workflows/unlocked.yml

@@ -251,3 +251,49 @@ jobs:
 
       - name: Test incremental regression with cfg comparison
         run: ruby scripts/update_suite.rb -c
+
+  gobview:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
+        ocaml-compiler:
+          - ocaml-variants.5.0.0+options,ocaml-option-flambda 
+        node-version:
+          - 14
+
+    runs-on: ${{ matrix.os }}
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v4
+
+      - name: Set up OCaml ${{ matrix.ocaml-compiler }}
+        uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+
+      - name: Set up Node.js ${{ matrix.node-version }}
+        uses: actions/setup-node@v4
+        with:
+          node-version: ${{ matrix.node-version }}
+
+      - name: Install dependencies
+        run: opam install . --deps-only
+
+      - name: Setup Gobview
+        run: ./make.sh setup_gobview
+
+      - name: Build
+        run: ./make.sh nat
+
+      - name: Build Gobview
+        run: ./make.sh view
+
+      - name: Install selenium
+        run: pip3 install selenium webdriver-manager
+
+      - name: Test Gobview
+        run: |
+          python3 scripts/test-gobview.py

docs/user-guide/inspecting.md

@@ -11,6 +11,8 @@ Modern browsers' security settings forbid some file access which is necessary fo
 
 ## GobView
 
+**Note:** GobView is not compatible with OCaml 4 any more. Use OCaml 5.0.0 or newer.
+
 For the initial setup:
 
 1. Install Node.js (preferably ≥ 12.0.0) and npm (≥ 5.2.0)

dune-project

@@ -67,6 +67,8 @@ 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
+    domain-shims
   )
   (depopts
     (apron (>= v0.9.15))

goblint.opam

@@ -67,6 +67,8 @@ depends: [
   "conf-ruby" {with-test}
   "benchmark" {with-test}
   "conf-gcc"
+  "domain-local-await"
+  "domain_shims"
 ]
 depopts: [
   "apron" {>= "v0.9.15"}

goblint.opam.locked

@@ -54,6 +54,8 @@ depends: [
   "csexp" {= "1.5.2"}
   "cstruct" {= "6.2.0"}
   "ctypes" {= "0.22.0"}
+  "domain-local-await" {= "1.0.1"}
+  "domain_shims" {= "0.1.0"}
   "dune" {= "3.16.0"}
   "dune-build-info" {= "3.16.0"}
   "dune-configurator" {= "3.16.0"}

src/cdomain/value/cdomains/mutexAttrDomain.ml

@@ -1,4 +1,5 @@
 (** Mutex attribute type domain. *)
+open Goblint_parallel
 
 module MutexKind =
 struct
@@ -21,7 +22,7 @@ end
 include Lattice.FlatConf (struct include Printable.DefaultConf let bot_name = "Uninitialized" let top_name = "Top" end) (MutexKind)
 
 (* Needed because OS X is weird and assigns different constants than normal systems... :( *)
-let recursive_int = lazy (
+let recursive_int = DomainsafeLazy.from_fun (fun () ->
   let res = ref (Z.of_int 2) in (* Use OS X as the default, it doesn't have the enum *)
   GoblintCil.iterGlobals !Cilfacade.current_file (function
       | GEnumTag (einfo, _) ->
@@ -39,7 +40,7 @@ let of_int z =
   if Z.equal z Z.zero then
     `Lifted MutexKind.NonRec
   else
-    let recursive_int = Lazy.force recursive_int in
+    let recursive_int = DomainsafeLazy.force recursive_int in
     if Z.equal z recursive_int then
       `Lifted MutexKind.Recursive
     else

src/cdomain/value/dune

@@ -13,6 +13,7 @@
    goblint_library
    goblint_domain
    goblint_incremental
+   goblint_parallel
    goblint-cil)
  (flags :standard -open Goblint_std -open Goblint_logs)
  (preprocess

src/common/util/messages.ml

@@ -8,6 +8,8 @@ module Category = MessageCategory
 
 open GobResult.Syntax
 
+module Format = BatFormat
+
 
 module Severity =
 struct
@@ -195,10 +197,14 @@ let print ?(ppf= !formatter) (m: Message.t) =
     | Debug -> "white" (* non-bright white is actually some gray *)
     | Success -> "green"
   in
-  let pp_prefix = Format.dprintf "@{<%s>[%a]%a@}" severity_stag Severity.pp m.severity Tags.pp m.tags in
+  let pp_print_option ?(none = fun _ () -> ()) pp_v ppf = function
+    | None -> none ppf ()
+    | Some v -> pp_v ppf v
+  in
+  let pp_prefix = (fun ppf -> Format.fprintf ppf "@{<%s>[%a]%a@}" severity_stag Severity.pp m.severity Tags.pp m.tags) in
   let pp_loc ppf = Format.fprintf ppf " @{<violet>(%a)@}" CilType.Location.pp in
   let pp_loc ppf loc =
-    Format.fprintf ppf "%a" (Format.pp_print_option pp_loc) (Option.map Location.to_cil loc)
+    Format.fprintf ppf "%a" (pp_print_option pp_loc) (Option.map Location.to_cil loc)
   in
   let pp_piece ppf piece =
     Format.fprintf ppf "@{<%s>%s@}%a" severity_stag (Piece.text_with_context piece) pp_loc piece.loc
@@ -229,7 +235,7 @@ let print ?(ppf= !formatter) (m: Message.t) =
   let pp_quote ppf loc =
     if get_bool "warn.quote-code" then (
       let pp_cut_quote ppf = Format.fprintf ppf "@,@[<v 0>%a@,@]" pp_quote in
-      (Format.pp_print_option pp_cut_quote) ppf (Option.map Location.to_cil loc)
+      (pp_print_option pp_cut_quote) ppf (Option.map Location.to_cil loc)
     )
   in
   let pp_piece ppf piece = Format.fprintf ppf "%a%a" pp_piece piece pp_quote piece.loc in

src/config/options.schema.json

@@ -2550,6 +2550,12 @@
               "description": "Check TD3 data structure invariants",
               "type": "boolean",
               "default": false
+            },
+            "parallel_domains" :{
+              "title": "solvers.td3.parallel_domains",
+              "description": "Maximal number of Domains that the solver can use in parallel. Only applies, when a solver of the 'td_parallel_*' family is used. If left at -1, the value of jobs will be used.",
+              "type": "integer",
+              "default": -1
             }
           },
           "additionalProperties": false

src/dune

@@ -7,7 +7,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (modules :standard \ goblint privPrecCompare apronPrecCompare messagesCompare)
-  (libraries goblint.sites goblint.build-info goblint-cil goblint-cil.pta goblint-cil.syntacticsearch batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs
+  (libraries goblint.sites goblint.build-info goblint-cil goblint-cil.pta goblint-cil.syntacticsearch batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs domain_shims
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
     ; See: https://dune.readthedocs.io/en/stable/reference/library-dependencies.html#alternative-dependencies

src/goblint_lib.ml

@@ -465,6 +465,17 @@ module PrivPrecCompareUtil = PrivPrecCompareUtil
 module RelationPrecCompareUtil = RelationPrecCompareUtil
 module ApronPrecCompareUtil = ApronPrecCompareUtil
 
+(** {2 Solver parallelism}
+
+    These modules provide utilities required for parallelizing the solver,
+    as well as backwards compatibility with OCaml 4 for the non-parallelized solvers.
+*)
+module DomainsafeLazy = DomainsafeLazy
+module Threadpool = Threadpool
+module GobMutex = GobMutex
+
+(** {2 Debugging} *)
+
 (** {1 Library extensions}
 
     OCaml library extensions which are completely independent of Goblint.

src/lifters/wideningTokenLifter.ml

@@ -12,13 +12,13 @@ module Token = WideningToken
 module TS = SetDomain.ToppedSet (Token) (struct let topname = "Top" end)
 
 (** Reference to current {!add} implementation. Maintained by {!Lifter}. *)
-let add_ref: (Token.t -> unit) ref = ref (fun _ ->
+let add_ref: (Token.t -> unit) Domain.DLS.key = Domain.DLS.new_key (fun () _ ->
     if GobConfig.get_bool "ana.widen.tokens" then
       failwith "Unhandled widening token"
   )
 
 (** Add widening token to local state. *)
-let add t = !add_ref t
+let add t = (Domain.DLS.get add_ref) t
 
 
 (** Widening tokens added to side effects.
@@ -137,16 +137,16 @@ struct
 
   let lift_fun man f g h =
     let new_tokens = ref (snd man.local) in (* New tokens not yet used during this transfer function, such that it is deterministic. *)
-    let old_add = !add_ref in
+    let old_add = Domain.DLS.get add_ref in
     let old_local_tokens = !local_tokens in
-    add_ref := (fun t -> new_tokens := TS.add t !new_tokens);
+    Domain.DLS.set add_ref (fun t -> new_tokens := TS.add t !new_tokens);
     local_tokens := snd man.local;
     let d =
       Fun.protect (fun () ->
           h (g (conv man))
         ) ~finally:(fun () ->
           local_tokens := old_local_tokens;
-          add_ref := old_add
+          Domain.DLS.set add_ref old_add
         )
     in
     (* If transfer function exits via exception, then new tokens are forgotten.

src/solver/dune

@@ -6,6 +6,7 @@
  (libraries
    batteries.unthreaded
    goblint_std
+   goblint_parallel
    goblint_logs
    goblint_common
    goblint_config

src/util/parallel/domainsafeLazy.ml

@@ -0,0 +1,9 @@
+type 'a t = GobMutex.t * ('a Stdlib.Lazy.t)
+
+let from_fun f = (GobMutex.create (), Stdlib.Lazy.from_fun f)
+
+let force (mtx, blk) = 
+  GobMutex.lock mtx; 
+  let value = Stdlib.Lazy.force blk in
+  GobMutex.unlock mtx;
+  value

src/util/parallel/domainsafeLazy.mli

@@ -0,0 +1,6 @@
+(** Lazy type which protects against concurrent calls of 'force'. *)
+
+type 'a t
+
+val from_fun: (unit -> 'a) -> 'a t
+val force: 'a t -> 'a

src/util/parallel/dune

@@ -0,0 +1,18 @@
+(include_subdirs no)
+
+(library
+ (name goblint_parallel)
+ (public_name goblint.parallel)
+ (libraries
+   batteries
+   (select gobMutex.ml from
+      (domainslib -> gobMutex.domainslib.ml)
+      ( -> gobMutex.no-domainslib.ml)
+   )
+   (select threadpool.ml from 
+      (domainslib -> threadpool.domainslib.ml)
+      (-> threadpool.no-domainslib.ml)
+      )
+   domain_shims
+   domain-local-await)
+ )

src/util/parallel/gobMutex.domainslib.ml

@@ -0,0 +1,51 @@
+(* 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

src/util/parallel/gobMutex.no-domainslib.ml

@@ -0,0 +1,6 @@
+type state = NoOp
+type t = state
+
+let create () = NoOp 
+let unlock _ = ()
+let lock _ = ()