Merge pull request #1708 from arkocal/parallelism_backwards_compat_1

Introduce backwards compatible infrastructure for parallelism

Author: arkocal

.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,9 +67,12 @@ 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))
+    domainslib
     z3
   )
   (conflicts

goblint.opam

@@ -67,10 +67,13 @@ depends: [
   "conf-ruby" {with-test}
   "benchmark" {with-test}
   "conf-gcc"
+  "domain-local-await"
+  "domain_shims"
 ]
 depopts: [
   "apron" {>= "v0.9.15"}
   "z3"
+  "domainslib"
 ]
 conflicts: [
   "result" {< "1.5"}

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"}

scripts/goblint-lib-modules.py

@@ -42,6 +42,13 @@
     "Goblint_build_info",
     "Dune_build_info",
 
+    # mocked parallelism: These files are called differently
+    # (x.domainslib.ml or x.no-domainslib.ml) and therefore not recognized
+    # by the script
+    "GobMutex",
+    "Threadpool",
+    "DomainsafeLazy",
+
     # ppx-s
     "Ppx_deriving_printable",
     "Ppx_deriving_lattice",

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/config/options.schema.json

@@ -2640,6 +2640,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