diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
index 16655bfdc7..2501577a14 100644
--- a/.github/workflows/locked.yml
+++ b/.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
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
index f3fe6cc558..2f8fb67af3 100644
--- a/.github/workflows/unlocked.yml
+++ b/.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
diff --git a/docs/user-guide/inspecting.md b/docs/user-guide/inspecting.md
index 6ea08db1f4..0aea8fd9e0 100644
--- a/docs/user-guide/inspecting.md
+++ b/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)
diff --git a/dune-project b/dune-project
index c4a627e95f..60fda293a0 100644
--- a/dune-project
+++ b/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
diff --git a/goblint.opam b/goblint.opam
index 92f3fa67e4..237c588662 100644
--- a/goblint.opam
+++ b/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"}
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 0980257070..d3ed6ccfbe 100644
--- a/goblint.opam.locked
+++ b/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"}
diff --git a/scripts/goblint-lib-modules.py b/scripts/goblint-lib-modules.py
index 0e0a0613a7..b3cd229841 100755
--- a/scripts/goblint-lib-modules.py
+++ b/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",
diff --git a/src/cdomain/value/cdomains/mutexAttrDomain.ml b/src/cdomain/value/cdomains/mutexAttrDomain.ml
index e12818c2c1..3cb1c325ae 100644
--- a/src/cdomain/value/cdomains/mutexAttrDomain.ml
+++ b/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
diff --git a/src/cdomain/value/dune b/src/cdomain/value/dune
index 7e5f727699..22dbff2316 100644
--- a/src/cdomain/value/dune
+++ b/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
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index d8a72fe24d..4421a916cb 100644
--- a/src/config/options.schema.json
+++ b/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
diff --git a/src/dune b/src/dune
index f114a14db7..615a16c067 100644
--- a/src/dune
+++ b/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
diff --git a/src/lifters/wideningTokenLifter.ml b/src/lifters/wideningTokenLifter.ml
index 0ba069328a..0001fb2796 100644
--- a/src/lifters/wideningTokenLifter.ml
+++ b/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.
diff --git a/src/solver/dune b/src/solver/dune
index 577c75c9de..0781815427 100644
--- a/src/solver/dune
+++ b/src/solver/dune
@@ -6,6 +6,7 @@
  (libraries
    batteries.unthreaded
    goblint_std
+   goblint_parallel
    goblint_logs
    goblint_common
    goblint_config
diff --git a/src/util/parallel/domainsafeLazy.ml b/src/util/parallel/domainsafeLazy.ml
new file mode 100644
index 0000000000..ea1f271fac
--- /dev/null
+++ b/src/util/parallel/domainsafeLazy.ml
@@ -0,0 +1,65 @@
+(* 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 'a state =
+  | Fun of (unit -> 'a)
+  | Run of (unit -> unit) list
+  | Val of 'a
+  | Exn of exn
+
+type 'a t = 'a state Atomic.t
+
+let from_fun th = Atomic.make (Fun th)
+(* val from_fun : (unit -> 'a) -> 'a state Atomic.t = <fun> *)
+
+let from_val v = Atomic.make (Val v)
+(* val from_val : 'a -> 'a state Atomic.t = <fun> *)
+
+let rec force t =
+  match Atomic.get t with
+  | Val v -> v
+  | Exn e -> raise e
+  | Fun th as before ->
+    if Atomic.compare_and_set t before (Run []) then
+      let result =
+        match th () with
+        | v -> Val v
+        | exception e -> Exn e
+      in
+      match Atomic.exchange t result with
+      | (Val _ | Exn _ | Fun _) ->
+        failwith "impossible"
+      | Run waiters ->
+        List.iter ((|>) ()) waiters;
+        force t
+    else
+      force t
+  | Run waiters as before ->
+    let dla = Domain_local_await.prepare_for_await () in
+    let after = Run (dla.release :: waiters) in
+    if Atomic.compare_and_set t before after then
+      match dla.await () with
+      | () ->
+        force t
+      | exception cancelation_exn ->
+        let rec cleanup () =
+          match Atomic.get t with
+          | (Val _ | Exn _ | Fun _) ->
+            ()
+          | Run waiters as before ->
+            let after = Run (List.filter ((!=) dla.release) waiters) in
+            if not (Atomic.compare_and_set t before after) then
+              cleanup ()
+        in
+        cleanup ();
+        raise cancelation_exn
+    else
+      force t
diff --git a/src/util/parallel/domainsafeLazy.mli b/src/util/parallel/domainsafeLazy.mli
new file mode 100644
index 0000000000..40fcb176a2
--- /dev/null
+++ b/src/util/parallel/domainsafeLazy.mli
@@ -0,0 +1,7 @@
+(** Lazy type which protects against concurrent calls of {!force}. *)
+
+type 'a t
+
+val from_fun: (unit -> 'a) -> 'a t
+val from_val: 'a -> 'a t
+val force: 'a t -> 'a
diff --git a/src/util/parallel/dune b/src/util/parallel/dune
new file mode 100644
index 0000000000..47dab8a752
--- /dev/null
+++ b/src/util/parallel/dune
@@ -0,0 +1,18 @@
+(include_subdirs no)
+
+(library
+ (name goblint_parallel)
+ (public_name goblint.parallel)
+ (modules gobMutex threadpool domainsafeLazy)
+ (libraries
+   (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)
+ )
diff --git a/src/util/parallel/gobMutex.domainslib.ml b/src/util/parallel/gobMutex.domainslib.ml
new file mode 100644
index 0000000000..fb2e74a020
--- /dev/null
+++ b/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
diff --git a/src/util/parallel/gobMutex.mli b/src/util/parallel/gobMutex.mli
new file mode 100644
index 0000000000..996eff662a
--- /dev/null
+++ b/src/util/parallel/gobMutex.mli
@@ -0,0 +1,9 @@
+(** A mutex that supports multiple threads on a domain when parallelism is supported
+    as detected by the presence of the [domainslib] library. It is mocked to a no-op
+    when [domainslib] is not available for backwards compatibility. *)
+
+type t
+
+val create: unit -> t
+val unlock: t -> unit
+val lock: t -> unit
diff --git a/src/util/parallel/gobMutex.no-domainslib.ml b/src/util/parallel/gobMutex.no-domainslib.ml
new file mode 100644
index 0000000000..d5249c6476
--- /dev/null
+++ b/src/util/parallel/gobMutex.no-domainslib.ml
@@ -0,0 +1,6 @@
+type state = NoOp
+type t = state
+
+let create () = NoOp 
+let unlock _ = ()
+let lock _ = ()
diff --git a/src/util/parallel/threadpool.domainslib.ml b/src/util/parallel/threadpool.domainslib.ml
new file mode 100644
index 0000000000..156994937c
--- /dev/null
+++ b/src/util/parallel/threadpool.domainslib.ml
@@ -0,0 +1,15 @@
+module T = Domainslib.Task
+
+type t = T.pool
+type 'a promise = 'a T.promise
+
+let run = T.run
+
+let create n = T.setup_pool ~num_domains:n ()
+
+let add_work pool f = T.async pool f 
+
+let await_all pool promises = 
+  List.iter (T.await pool) promises
+
+let finished_with pool = T.teardown_pool pool
diff --git a/src/util/parallel/threadpool.mli b/src/util/parallel/threadpool.mli
new file mode 100644
index 0000000000..300c93aa92
--- /dev/null
+++ b/src/util/parallel/threadpool.mli
@@ -0,0 +1,9 @@
+type t
+type 'a promise
+
+val create : int -> t
+val run : t -> (unit -> 'a) -> 'a
+val add_work : t -> (unit -> 'a) -> 'a promise
+val await_all : t -> unit promise list -> unit
+val finished_with : t -> unit
+
diff --git a/src/util/parallel/threadpool.no-domainslib.ml b/src/util/parallel/threadpool.no-domainslib.ml
new file mode 100644
index 0000000000..abd7df4aa4
--- /dev/null
+++ b/src/util/parallel/threadpool.no-domainslib.ml
@@ -0,0 +1,12 @@
+type t = unit
+type 'a promise = 'a
+
+let run pool f = f ()
+
+let create n = ()
+
+let add_work pool f = f ()
+
+let await_all pool promises = ()
+
+let finished_with pool = ()
diff --git a/src/util/timing/dune b/src/util/timing/dune
index 1a90c9bc12..3eb5c58cfa 100644
--- a/src/util/timing/dune
+++ b/src/util/timing/dune
@@ -3,4 +3,4 @@
 (library
  (name goblint_timing)
  (public_name goblint.timing)
- (libraries catapult catapult-file))
+ (libraries catapult catapult-file domain_shims))
diff --git a/src/util/timing/goblint_timing.ml b/src/util/timing/goblint_timing.ml
index a65ce0ecf4..4d04d4853f 100644
--- a/src/util/timing/goblint_timing.ml
+++ b/src/util/timing/goblint_timing.ml
@@ -63,7 +63,14 @@ struct
     }
 
   (** Stack of currently active timing frames. *)
-  let current: frame Stack.t = Stack.create ()
+  let current: frame Stack.t Domain.DLS.key = Domain.DLS.new_key 
+      (fun () -> Stack.create ())
+      (* A root frame must be created for new threads, as each thread has its own stack *)
+      ~split_from_parent: (fun _ -> begin
+            let (stack : frame Stack.t) = Stack.create () in 
+            Stack.push (create_frame root) stack;
+            stack
+          end)
 
   let reset () =
     (* Reset tree. *)
@@ -73,9 +80,9 @@ struct
     root.count <- 0;
     root.children <- [];
     (* Reset frames. *)
-    if not (Stack.is_empty current) then ( (* If ever started. In case reset before first start. *)
-      Stack.clear current;
-      Stack.push (create_frame root) current
+    if not (Stack.is_empty (Domain.DLS.get current)) then ( (* If ever started. In case reset before first start. *)
+      Stack.clear (Domain.DLS.get current);
+      Stack.push (create_frame root) (Domain.DLS.get current)
     )
 
   let start options' =
@@ -87,8 +94,8 @@ struct
       Catapult.Tracing.emit ~pid:tef_pid "process_name" ~args:[("name", `String Name.name)] Catapult.Event_type.M
     );
     enabled := true;
-    if Stack.is_empty current then (* If never started. *)
-      Stack.push (create_frame root) current
+    if Stack.is_empty (Domain.DLS.get current) then (* If never started. *)
+      Stack.push (create_frame root) (Domain.DLS.get current)
 
   let stop () =
     enabled := false
@@ -96,7 +103,7 @@ struct
   let enter ?args name =
     (* Find the right tree. *)
     let tree: tree =
-      let {tree; _} = Stack.top current in
+      let {tree; _} = Stack.top (Domain.DLS.get current) in
       let rec loop = function
         | child :: _ when child.name = name -> child
         | _ :: children' -> loop children'
@@ -108,7 +115,7 @@ struct
       in
       loop tree.children
     in
-    Stack.push (create_frame tree) current;
+    Stack.push (create_frame tree) (Domain.DLS.get current);
     if !options.tef then
       Catapult.Tracing.begin' ~pid:tef_pid ?args name
 
@@ -130,7 +137,7 @@ struct
       tree.count <- tree.count + 1
 
   let exit name =
-    let {tree; _} as frame = Stack.pop current in
+    let {tree; _} as frame = Stack.pop (Domain.DLS.get current) in
     assert (tree.name = name);
     add_frame_to_tree frame tree;
     if !options.tef then
@@ -177,7 +184,7 @@ struct
         tree (* no need to recurse, current doesn't go into subtree *)
     in
     (* Folding the stack also reverses it such that the root frame is at the beginning. *)
-    let current_rev = Stack.fold (fun acc frame -> frame :: acc) [] current in
+    let current_rev = Stack.fold (fun acc frame -> frame :: acc) [] (Domain.DLS.get current) in
     tree_with_current current_rev root
 
   let rec pp_tree ppf node =
diff --git a/src/util/tracing/dune b/src/util/tracing/dune
index 452d226eec..0bb38f42d1 100644
--- a/src/util/tracing/dune
+++ b/src/util/tracing/dune
@@ -4,6 +4,7 @@
  (name goblint_tracing)
  (public_name goblint.tracing)
  (libraries
+   goblint_parallel
    goblint_std
    goblint_logs
    goblint-cil
diff --git a/src/util/tracing/goblint_tracing.ml b/src/util/tracing/goblint_tracing.ml
index 122ebeb325..f62ec3ee38 100644
--- a/src/util/tracing/goblint_tracing.ml
+++ b/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 =