From 4f611d54355d96f3a07178e3c9b1cb515c1369a6 Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Thu, 15 Jan 2026 13:07:25 +0100
Subject: [PATCH 01/24] mustlock history analysis

---
 src/analyses/mustlockHistory.ml | 38 +++++++++++++++++++++++++++++++++
 src/domains/queries.ml          |  7 ++++++
 src/goblint_lib.ml              |  1 +
 3 files changed, 46 insertions(+)
 create mode 100644 src/analyses/mustlockHistory.ml

diff --git a/src/analyses/mustlockHistory.ml b/src/analyses/mustlockHistory.ml
new file mode 100644
index 0000000000..d9747ea7cb
--- /dev/null
+++ b/src/analyses/mustlockHistory.ml
@@ -0,0 +1,38 @@
+open Analyses
+module TIDs = SetDomain.Reverse (ConcDomain.ThreadSet)
+module Lock = LockDomain.MustLock
+
+module Spec = struct
+  include IdentityUnitContextsSpec
+  module D = Queries.LH
+
+  let name () = "mustlockHistory"
+  let startstate _ = D.empty ()
+  let exitstate _ = D.empty ()
+
+  let lock man tid lock =
+    let old_threadset = D.find lock man.local in
+    let new_threadset = TIDs.add tid old_threadset in
+    D.add lock new_threadset man.local
+
+  let event man e _ =
+    match e with
+    (* we only handle exclusive locks here *)
+    | Events.Lock (addr, true) ->
+      let tid_lifted = man.ask Queries.CurrentThreadId in
+      let lock_opt = Lock.of_addr addr in
+      (match tid_lifted, lock_opt with
+       | `Lifted tid, Some l -> lock man tid l
+       | _ -> man.local)
+    | _ -> man.local
+
+  let query man (type a) (x : a Queries.t) : a Queries.result =
+    match x with
+    | Queries.MustlockHistory -> (man.local : D.t)
+    | _ -> Queries.Result.top x
+end
+
+let _ =
+  MCP.register_analysis
+    ~dep:[ "threadid"; "threadJoins"; "threadDescendants" ]
+    (module Spec : MCPSpec)
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 6b85a2729c..3c36966686 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -77,6 +77,8 @@ type invariant_context = Invariant.context = {
 
 module YS = SetDomain.ToppedSet (YamlWitnessType.Entry) (struct let topname = "Top" end)
 
+module LH = MapDomain.MapTop (LockDomain.MustLock) (SetDomain.Reverse (ConcDomain.ThreadSet))
+
 
 (** GADT for queries with specific result type. *)
 type _ t =
@@ -147,6 +149,7 @@ type _ t =
   | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t
   | InvariantGlobalNodes: NS.t t (** Nodes where YAML witness flow-insensitive invariants should be emitted as location invariants (if [witness.invariant.flow_insensitive-as] is configured to do so). *) (* [Spec.V.t] argument (as [Obj.t]) could be added, if this should be different for different flow-insensitive invariants. *)
   | DescendantThreads: ThreadIdDomain.Thread.t -> ConcDomain.ThreadSet.t t
+  | MustlockHistory: LH.t t
 
 type 'a result = 'a
 
@@ -223,6 +226,7 @@ struct
     | GhostVarAvailable _ -> (module MayBool)
     | InvariantGlobalNodes -> (module NS)
     | DescendantThreads _ -> (module ConcDomain.ThreadSet)
+    | MustlockHistory -> (module LH)
 
   (** Get bottom result for query. *)
   let bot (type a) (q: a t): a result =
@@ -298,6 +302,7 @@ struct
     | GhostVarAvailable _ -> MayBool.top ()
     | InvariantGlobalNodes -> NS.top ()
     | DescendantThreads _ -> ConcDomain.ThreadSet.top ()
+    | MustlockHistory -> LH.top ()
 end
 
 (* The type any_query can't be directly defined in Any as t,
@@ -370,6 +375,7 @@ struct
     | Any (GhostVarAvailable _) -> 62
     | Any InvariantGlobalNodes -> 63
     | Any (DescendantThreads _) -> 64
+    | Any (MustlockHistory) -> 65
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -547,6 +553,7 @@ struct
     | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v
     | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes"
     | Any (DescendantThreads t) -> Pretty.dprintf "DescendantThreads %a" ThreadIdDomain.Thread.pretty t
+    | Any (MustlockHistory) -> Pretty.dprintf "MustlockHistory"
 end
 
 let to_value_domain_ask (ask: ask) =
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 92fa69c3b4..9047224735 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -109,6 +109,7 @@ module MayLocks = MayLocks
 module SymbLocks = SymbLocks
 module Deadlock = Deadlock
 module MutexGhosts = MutexGhosts
+module MustlockHistory = MustlockHistory
 
 (** {3 Threads}
 

From d4189b440f7f16d3a586adb53f783633538376be Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Thu, 15 Jan 2026 13:08:02 +0100
Subject: [PATCH 02/24] initial version of descendant lockset analysis

---
 src/analyses/descendantLockset.ml | 115 ++++++++++++++++++++++++++++++
 src/goblint_lib.ml                |   1 +
 2 files changed, 116 insertions(+)
 create mode 100644 src/analyses/descendantLockset.ml

diff --git a/src/analyses/descendantLockset.ml b/src/analyses/descendantLockset.ml
new file mode 100644
index 0000000000..f6db475ce9
--- /dev/null
+++ b/src/analyses/descendantLockset.ml
@@ -0,0 +1,115 @@
+open Analyses
+module TID = ThreadIdDomain.Thread
+module TIDs = ConcDomain.ThreadSet
+module Lockset = LockDomain.MustLockset
+
+module Spec = struct
+  include IdentityUnitContextsSpec
+  module D = MapDomain.MapBot (TID) (Lockset)
+
+  let name () = "descendantLockset"
+  let startstate _ = D.empty ()
+  let exitstate _ = D.empty ()
+
+  (** reflexive-transitive closure of child relation applied to [tid] and
+      filtered to only include threads, where [tid] is a must-ancestor
+      @param man any man
+      @param tid *)
+  let must_ancestor_descendants_closure man tid =
+    let descendants = man.ask @@ Queries.DescendantThreads tid in
+    let must_ancestors_descendants = TIDs.filter (TID.must_be_ancestor tid) descendants in
+    TIDs.add tid must_ancestors_descendants
+
+  let threadspawn man ~multiple lval f args fman =
+    let tid_lifted = man.ask Queries.CurrentThreadId in
+    let child_tid_lifted = fman.ask Queries.CurrentThreadId in
+    match tid_lifted, child_tid_lifted with
+    | `Lifted tid, `Lifted child_tid when TID.must_be_ancestor tid child_tid ->
+      let must_ancestor_descendants = must_ancestor_descendants_closure fman child_tid in
+      let lockset = man.ask Queries.MustLockset in
+      TIDs.fold
+        (fun t_d -> D.join (D.singleton t_d lockset))
+        must_ancestor_descendants
+        man.local
+    | _ -> man.local
+
+  let get_must_ancestor_running_descendants man tid =
+    let may_created_tids = man.ask Queries.CreatedThreads in
+    let may_must_ancestor_created_tids =
+      TIDs.filter (TID.must_be_ancestor tid) may_created_tids
+    in
+    let may_transitively_created_tids =
+      TIDs.fold
+        (fun child_tid acc ->
+           TIDs.union acc (must_ancestor_descendants_closure man child_tid))
+        may_must_ancestor_created_tids
+        (TIDs.empty ())
+    in
+    let must_joined_tids = man.ask Queries.MustJoinedThreads in
+    TIDs.diff may_transitively_created_tids must_joined_tids
+
+  let unlock man tid possibly_running_tids lock =
+    TIDs.fold
+      (fun tid ->
+         let old_value = D.find tid man.local in
+         let new_value = Lockset.remove lock old_value in
+         D.add tid new_value)
+      possibly_running_tids
+      (D.empty ())
+
+  let unknown_unlock man tid possibly_running_tids =
+    TIDs.fold (fun tid -> D.add tid (Lockset.empty ())) possibly_running_tids (D.empty ())
+
+  let event man e _ =
+    match e with
+    | Events.Unlock addr ->
+      let tid_lifted = man.ask Queries.CurrentThreadId in
+      (match tid_lifted with
+       | `Lifted tid ->
+         let possibly_running_tids = get_must_ancestor_running_descendants man tid in
+         let lock_opt = LockDomain.MustLock.of_addr addr in
+         (match lock_opt with
+          | Some lock -> unlock man tid possibly_running_tids lock
+          | None -> unknown_unlock man tid possibly_running_tids)
+       | _ -> man.local)
+    | _ -> man.local
+
+  module A = struct
+    (** ego tid * lock history * descendant lockset *)
+    include Printable.Prod3 (TID) (Queries.LH) (D)
+
+    let happens_before (t1, dl1) (t2, lh2) =
+      let locks_held_creating_t2 = D.find t2 dl1 in
+      if Lockset.is_bot locks_held_creating_t2
+      then false
+      else (
+        let relevant_lh2_threads =
+          Lockset.fold
+            (fun lock -> TIDs.union (Queries.LH.find lock lh2))
+            locks_held_creating_t2
+            (TIDs.empty ())
+        in
+        TIDs.exists
+          (fun t_lh ->
+             TID.must_be_ancestor t1 t_lh
+             && (TID.equal t_lh t2 || TID.must_be_ancestor t_lh t2))
+          relevant_lh2_threads)
+
+    let may_race (t1, lh1, dl1) (t2, lh2, dl2) =
+      not (happens_before (t1, dl1) (t2, lh2) || happens_before (t2, dl2) (t1, lh1))
+
+    let should_print _ = false
+  end
+
+  let access man _ =
+    let lh = man.ask Queries.MustlockHistory in
+    let tid_lifted = man.ask Queries.CurrentThreadId in
+    match tid_lifted with
+    | `Lifted tid -> tid, lh, man.local
+    | _ -> ThreadIdDomain.UnknownThread, Queries.LH.empty (), D.empty ()
+end
+
+let _ =
+  MCP.register_analysis
+    ~dep:[ "threadid"; "mutex"; "threadJoins"; "threadDescendants"; "mustlockHistory" ]
+    (module Spec : MCPSpec)
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 9047224735..ead3965c1e 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -134,6 +134,7 @@ module PthreadBarriers = PthreadBarriers
 module ExtractPthread = ExtractPthread
 module PthreadOnce = PthreadOnce
 module CreationLockset = CreationLockset
+module DescendantLockset = DescendantLockset
 
 (** {2 Longjmp}
 

From 4d5fee2115b0add2046656c72f724ed49e75c2d1 Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Thu, 15 Jan 2026 13:09:53 +0100
Subject: [PATCH 03/24] first descendant lockset racefree tests

---
 .../53-races-mhp/40-dl_simple_racefree.c      | 22 +++++++++++++++
 ...-dl_lock_in_intermediate_thread_racefree.c | 27 +++++++++++++++++++
 .../43-dl_maybe_create_racefree.c             | 25 +++++++++++++++++
 3 files changed, 74 insertions(+)
 create mode 100644 tests/regression/53-races-mhp/40-dl_simple_racefree.c
 create mode 100644 tests/regression/53-races-mhp/41-dl_lock_in_intermediate_thread_racefree.c
 create mode 100644 tests/regression/53-races-mhp/43-dl_maybe_create_racefree.c

diff --git a/tests/regression/53-races-mhp/40-dl_simple_racefree.c b/tests/regression/53-races-mhp/40-dl_simple_racefree.c
new file mode 100644
index 0000000000..73416bf5cb
--- /dev/null
+++ b/tests/regression/53-races-mhp/40-dl_simple_racefree.c
@@ -0,0 +1,22 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex);
+  // everything from here must happen after unlock in main
+  pthread_mutex_unlock(&mutex);
+  global++; // NORACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_mutex_lock(&mutex);
+  pthread_create(&id1, NULL, t1, NULL);
+  global++; // NORACE
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}
diff --git a/tests/regression/53-races-mhp/41-dl_lock_in_intermediate_thread_racefree.c b/tests/regression/53-races-mhp/41-dl_lock_in_intermediate_thread_racefree.c
new file mode 100644
index 0000000000..129fc9249c
--- /dev/null
+++ b/tests/regression/53-races-mhp/41-dl_lock_in_intermediate_thread_racefree.c
@@ -0,0 +1,27 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1, id2;
+
+void *t2(void *arg) {
+  global++; // NORACE
+  return NULL;
+}
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex);
+  // everything from here must happen after unlock in main
+  pthread_create(&id2, NULL, t2, NULL);
+  pthread_mutex_unlock(&mutex);
+  return NULL;
+}
+
+int main(void) {
+  pthread_mutex_lock(&mutex);
+  pthread_create(&id1, NULL, t1, NULL);
+  global++; // NORACE
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}
diff --git a/tests/regression/53-races-mhp/43-dl_maybe_create_racefree.c b/tests/regression/53-races-mhp/43-dl_maybe_create_racefree.c
new file mode 100644
index 0000000000..cb020006a4
--- /dev/null
+++ b/tests/regression/53-races-mhp/43-dl_maybe_create_racefree.c
@@ -0,0 +1,25 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex);
+  // everything from here must happen after unlock in main
+  pthread_mutex_unlock(&mutex);
+  global++; // NORACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_mutex_lock(&mutex);
+  int maybe;
+  if (maybe) {
+    pthread_create(&id1, NULL, t1, NULL);
+  }
+  global++; // NORACE
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}

From 2cc4be9c81fd2e2463b5d4ce7164748d20a098b3 Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Thu, 15 Jan 2026 13:10:34 +0100
Subject: [PATCH 04/24] first descendant lockset racing tests

---
 .../53-races-mhp/50-dl_no_lh_racing.c         | 19 +++++++++++++++
 .../53-races-mhp/51-dl_unlock_parent_racing.c | 20 ++++++++++++++++
 .../53-races-mhp/52-dl_maybe_lh_racing.c      | 24 +++++++++++++++++++
 .../53-dl_maybe_unlock_parent_racing.c        | 23 ++++++++++++++++++
 .../53-races-mhp/54-dl_unknown_lh_racing.c    | 22 +++++++++++++++++
 .../55-dl_unknown_unlock_parent_racing.c      | 21 ++++++++++++++++
 6 files changed, 129 insertions(+)
 create mode 100644 tests/regression/53-races-mhp/50-dl_no_lh_racing.c
 create mode 100644 tests/regression/53-races-mhp/51-dl_unlock_parent_racing.c
 create mode 100644 tests/regression/53-races-mhp/52-dl_maybe_lh_racing.c
 create mode 100644 tests/regression/53-races-mhp/53-dl_maybe_unlock_parent_racing.c
 create mode 100644 tests/regression/53-races-mhp/54-dl_unknown_lh_racing.c
 create mode 100644 tests/regression/53-races-mhp/55-dl_unknown_unlock_parent_racing.c

diff --git a/tests/regression/53-races-mhp/50-dl_no_lh_racing.c b/tests/regression/53-races-mhp/50-dl_no_lh_racing.c
new file mode 100644
index 0000000000..3d34d41c3e
--- /dev/null
+++ b/tests/regression/53-races-mhp/50-dl_no_lh_racing.c
@@ -0,0 +1,19 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1;
+
+void *t1(void *arg) {
+  global++; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_mutex_lock(&mutex);
+  pthread_create(&id1, NULL, t1, NULL);
+  global++; // RACE!
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}
diff --git a/tests/regression/53-races-mhp/51-dl_unlock_parent_racing.c b/tests/regression/53-races-mhp/51-dl_unlock_parent_racing.c
new file mode 100644
index 0000000000..8615b5f2e6
--- /dev/null
+++ b/tests/regression/53-races-mhp/51-dl_unlock_parent_racing.c
@@ -0,0 +1,20 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex);
+  global++; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_mutex_lock(&mutex);
+  pthread_create(&id1, NULL, t1, NULL);
+  pthread_mutex_unlock(&mutex);
+  global++; // RACE!
+  return 0;
+}
diff --git a/tests/regression/53-races-mhp/52-dl_maybe_lh_racing.c b/tests/regression/53-races-mhp/52-dl_maybe_lh_racing.c
new file mode 100644
index 0000000000..c4e9218dc2
--- /dev/null
+++ b/tests/regression/53-races-mhp/52-dl_maybe_lh_racing.c
@@ -0,0 +1,24 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1;
+
+void *t1(void *arg) {
+  int maybe;
+  if (maybe) { 
+    pthread_mutex_lock(&mutex);
+    pthread_mutex_unlock(&mutex);
+  }
+  global++; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_mutex_lock(&mutex);
+  pthread_create(&id1, NULL, t1, NULL);
+  global++; // RACE!
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}
diff --git a/tests/regression/53-races-mhp/53-dl_maybe_unlock_parent_racing.c b/tests/regression/53-races-mhp/53-dl_maybe_unlock_parent_racing.c
new file mode 100644
index 0000000000..1f62562e1f
--- /dev/null
+++ b/tests/regression/53-races-mhp/53-dl_maybe_unlock_parent_racing.c
@@ -0,0 +1,23 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex);
+  global++; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_mutex_lock(&mutex);
+  pthread_create(&id1, NULL, t1, NULL);
+  int maybe;
+  if (maybe) {
+  pthread_mutex_unlock(&mutex);
+  }
+  global++; // RACE!
+  return 0;
+}
diff --git a/tests/regression/53-races-mhp/54-dl_unknown_lh_racing.c b/tests/regression/53-races-mhp/54-dl_unknown_lh_racing.c
new file mode 100644
index 0000000000..dee7f56fec
--- /dev/null
+++ b/tests/regression/53-races-mhp/54-dl_unknown_lh_racing.c
@@ -0,0 +1,22 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1;
+
+void *t1(void *arg) {
+  pthread_mutex_t *mutex_ref;
+  pthread_mutex_lock(mutex_ref); // lock of unknown mutex
+  pthread_mutex_unlock(mutex_ref);
+  global++; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_mutex_lock(&mutex);
+  pthread_create(&id1, NULL, t1, NULL);
+  global++; // RACE!
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}
diff --git a/tests/regression/53-races-mhp/55-dl_unknown_unlock_parent_racing.c b/tests/regression/53-races-mhp/55-dl_unknown_unlock_parent_racing.c
new file mode 100644
index 0000000000..22e0d84a17
--- /dev/null
+++ b/tests/regression/53-races-mhp/55-dl_unknown_unlock_parent_racing.c
@@ -0,0 +1,21 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex);
+  global++; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_mutex_lock(&mutex);
+  pthread_create(&id1, NULL, t1, NULL);
+  pthread_mutex_t *mutex_ref;
+  pthread_mutex_unlock(mutex_ref); // unlock of unknown mutex
+  global++; // RACE!
+  return 0;
+}

From 470279f09ab4fffcd922a49c7ed7122d5307929d Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Sun, 18 Jan 2026 14:36:15 +0100
Subject: [PATCH 05/24] descendant lockset racing tests with multiple thread
 creations

---
 ...56-dl_multiple_creates_sequential_racing.c | 23 ++++++++++++++++
 ...7-dl_multiple_creates_conditional_racing.c | 27 +++++++++++++++++++
 2 files changed, 50 insertions(+)
 create mode 100644 tests/regression/53-races-mhp/56-dl_multiple_creates_sequential_racing.c
 create mode 100644 tests/regression/53-races-mhp/57-dl_multiple_creates_conditional_racing.c

diff --git a/tests/regression/53-races-mhp/56-dl_multiple_creates_sequential_racing.c b/tests/regression/53-races-mhp/56-dl_multiple_creates_sequential_racing.c
new file mode 100644
index 0000000000..0840d5e4ac
--- /dev/null
+++ b/tests/regression/53-races-mhp/56-dl_multiple_creates_sequential_racing.c
@@ -0,0 +1,23 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset --disable ana.thread.include-node
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1, id2, id3;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex);
+  pthread_mutex_unlock(&mutex);
+  global++; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_create(&id1, NULL, t1, NULL);
+  pthread_create(&id2, NULL, t1, NULL);
+  pthread_mutex_lock(&mutex);
+  pthread_create(&id3, NULL, t1, NULL); // t1 can already be created before locking
+  global++; // RACE!
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}
diff --git a/tests/regression/53-races-mhp/57-dl_multiple_creates_conditional_racing.c b/tests/regression/53-races-mhp/57-dl_multiple_creates_conditional_racing.c
new file mode 100644
index 0000000000..2791f8b610
--- /dev/null
+++ b/tests/regression/53-races-mhp/57-dl_multiple_creates_conditional_racing.c
@@ -0,0 +1,27 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset --disable ana.thread.include-node
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1, id2, id3;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex);
+  pthread_mutex_unlock(&mutex);
+  global++; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  int maybe;
+  if (maybe) {
+    pthread_create(&id1, NULL, t1, NULL); // locking happens after thread creation!
+    pthread_mutex_lock(&mutex);
+  } else {
+    pthread_mutex_lock(&mutex);
+    pthread_create(&id2, NULL, t1, NULL);
+  }
+  global++; // RACE!
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}

From 1f883f250295d53c160c97575a3303f0f0cbe379 Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Mon, 19 Jan 2026 10:14:34 +0100
Subject: [PATCH 06/24] creation lockset query

---
 src/analyses/creationLockset.ml |  7 ++++++-
 src/domains/queries.ml          | 11 ++++++++++-
 2 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml
index 118dc2d590..d6289065da 100644
--- a/src/analyses/creationLockset.ml
+++ b/src/analyses/creationLockset.ml
@@ -20,7 +20,7 @@ module Spec = struct
     include StdV
   end
 
-  module G = MapDomain.MapBot (TID) (Lockset)
+  module G = Queries.CL
 
   let name () = "creationLockset"
   let startstate _ = D.bot ()
@@ -148,6 +148,11 @@ module Spec = struct
       let creation_lockset = man.global tid in
       tid, lockset, creation_lockset
     | _ -> ThreadIdDomain.UnknownThread, Lockset.empty (), G.empty ()
+
+  let query man (type a) (x : a Queries.t) : a Queries.result =
+    match x with
+    | Queries.CreationLockset t -> (man.global  t : G.t)
+    | _ -> Queries.Result.top x
 end
 
 let _ =
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 3c36966686..b068e8a09b 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -77,6 +77,8 @@ type invariant_context = Invariant.context = {
 
 module YS = SetDomain.ToppedSet (YamlWitnessType.Entry) (struct let topname = "Top" end)
 
+module CL = MapDomain.MapBot_LiftTop (ThreadIdDomain.Thread) (LockDomain.MustLockset)
+
 module LH = MapDomain.MapTop (LockDomain.MustLock) (SetDomain.Reverse (ConcDomain.ThreadSet))
 
 
@@ -149,6 +151,7 @@ type _ t =
   | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t
   | InvariantGlobalNodes: NS.t t (** Nodes where YAML witness flow-insensitive invariants should be emitted as location invariants (if [witness.invariant.flow_insensitive-as] is configured to do so). *) (* [Spec.V.t] argument (as [Obj.t]) could be added, if this should be different for different flow-insensitive invariants. *)
   | DescendantThreads: ThreadIdDomain.Thread.t -> ConcDomain.ThreadSet.t t
+  | CreationLockset: ThreadIdDomain.Thread.t -> CL.t t
   | MustlockHistory: LH.t t
 
 type 'a result = 'a
@@ -226,6 +229,7 @@ struct
     | GhostVarAvailable _ -> (module MayBool)
     | InvariantGlobalNodes -> (module NS)
     | DescendantThreads _ -> (module ConcDomain.ThreadSet)
+    | CreationLockset _ -> (module CL)
     | MustlockHistory -> (module LH)
 
   (** Get bottom result for query. *)
@@ -302,6 +306,7 @@ struct
     | GhostVarAvailable _ -> MayBool.top ()
     | InvariantGlobalNodes -> NS.top ()
     | DescendantThreads _ -> ConcDomain.ThreadSet.top ()
+    | CreationLockset _ -> CL.top ()
     | MustlockHistory -> LH.top ()
 end
 
@@ -375,7 +380,8 @@ struct
     | Any (GhostVarAvailable _) -> 62
     | Any InvariantGlobalNodes -> 63
     | Any (DescendantThreads _) -> 64
-    | Any (MustlockHistory) -> 65
+    | Any (CreationLockset _) -> 65
+    | Any (MustlockHistory) -> 66
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -436,6 +442,7 @@ struct
       | Any (GasExhausted f1), Any (GasExhausted f2) -> CilType.Fundec.compare f1 f2
       | Any (GhostVarAvailable v1), Any (GhostVarAvailable v2) -> WitnessGhostVar.compare v1 v2
       | Any (DescendantThreads t1), Any (DescendantThreads t2) -> ThreadIdDomain.Thread.compare t1 t2
+      | Any (CreationLockset t1), Any (CreationLockset t2) -> ThreadIdDomain.Thread.compare t1 t2
       (* only argumentless queries should remain *)
       | _, _ -> Stdlib.compare (order a) (order b)
 
@@ -484,6 +491,7 @@ struct
     | Any (GasExhausted f) -> CilType.Fundec.hash f
     | Any (GhostVarAvailable v) -> WitnessGhostVar.hash v
     | Any (DescendantThreads t) -> ThreadIdDomain.Thread.hash t
+    | Any (CreationLockset t) -> ThreadIdDomain.Thread.hash t
     (* IterSysVars:                                                                    *)
     (*   - argument is a function and functions cannot be compared in any meaningful way. *)
     (*   - doesn't matter because IterSysVars is always queried from outside of the analysis, so MCP's query caching is not done for it. *)
@@ -553,6 +561,7 @@ struct
     | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v
     | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes"
     | Any (DescendantThreads t) -> Pretty.dprintf "DescendantThreads %a" ThreadIdDomain.Thread.pretty t
+    | Any (CreationLockset t) -> Pretty.dprintf "CreationLockset %a" ThreadIdDomain.Thread.pretty t
     | Any (MustlockHistory) -> Pretty.dprintf "MustlockHistory"
 end
 

From bb16da6406354af64e12a64617871586858c217d Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Mon, 19 Jan 2026 10:28:46 +0100
Subject: [PATCH 07/24] global descendant locksets

---
 src/analyses/descendantLockset.ml | 63 +++++++++++++++++++++++++------
 1 file changed, 52 insertions(+), 11 deletions(-)

diff --git a/src/analyses/descendantLockset.ml b/src/analyses/descendantLockset.ml
index f6db475ce9..303d9a0987 100644
--- a/src/analyses/descendantLockset.ml
+++ b/src/analyses/descendantLockset.ml
@@ -2,11 +2,24 @@ open Analyses
 module TID = ThreadIdDomain.Thread
 module TIDs = ConcDomain.ThreadSet
 module Lockset = LockDomain.MustLockset
+module TidToLocksetMapTop = MapDomain.MapBot (TID) (Lockset)
 
 module Spec = struct
   include IdentityUnitContextsSpec
   module D = MapDomain.MapBot (TID) (Lockset)
 
+  (** [{ t_0 |-> { t_d |-> L } }]
+
+      [{ t_d |-> L }] is the descendant lockset valid for the [V] value,
+      because [t_d] was created in [t_0] with the lockset being a superset of L.
+  *)
+  module G = MapDomain.MapBot (TID) (TidToLocksetMapTop)
+
+  module V = struct
+    include TID
+    include StdV
+  end
+
   let name () = "descendantLockset"
   let startstate _ = D.empty ()
   let exitstate _ = D.empty ()
@@ -20,17 +33,38 @@ module Spec = struct
     let must_ancestors_descendants = TIDs.filter (TID.must_be_ancestor tid) descendants in
     TIDs.add tid must_ancestors_descendants
 
+  let threadspawn_contribute_globals man tid must_ancestor_descendants =
+    let descendant_lockset = man.local in
+    let contribute_for_descendant t_d =
+      let creation_lockset = man.ask @@ Queries.CreationLockset t_d in
+      let to_contribute =
+        D.fold
+          (fun t_l l_dl acc ->
+             let l_cl = Queries.CL.find tid creation_lockset in
+             let l_inter = Lockset.inter l_cl l_dl in
+             TidToLocksetMapTop.add t_l l_inter acc)
+          descendant_lockset
+          (TidToLocksetMapTop.empty ())
+      in
+      man.sideg t_d (G.singleton tid to_contribute)
+    in
+    TIDs.iter contribute_for_descendant must_ancestor_descendants
+
+  let threadspawn_compute_local_contribution man tid must_ancestor_descendants =
+    let lockset = man.ask Queries.MustLockset in
+    TIDs.fold
+      (fun t_d -> D.join (D.singleton t_d lockset))
+      must_ancestor_descendants
+      man.local
+
   let threadspawn man ~multiple lval f args fman =
     let tid_lifted = man.ask Queries.CurrentThreadId in
     let child_tid_lifted = fman.ask Queries.CurrentThreadId in
     match tid_lifted, child_tid_lifted with
     | `Lifted tid, `Lifted child_tid when TID.must_be_ancestor tid child_tid ->
       let must_ancestor_descendants = must_ancestor_descendants_closure fman child_tid in
-      let lockset = man.ask Queries.MustLockset in
-      TIDs.fold
-        (fun t_d -> D.join (D.singleton t_d lockset))
-        must_ancestor_descendants
-        man.local
+      threadspawn_contribute_globals man tid must_ancestor_descendants;
+      threadspawn_compute_local_contribution man tid must_ancestor_descendants
     | _ -> man.local
 
   let get_must_ancestor_running_descendants man tid =
@@ -75,8 +109,8 @@ module Spec = struct
     | _ -> man.local
 
   module A = struct
-    (** ego tid * lock history * descendant lockset *)
-    include Printable.Prod3 (TID) (Queries.LH) (D)
+    (** ego tid * lock history * (local descendant lockset * global descendant lockset) *)
+    include Printable.Prod3 (TID) (Queries.LH) (Printable.Prod (D) (G))
 
     let happens_before (t1, dl1) (t2, lh2) =
       let locks_held_creating_t2 = D.find t2 dl1 in
@@ -95,8 +129,15 @@ module Spec = struct
              && (TID.equal t_lh t2 || TID.must_be_ancestor t_lh t2))
           relevant_lh2_threads)
 
-    let may_race (t1, lh1, dl1) (t2, lh2, dl2) =
-      not (happens_before (t1, dl1) (t2, lh2) || happens_before (t2, dl2) (t1, lh1))
+    let happens_before_global dlg1 (t2, lh2) =
+      G.exists (fun t dl -> happens_before (t, dl) (t2, lh2)) dlg1
+
+    let may_race (t1, lh1, (dl1, dlg1)) (t2, lh2, (dl2, dlg2)) =
+      not
+        (happens_before (t1, dl1) (t2, lh2)
+         || happens_before (t2, dl2) (t1, lh1)
+         || happens_before_global dlg1 (t2, lh2)
+         || happens_before_global dlg2 (t1, lh1))
 
     let should_print _ = false
   end
@@ -105,8 +146,8 @@ module Spec = struct
     let lh = man.ask Queries.MustlockHistory in
     let tid_lifted = man.ask Queries.CurrentThreadId in
     match tid_lifted with
-    | `Lifted tid -> tid, lh, man.local
-    | _ -> ThreadIdDomain.UnknownThread, Queries.LH.empty (), D.empty ()
+    | `Lifted tid -> tid, lh, (man.local, man.global tid)
+    | _ -> ThreadIdDomain.UnknownThread, Queries.LH.empty (), (D.empty (), G.empty ())
 end
 
 let _ =

From 8f46eb38f1ac10b90db609631d48482f44186955 Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Mon, 19 Jan 2026 10:29:44 +0100
Subject: [PATCH 08/24] regression tests for global descendant locksets

---
 .../53-races-mhp/42-dl_cl_simple_racefree.c   | 31 ++++++++++++++++
 .../44-dl_cl_transitive_create_racefree.c     | 35 +++++++++++++++++++
 .../58-dl_cl_unlock_before_join_racing.c      | 30 ++++++++++++++++
 3 files changed, 96 insertions(+)
 create mode 100644 tests/regression/53-races-mhp/42-dl_cl_simple_racefree.c
 create mode 100644 tests/regression/53-races-mhp/44-dl_cl_transitive_create_racefree.c
 create mode 100644 tests/regression/53-races-mhp/58-dl_cl_unlock_before_join_racing.c

diff --git a/tests/regression/53-races-mhp/42-dl_cl_simple_racefree.c b/tests/regression/53-races-mhp/42-dl_cl_simple_racefree.c
new file mode 100644
index 0000000000..491a414c27
--- /dev/null
+++ b/tests/regression/53-races-mhp/42-dl_cl_simple_racefree.c
@@ -0,0 +1,31 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset --set "ana.activated[+]" creationLockset
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1, id2;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex);
+  // everything from here must happen after unlock in main
+  pthread_mutex_unlock(&mutex);
+  global++; // NORACE
+  return NULL;
+}
+
+void *t2(void *arg) { // t2 is joined into main before unlock happens
+  global++; // NORACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_mutex_lock(&mutex);
+
+  pthread_create(&id1, NULL, t1, NULL);
+
+  pthread_create(&id2, NULL, t2, NULL);
+  pthread_join(id2, NULL);
+
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}
diff --git a/tests/regression/53-races-mhp/44-dl_cl_transitive_create_racefree.c b/tests/regression/53-races-mhp/44-dl_cl_transitive_create_racefree.c
new file mode 100644
index 0000000000..cc603ca032
--- /dev/null
+++ b/tests/regression/53-races-mhp/44-dl_cl_transitive_create_racefree.c
@@ -0,0 +1,35 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset --set "ana.activated[+]" creationLockset
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1, id2, id3;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex);
+  // everything from here must happen after unlock in main
+  pthread_mutex_unlock(&mutex);
+  global++; // NORACE
+  return NULL;
+}
+
+void *t3(void *arg) { // t3 is joined into main before unlock happens
+  global++; // NORACE
+  return NULL;
+}
+
+void *t2(void *arg) {
+  pthread_create(&id3, NULL, t3, NULL);
+}
+
+int main(void) {
+  pthread_mutex_lock(&mutex);
+
+  pthread_create(&id1, NULL, t1, NULL);
+
+  pthread_create(&id2, NULL, t2, NULL);
+  pthread_join(id3, NULL);
+
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}
diff --git a/tests/regression/53-races-mhp/58-dl_cl_unlock_before_join_racing.c b/tests/regression/53-races-mhp/58-dl_cl_unlock_before_join_racing.c
new file mode 100644
index 0000000000..487725b3b3
--- /dev/null
+++ b/tests/regression/53-races-mhp/58-dl_cl_unlock_before_join_racing.c
@@ -0,0 +1,30 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset --set "ana.activated[+]" creationLockset
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1, id2;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex);
+  // everything from here must happen after unlock in main
+  pthread_mutex_unlock(&mutex);
+  global++; // RACE!
+  return NULL;
+}
+
+void *t2(void *arg) { // t2 is joined into main before unlock happens
+    global++; // RACE!
+    return NULL;
+}
+
+int main(void) {
+  pthread_mutex_lock(&mutex);
+
+  pthread_create(&id1, NULL, t1, NULL);
+
+  pthread_create(&id2, NULL, t2, NULL);
+  pthread_mutex_unlock(&mutex);
+  pthread_join(id2, NULL);
+  return 0;
+}

From 61cdb71210941205b5a18044bd6c5639f93f52bf Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Mon, 19 Jan 2026 10:31:45 +0100
Subject: [PATCH 09/24] descendant lockset tests involving multiple mutexes

---
 .../45-dl_multiple_mutexes_racefree.c         | 22 +++++++++++++++++++
 .../59-dl_multiple_mutexes_racing.c           | 22 +++++++++++++++++++
 2 files changed, 44 insertions(+)
 create mode 100644 tests/regression/53-races-mhp/45-dl_multiple_mutexes_racefree.c
 create mode 100644 tests/regression/53-races-mhp/59-dl_multiple_mutexes_racing.c

diff --git a/tests/regression/53-races-mhp/45-dl_multiple_mutexes_racefree.c b/tests/regression/53-races-mhp/45-dl_multiple_mutexes_racefree.c
new file mode 100644
index 0000000000..bc96b37cb5
--- /dev/null
+++ b/tests/regression/53-races-mhp/45-dl_multiple_mutexes_racefree.c
@@ -0,0 +1,22 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex1, mutex2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  pthread_mutex_unlock(&mutex1);
+  global++; // NORACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex2);
+  pthread_create(&id1, NULL, t1, NULL);
+  pthread_mutex_unlock(&mutex2);
+  global++; // NORACE
+  return 0;
+}
diff --git a/tests/regression/53-races-mhp/59-dl_multiple_mutexes_racing.c b/tests/regression/53-races-mhp/59-dl_multiple_mutexes_racing.c
new file mode 100644
index 0000000000..e3ac97d94e
--- /dev/null
+++ b/tests/regression/53-races-mhp/59-dl_multiple_mutexes_racing.c
@@ -0,0 +1,22 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex1, mutex2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  pthread_mutex_unlock(&mutex1);
+  global++; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex2);
+  pthread_create(&id1, NULL, t1, NULL);
+  pthread_mutex_unlock(&mutex1);
+  global++; // RACE!
+  return 0;
+}

From c8cdf89feb3facd69535dcc549efeceb59ad6a4c Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Tue, 20 Jan 2026 09:48:43 +0100
Subject: [PATCH 10/24] fix incorrect indentatoin in regression test

---
 .../53-races-mhp/58-dl_cl_unlock_before_join_racing.c         | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/regression/53-races-mhp/58-dl_cl_unlock_before_join_racing.c b/tests/regression/53-races-mhp/58-dl_cl_unlock_before_join_racing.c
index 487725b3b3..cb6a52c43d 100644
--- a/tests/regression/53-races-mhp/58-dl_cl_unlock_before_join_racing.c
+++ b/tests/regression/53-races-mhp/58-dl_cl_unlock_before_join_racing.c
@@ -14,8 +14,8 @@ void *t1(void *arg) {
 }
 
 void *t2(void *arg) { // t2 is joined into main before unlock happens
-    global++; // RACE!
-    return NULL;
+  global++; // RACE!
+  return NULL;
 }
 
 int main(void) {

From 6c68a6c61ba8fb06ec3da673e007c5e89f5a5a7e Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Tue, 20 Jan 2026 09:49:16 +0100
Subject: [PATCH 11/24] add missing return statement to regression test

---
 .../53-races-mhp/44-dl_cl_transitive_create_racefree.c           | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tests/regression/53-races-mhp/44-dl_cl_transitive_create_racefree.c b/tests/regression/53-races-mhp/44-dl_cl_transitive_create_racefree.c
index cc603ca032..30c7ac75f4 100644
--- a/tests/regression/53-races-mhp/44-dl_cl_transitive_create_racefree.c
+++ b/tests/regression/53-races-mhp/44-dl_cl_transitive_create_racefree.c
@@ -20,6 +20,7 @@ void *t3(void *arg) { // t3 is joined into main before unlock happens
 
 void *t2(void *arg) {
   pthread_create(&id3, NULL, t3, NULL);
+  return NULL;
 }
 
 int main(void) {

From 6020267c773a38d0552302b87d8f9036813c6264 Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Tue, 20 Jan 2026 09:50:52 +0100
Subject: [PATCH 12/24] add missing mutex initializations

---
 tests/regression/53-races-mhp/45-dl_multiple_mutexes_racefree.c | 2 +-
 tests/regression/53-races-mhp/59-dl_multiple_mutexes_racing.c   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/regression/53-races-mhp/45-dl_multiple_mutexes_racefree.c b/tests/regression/53-races-mhp/45-dl_multiple_mutexes_racefree.c
index bc96b37cb5..53c1340cb3 100644
--- a/tests/regression/53-races-mhp/45-dl_multiple_mutexes_racefree.c
+++ b/tests/regression/53-races-mhp/45-dl_multiple_mutexes_racefree.c
@@ -2,7 +2,7 @@
 #include <pthread.h>
 
 int global = 0;
-pthread_mutex_t mutex1, mutex2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER, mutex2 = PTHREAD_MUTEX_INITIALIZER;
 pthread_t id1;
 
 void *t1(void *arg) {
diff --git a/tests/regression/53-races-mhp/59-dl_multiple_mutexes_racing.c b/tests/regression/53-races-mhp/59-dl_multiple_mutexes_racing.c
index e3ac97d94e..4a90cf244f 100644
--- a/tests/regression/53-races-mhp/59-dl_multiple_mutexes_racing.c
+++ b/tests/regression/53-races-mhp/59-dl_multiple_mutexes_racing.c
@@ -2,7 +2,7 @@
 #include <pthread.h>
 
 int global = 0;
-pthread_mutex_t mutex1, mutex2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER, mutex2 = PTHREAD_MUTEX_INITIALIZER;
 pthread_t id1;
 
 void *t1(void *arg) {

From 5bf536d573e000c9efe8f30b628d7968e9f4fd6b Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Tue, 20 Jan 2026 09:53:09 +0100
Subject: [PATCH 13/24] remove redundant whitespace in creation lockset
 analysis

---
 src/analyses/creationLockset.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml
index d6289065da..234e11aa4c 100644
--- a/src/analyses/creationLockset.ml
+++ b/src/analyses/creationLockset.ml
@@ -151,7 +151,7 @@ module Spec = struct
 
   let query man (type a) (x : a Queries.t) : a Queries.result =
     match x with
-    | Queries.CreationLockset t -> (man.global  t : G.t)
+    | Queries.CreationLockset t -> (man.global t : G.t)
     | _ -> Queries.Result.top x
 end
 

From bd388a2638837025c17a6b06d2ead215e4c4a6f6 Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Tue, 20 Jan 2026 10:02:18 +0100
Subject: [PATCH 14/24] remove unused tid function parameter in `unlock` and
 `unknown_unlock` of descendant lockset analysis

---
 src/analyses/descendantLockset.ml | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/analyses/descendantLockset.ml b/src/analyses/descendantLockset.ml
index 303d9a0987..ca5ce09f95 100644
--- a/src/analyses/descendantLockset.ml
+++ b/src/analyses/descendantLockset.ml
@@ -82,17 +82,20 @@ module Spec = struct
     let must_joined_tids = man.ask Queries.MustJoinedThreads in
     TIDs.diff may_transitively_created_tids must_joined_tids
 
-  let unlock man tid possibly_running_tids lock =
+  let unlock man possibly_running_tids lock =
     TIDs.fold
-      (fun tid ->
-         let old_value = D.find tid man.local in
+      (fun des_tid ->
+         let old_value = D.find des_tid man.local in
          let new_value = Lockset.remove lock old_value in
-         D.add tid new_value)
+         D.add des_tid new_value)
       possibly_running_tids
       (D.empty ())
 
-  let unknown_unlock man tid possibly_running_tids =
-    TIDs.fold (fun tid -> D.add tid (Lockset.empty ())) possibly_running_tids (D.empty ())
+  let unknown_unlock man possibly_running_tids =
+    TIDs.fold
+      (fun des_tid -> D.add des_tid (Lockset.empty ()))
+      possibly_running_tids
+      (D.empty ())
 
   let event man e _ =
     match e with
@@ -103,8 +106,8 @@ module Spec = struct
          let possibly_running_tids = get_must_ancestor_running_descendants man tid in
          let lock_opt = LockDomain.MustLock.of_addr addr in
          (match lock_opt with
-          | Some lock -> unlock man tid possibly_running_tids lock
-          | None -> unknown_unlock man tid possibly_running_tids)
+          | Some lock -> unlock man possibly_running_tids lock
+          | None -> unknown_unlock man possibly_running_tids)
        | _ -> man.local)
     | _ -> man.local
 

From 66ad3f139e3f34e7d24113344816738f1cb06e46 Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Tue, 20 Jan 2026 10:15:25 +0100
Subject: [PATCH 15/24] modify global domain to use `D` instances as values

---
 src/analyses/descendantLockset.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/analyses/descendantLockset.ml b/src/analyses/descendantLockset.ml
index ca5ce09f95..7754b1c92f 100644
--- a/src/analyses/descendantLockset.ml
+++ b/src/analyses/descendantLockset.ml
@@ -2,7 +2,6 @@ open Analyses
 module TID = ThreadIdDomain.Thread
 module TIDs = ConcDomain.ThreadSet
 module Lockset = LockDomain.MustLockset
-module TidToLocksetMapTop = MapDomain.MapBot (TID) (Lockset)
 
 module Spec = struct
   include IdentityUnitContextsSpec
@@ -13,7 +12,7 @@ module Spec = struct
       [{ t_d |-> L }] is the descendant lockset valid for the [V] value,
       because [t_d] was created in [t_0] with the lockset being a superset of L.
   *)
-  module G = MapDomain.MapBot (TID) (TidToLocksetMapTop)
+  module G = MapDomain.MapBot (TID) (D)
 
   module V = struct
     include TID
@@ -42,9 +41,9 @@ module Spec = struct
           (fun t_l l_dl acc ->
              let l_cl = Queries.CL.find tid creation_lockset in
              let l_inter = Lockset.inter l_cl l_dl in
-             TidToLocksetMapTop.add t_l l_inter acc)
+             D.add t_l l_inter acc)
           descendant_lockset
-          (TidToLocksetMapTop.empty ())
+          (D.empty ())
       in
       man.sideg t_d (G.singleton tid to_contribute)
     in

From 743092a80fc0d18f9fad20ef648d562a95714f9d Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Wed, 21 Jan 2026 15:18:19 +0100
Subject: [PATCH 16/24] recursive mutex regression tests for descendant
 locksets

---
 .../53-races-mhp/46-dl_recursive_mutex.c      | 30 ++++++++++++++++++
 ...te_before_second_lock_of_recursive_mutex.c | 31 +++++++++++++++++++
 2 files changed, 61 insertions(+)
 create mode 100644 tests/regression/53-races-mhp/46-dl_recursive_mutex.c
 create mode 100644 tests/regression/53-races-mhp/47-dl_create_before_second_lock_of_recursive_mutex.c

diff --git a/tests/regression/53-races-mhp/46-dl_recursive_mutex.c b/tests/regression/53-races-mhp/46-dl_recursive_mutex.c
new file mode 100644
index 0000000000..b5abb8db47
--- /dev/null
+++ b/tests/regression/53-races-mhp/46-dl_recursive_mutex.c
@@ -0,0 +1,30 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset
+#define _GNU_SOURCE
+#include <pthread.h>
+
+int global = 0;
+#ifdef __APPLE__
+pthread_mutex_t mutex = PTHREAD_RECURSIVE_MUTEX_INITIALIZER;
+#else
+pthread_mutex_t mutex = PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP;
+#endif
+pthread_t id1;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex);
+  pthread_mutex_unlock(&mutex);
+  global++;
+  return NULL;
+}
+
+int main(void) {
+  pthread_mutex_lock(&mutex);
+  pthread_mutex_lock(&mutex);
+  pthread_create(&id1, NULL, t1, NULL);
+  global++; // NORACE
+  pthread_mutex_unlock(&mutex);
+  global++; // RACE (the unlock statement above doesn't fully unlock the recursive mutex)
+  pthread_mutex_unlock(&mutex);
+  global++; // RACE!
+  return 0;
+}
diff --git a/tests/regression/53-races-mhp/47-dl_create_before_second_lock_of_recursive_mutex.c b/tests/regression/53-races-mhp/47-dl_create_before_second_lock_of_recursive_mutex.c
new file mode 100644
index 0000000000..e02a01ac60
--- /dev/null
+++ b/tests/regression/53-races-mhp/47-dl_create_before_second_lock_of_recursive_mutex.c
@@ -0,0 +1,31 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset
+#define _GNU_SOURCE
+#include <pthread.h>
+
+int global = 0;
+#ifdef __APPLE__
+pthread_mutex_t mutex = PTHREAD_RECURSIVE_MUTEX_INITIALIZER;
+#else
+pthread_mutex_t mutex = PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP;
+#endif
+pthread_t id1;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex);
+  pthread_mutex_unlock(&mutex);
+  global++;
+  return NULL;
+}
+
+int main(void) {
+  pthread_mutex_lock(&mutex);
+  pthread_create(&id1, NULL, t1, NULL);
+  global++; // NORACE
+  pthread_mutex_lock(&mutex);
+  global++; // NORACE
+  pthread_mutex_unlock(&mutex);
+  global++; // RACE (the unlock statement above doesn't fully unlock the recursive mutex)
+  pthread_mutex_unlock(&mutex);
+  global++; // RACE!
+  return 0;
+}

From 346121473f5f832d2c140b1a409e26ce54f863b1 Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Sun, 25 Jan 2026 10:29:04 +0100
Subject: [PATCH 17/24] use `MapTop` instead of `MapBot` for inner map of
 descendant lockset global domain

---
 src/analyses/descendantLockset.ml | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/analyses/descendantLockset.ml b/src/analyses/descendantLockset.ml
index 7754b1c92f..649c9f795e 100644
--- a/src/analyses/descendantLockset.ml
+++ b/src/analyses/descendantLockset.ml
@@ -2,6 +2,7 @@ open Analyses
 module TID = ThreadIdDomain.Thread
 module TIDs = ConcDomain.ThreadSet
 module Lockset = LockDomain.MustLockset
+module TidToLocksetMapTop = MapDomain.MapTop (TID) (Lockset)
 
 module Spec = struct
   include IdentityUnitContextsSpec
@@ -12,7 +13,7 @@ module Spec = struct
       [{ t_d |-> L }] is the descendant lockset valid for the [V] value,
       because [t_d] was created in [t_0] with the lockset being a superset of L.
   *)
-  module G = MapDomain.MapBot (TID) (D)
+  module G = MapDomain.MapBot (TID) (TidToLocksetMapTop)
 
   module V = struct
     include TID
@@ -41,9 +42,9 @@ module Spec = struct
           (fun t_l l_dl acc ->
              let l_cl = Queries.CL.find tid creation_lockset in
              let l_inter = Lockset.inter l_cl l_dl in
-             D.add t_l l_inter acc)
+             TidToLocksetMapTop.add t_l l_inter acc)
           descendant_lockset
-          (D.empty ())
+          (TidToLocksetMapTop.empty ())
       in
       man.sideg t_d (G.singleton tid to_contribute)
     in
@@ -132,7 +133,11 @@ module Spec = struct
           relevant_lh2_threads)
 
     let happens_before_global dlg1 (t2, lh2) =
-      G.exists (fun t dl -> happens_before (t, dl) (t2, lh2)) dlg1
+      G.exists
+        (fun t dl_map_top ->
+           let dl_map_bot = TidToLocksetMapTop.fold D.add dl_map_top (D.empty ()) in (* convert MapTop to MapBot *)
+           happens_before (t, dl_map_bot) (t2, lh2))
+        dlg1
 
     let may_race (t1, lh1, (dl1, dlg1)) (t2, lh2, (dl2, dlg2)) =
       not

From 717b52fde8efee638360afdadd97231b480b8cd4 Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Sun, 25 Jan 2026 22:50:43 +0100
Subject: [PATCH 18/24] some documentation in `descendantLockset` analysis

---
 src/analyses/descendantLockset.ml | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/src/analyses/descendantLockset.ml b/src/analyses/descendantLockset.ml
index 649c9f795e..b395f410dd 100644
--- a/src/analyses/descendantLockset.ml
+++ b/src/analyses/descendantLockset.ml
@@ -1,3 +1,11 @@
+(** descendant lockset analysis [descendantLockset]
+    analyzes a happened-before relationship related to thread creations with mutexes held.
+
+    Enabling [creationLockset] may improve the precision of this analysis.
+
+    @see https://github.com/goblint/analyzer/pull/1923
+*)
+
 open Analyses
 module TID = ThreadIdDomain.Thread
 module TIDs = ConcDomain.ThreadSet
@@ -6,12 +14,20 @@ module TidToLocksetMapTop = MapDomain.MapTop (TID) (Lockset)
 
 module Spec = struct
   include IdentityUnitContextsSpec
+
+  (** [{ t_d |-> L }]
+
+      [t_d] was transitively created with all members of [L] held.
+      Additionally, no member of [L] could have been unlocked after the creation of [t_d]
+  *)
   module D = MapDomain.MapBot (TID) (Lockset)
 
   (** [{ t_0 |-> { t_d |-> L } }]
 
       [{ t_d |-> L }] is the descendant lockset valid for the [V] value,
       because [t_d] was created in [t_0] with the lockset being a superset of L.
+
+      We suspect [MapBot] to suffice for the inner map. To ensure soundness, we use [MapTop] instead
   *)
   module G = MapDomain.MapBot (TID) (TidToLocksetMapTop)
 

From ee18c9a8e36ac1bdeed1af88fa09dedc122060d5 Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Sun, 25 Jan 2026 23:12:34 +0100
Subject: [PATCH 19/24] improve printing of `descendantLockset` analysis

---
 src/analyses/descendantLockset.ml | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/analyses/descendantLockset.ml b/src/analyses/descendantLockset.ml
index b395f410dd..dc6df25f80 100644
--- a/src/analyses/descendantLockset.ml
+++ b/src/analyses/descendantLockset.ml
@@ -128,8 +128,10 @@ module Spec = struct
     | _ -> man.local
 
   module A = struct
+    module DlProd = Printable.Prod (D) (G)
+
     (** ego tid * lock history * (local descendant lockset * global descendant lockset) *)
-    include Printable.Prod3 (TID) (Queries.LH) (Printable.Prod (D) (G))
+    include Printable.Prod3 (TID) (Queries.LH) (DlProd)
 
     let happens_before (t1, dl1) (t2, lh2) =
       let locks_held_creating_t2 = D.find t2 dl1 in
@@ -162,7 +164,16 @@ module Spec = struct
          || happens_before_global dlg1 (t2, lh2)
          || happens_before_global dlg2 (t1, lh1))
 
-    let should_print _ = false
+    (* only descendant locksets need to be printed *)
+    let pretty () (_, _, dl) = DlProd.pretty () dl
+    let show (_, _, dl) = DlProd.show dl
+    let to_yojson (_, _, dl) = DlProd.to_yojson dl
+    let printXml f (_, _, dl) = DlProd.printXml f dl
+
+    let should_print (_, _, (dl, dlg)) =
+      let ls_not_empty _ ls = not @@ Lockset.is_empty ls in
+      D.exists (ls_not_empty) dl
+      || G.exists (fun _ -> TidToLocksetMapTop.exists (ls_not_empty)) dlg
   end
 
   let access man _ =

From 9f5b2645f9ed5ae41a4a779836c9b3e8c0ac3a96 Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Sun, 25 Jan 2026 23:53:03 +0100
Subject: [PATCH 20/24] documentation for `mustlockHistory` analysis

---
 src/analyses/mustlockHistory.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/analyses/mustlockHistory.ml b/src/analyses/mustlockHistory.ml
index d9747ea7cb..92df6de611 100644
--- a/src/analyses/mustlockHistory.ml
+++ b/src/analyses/mustlockHistory.ml
@@ -1,9 +1,21 @@
+(** must-lock history analysis [mustlockHistory]
+    collects for locks, in which threads a lock operation must have happened
+    before reaching the current program point.
+
+    @see https://github.com/goblint/analyzer/pull/1923
+*)
+
 open Analyses
 module TIDs = SetDomain.Reverse (ConcDomain.ThreadSet)
 module Lock = LockDomain.MustLock
 
 module Spec = struct
   include IdentityUnitContextsSpec
+
+  (** [{ l |-> T }]
+
+      [l] must have been in all members of [T].
+  *)
   module D = Queries.LH
 
   let name () = "mustlockHistory"

From 83d6f5af9c3ba49367d57658aef65737e1496d41 Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Sun, 25 Jan 2026 23:54:03 +0100
Subject: [PATCH 21/24] remove unused dependencies from mustlock history
 analysis

---
 src/analyses/mustlockHistory.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/src/analyses/mustlockHistory.ml b/src/analyses/mustlockHistory.ml
index 92df6de611..ea862927e2 100644
--- a/src/analyses/mustlockHistory.ml
+++ b/src/analyses/mustlockHistory.ml
@@ -44,7 +44,4 @@ module Spec = struct
     | _ -> Queries.Result.top x
 end
 
-let _ =
-  MCP.register_analysis
-    ~dep:[ "threadid"; "threadJoins"; "threadDescendants" ]
-    (module Spec : MCPSpec)
+let _ = MCP.register_analysis ~dep:[ "threadid" ] (module Spec : MCPSpec)

From a71d29e18af53e3f9af903f1d7cb3089914f6e85 Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Mon, 26 Jan 2026 20:05:54 +0100
Subject: [PATCH 22/24] refactor functions related to thread descendants

---
 src/analyses/creationLockset.ml   | 37 +++++--------------------------
 src/analyses/descendantLockset.ml | 32 +++++---------------------
 src/analyses/threadDescendants.ml | 31 ++++++++++++++++++++++++++
 3 files changed, 43 insertions(+), 57 deletions(-)

diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml
index 234e11aa4c..8998b5bc39 100644
--- a/src/analyses/creationLockset.ml
+++ b/src/analyses/creationLockset.ml
@@ -33,46 +33,19 @@ module Spec = struct
   *)
   let contribute_locks man to_contribute child_tid = man.sideg child_tid to_contribute
 
-  (** reflexive-transitive closure of child relation applied to [tid]
-      and filtered to only include threads, where [tid] is a must-ancestor
-      @param man any man
-      @param tid
-  *)
-  let must_ancestor_descendants_closure man tid =
-    let descendants = man.ask @@ Queries.DescendantThreads tid in
-    let must_ancestors_descendants = TIDs.filter (TID.must_be_ancestor tid) descendants in
-    TIDs.add tid must_ancestors_descendants
-
   let threadspawn man ~multiple lval f args fman =
     let tid_lifted = man.ask Queries.CurrentThreadId in
     let child_tid_lifted = fman.ask Queries.CurrentThreadId in
     match tid_lifted, child_tid_lifted with
     | `Lifted tid, `Lifted child_tid when TID.must_be_ancestor tid child_tid ->
-      let must_ancestor_descendants = must_ancestor_descendants_closure fman child_tid in
+      let must_ancestor_descendants =
+        ThreadDescendants.must_ancestor_descendants_closure (ask_of_man fman) child_tid
+      in
       let lockset = man.ask Queries.MustLockset in
       let to_contribute = G.singleton tid lockset in
       TIDs.iter (contribute_locks man to_contribute) must_ancestor_descendants
     | _ -> ()
 
-  (** compute all descendant threads that may run along with the ego thread at a program point.
-      for all of them, tid must be an ancestor
-      @param man man of ego thread at the program point
-      @param tid ego thread id
-  *)
-  let get_must_ancestor_running_descendants man tid =
-    let may_created_tids = man.ask Queries.CreatedThreads in
-    let may_must_ancestor_created_tids =
-      TIDs.filter (TID.must_be_ancestor tid) may_created_tids
-    in
-    let may_transitively_created_tids =
-      TIDs.fold
-        (fun child_tid acc -> TIDs.union acc (must_ancestor_descendants_closure man child_tid))
-        may_must_ancestor_created_tids
-        (TIDs.empty ())
-    in
-    let must_joined_tids = man.ask Queries.MustJoinedThreads in
-    TIDs.diff may_transitively_created_tids must_joined_tids
-
   (** handle unlock of mutex [lock] *)
   let unlock man tid possibly_running_tids lock =
     let shrink_locksets des_tid =
@@ -98,7 +71,9 @@ module Spec = struct
       let tid_lifted = man.ask Queries.CurrentThreadId in
       (match tid_lifted with
        | `Lifted tid ->
-         let possibly_running_tids = get_must_ancestor_running_descendants man tid in
+         let possibly_running_tids =
+           ThreadDescendants.must_ancestor_running_descendants (ask_of_man man) tid
+         in
          let lock_opt = LockDomain.MustLock.of_addr addr in
          (match lock_opt with
           | Some lock -> unlock man tid possibly_running_tids lock
diff --git a/src/analyses/descendantLockset.ml b/src/analyses/descendantLockset.ml
index dc6df25f80..60c5237f3a 100644
--- a/src/analyses/descendantLockset.ml
+++ b/src/analyses/descendantLockset.ml
@@ -40,15 +40,6 @@ module Spec = struct
   let startstate _ = D.empty ()
   let exitstate _ = D.empty ()
 
-  (** reflexive-transitive closure of child relation applied to [tid] and
-      filtered to only include threads, where [tid] is a must-ancestor
-      @param man any man
-      @param tid *)
-  let must_ancestor_descendants_closure man tid =
-    let descendants = man.ask @@ Queries.DescendantThreads tid in
-    let must_ancestors_descendants = TIDs.filter (TID.must_be_ancestor tid) descendants in
-    TIDs.add tid must_ancestors_descendants
-
   let threadspawn_contribute_globals man tid must_ancestor_descendants =
     let descendant_lockset = man.local in
     let contribute_for_descendant t_d =
@@ -78,26 +69,13 @@ module Spec = struct
     let child_tid_lifted = fman.ask Queries.CurrentThreadId in
     match tid_lifted, child_tid_lifted with
     | `Lifted tid, `Lifted child_tid when TID.must_be_ancestor tid child_tid ->
-      let must_ancestor_descendants = must_ancestor_descendants_closure fman child_tid in
+      let must_ancestor_descendants =
+        ThreadDescendants.must_ancestor_descendants_closure (ask_of_man fman) child_tid
+      in
       threadspawn_contribute_globals man tid must_ancestor_descendants;
       threadspawn_compute_local_contribution man tid must_ancestor_descendants
     | _ -> man.local
 
-  let get_must_ancestor_running_descendants man tid =
-    let may_created_tids = man.ask Queries.CreatedThreads in
-    let may_must_ancestor_created_tids =
-      TIDs.filter (TID.must_be_ancestor tid) may_created_tids
-    in
-    let may_transitively_created_tids =
-      TIDs.fold
-        (fun child_tid acc ->
-           TIDs.union acc (must_ancestor_descendants_closure man child_tid))
-        may_must_ancestor_created_tids
-        (TIDs.empty ())
-    in
-    let must_joined_tids = man.ask Queries.MustJoinedThreads in
-    TIDs.diff may_transitively_created_tids must_joined_tids
-
   let unlock man possibly_running_tids lock =
     TIDs.fold
       (fun des_tid ->
@@ -119,7 +97,9 @@ module Spec = struct
       let tid_lifted = man.ask Queries.CurrentThreadId in
       (match tid_lifted with
        | `Lifted tid ->
-         let possibly_running_tids = get_must_ancestor_running_descendants man tid in
+         let possibly_running_tids =
+           ThreadDescendants.must_ancestor_running_descendants (ask_of_man man) tid
+         in
          let lock_opt = LockDomain.MustLock.of_addr addr in
          (match lock_opt with
           | Some lock -> unlock man possibly_running_tids lock
diff --git a/src/analyses/threadDescendants.ml b/src/analyses/threadDescendants.ml
index 22d7911fa4..8f524d8fc7 100644
--- a/src/analyses/threadDescendants.ml
+++ b/src/analyses/threadDescendants.ml
@@ -4,6 +4,37 @@
 
 open Analyses
 module TID = ThreadIdDomain.Thread
+module TIDs = ConcDomain.ThreadSet
+
+(** reflexive-transitive closure of child relation applied to [tid] and
+    filtered to only include threads, where [tid] is a must-ancestor
+    @param ask any ask
+    @param tid
+*)
+let must_ancestor_descendants_closure (ask: Queries.ask) tid =
+  let descendants = ask.f @@ Queries.DescendantThreads tid in
+  let must_ancestors_descendants = TIDs.filter (TID.must_be_ancestor tid) descendants in
+  TIDs.add tid must_ancestors_descendants
+
+(** compute all descendant threads that may run along with the ego thread at a program point.
+    for all of them, tid must be an ancestor
+    @param man man of ego thread at the program point
+    @param tid ego thread id
+*)
+let must_ancestor_running_descendants (ask: Queries.ask) tid =
+  let may_created_tids = ask.f Queries.CreatedThreads in
+  let may_must_ancestor_created_tids =
+    TIDs.filter (TID.must_be_ancestor tid) may_created_tids
+  in
+  let may_transitively_created_tids =
+    TIDs.fold
+      (fun child_tid acc ->
+         TIDs.union acc (must_ancestor_descendants_closure ask child_tid))
+      may_must_ancestor_created_tids
+      (TIDs.empty ())
+  in
+  let must_joined_tids = ask.f Queries.MustJoinedThreads in
+  TIDs.diff may_transitively_created_tids must_joined_tids
 
 module Spec = struct
   include IdentityUnitContextsSpec

From be913baa4d53a7d49f80be133c82e8a59ff4c7b4 Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Mon, 26 Jan 2026 22:44:39 +0100
Subject: [PATCH 23/24] locally abstract type for `happens_before` function in
 `descendantLockset` analysis

---
 src/analyses/descendantLockset.ml | 23 ++++++++++++++++-------
 1 file changed, 16 insertions(+), 7 deletions(-)

diff --git a/src/analyses/descendantLockset.ml b/src/analyses/descendantLockset.ml
index 60c5237f3a..f2cf4f3e86 100644
--- a/src/analyses/descendantLockset.ml
+++ b/src/analyses/descendantLockset.ml
@@ -113,8 +113,15 @@ module Spec = struct
     (** ego tid * lock history * (local descendant lockset * global descendant lockset) *)
     include Printable.Prod3 (TID) (Queries.LH) (DlProd)
 
-    let happens_before (t1, dl1) (t2, lh2) =
-      let locks_held_creating_t2 = D.find t2 dl1 in
+    module type TidToLs = MapDomain.S with type key = TID.t and type value = Lockset.t
+
+    (** checks if program point 1 must happen before program point 2
+        @param (t1,dl1) thread id and descendant lockset of program point 1
+        @param (t2,lh2) thread id and mustlock history of program point 2
+        @param M module of [dl1]
+    *)
+    let happens_before (type t) (t1, dl1) (t2, lh2) (module M : TidToLs with type t = t) =
+      let locks_held_creating_t2 = M.find t2 dl1 in
       if Lockset.is_bot locks_held_creating_t2
       then false
       else (
@@ -130,17 +137,19 @@ module Spec = struct
              && (TID.equal t_lh t2 || TID.must_be_ancestor t_lh t2))
           relevant_lh2_threads)
 
+    (** checks if the entire execution of a thread must happen before a program point
+        @param dlg1 glabal descendant lockset of the thread
+        @param (t2,lh2) thread id and mustlock history of the program point
+    *)
     let happens_before_global dlg1 (t2, lh2) =
       G.exists
-        (fun t dl_map_top ->
-           let dl_map_bot = TidToLocksetMapTop.fold D.add dl_map_top (D.empty ()) in (* convert MapTop to MapBot *)
-           happens_before (t, dl_map_bot) (t2, lh2))
+        (fun t dl_map -> happens_before (t, dl_map) (t2, lh2) (module TidToLocksetMapTop))
         dlg1
 
     let may_race (t1, lh1, (dl1, dlg1)) (t2, lh2, (dl2, dlg2)) =
       not
-        (happens_before (t1, dl1) (t2, lh2)
-         || happens_before (t2, dl2) (t1, lh1)
+        (happens_before (t1, dl1) (t2, lh2) (module D)
+         || happens_before (t2, dl2) (t1, lh1) (module D)
          || happens_before_global dlg1 (t2, lh2)
          || happens_before_global dlg2 (t1, lh1))
 

From 624254b9217ffd34d5db2b33125091cbd5d28711 Mon Sep 17 00:00:00 2001
From: dabund24 <dev@dabund24.de>
Date: Wed, 28 Jan 2026 10:03:21 +0100
Subject: [PATCH 24/24] also print mustlock history in `A` of descendant
 lockset analysis

---
 src/analyses/descendantLockset.ml | 29 +++++++++++++++--------------
 1 file changed, 15 insertions(+), 14 deletions(-)

diff --git a/src/analyses/descendantLockset.ml b/src/analyses/descendantLockset.ml
index f2cf4f3e86..632be40165 100644
--- a/src/analyses/descendantLockset.ml
+++ b/src/analyses/descendantLockset.ml
@@ -108,10 +108,10 @@ module Spec = struct
     | _ -> man.local
 
   module A = struct
-    module DlProd = Printable.Prod (D) (G)
+    module DlLhProd = Printable.Prod3 (D) (G) (Queries.LH)
 
-    (** ego tid * lock history * (local descendant lockset * global descendant lockset) *)
-    include Printable.Prod3 (TID) (Queries.LH) (DlProd)
+    (** ego tid * (local descendant lockset * global descendant lockset * lock history) *)
+    include Printable.Prod (TID) (DlLhProd)
 
     module type TidToLs = MapDomain.S with type key = TID.t and type value = Lockset.t
 
@@ -146,31 +146,32 @@ module Spec = struct
         (fun t dl_map -> happens_before (t, dl_map) (t2, lh2) (module TidToLocksetMapTop))
         dlg1
 
-    let may_race (t1, lh1, (dl1, dlg1)) (t2, lh2, (dl2, dlg2)) =
+    let may_race (t1, (dl1, dlg1, lh1)) (t2, (dl2, dlg2, lh2)) =
       not
         (happens_before (t1, dl1) (t2, lh2) (module D)
          || happens_before (t2, dl2) (t1, lh1) (module D)
          || happens_before_global dlg1 (t2, lh2)
          || happens_before_global dlg2 (t1, lh1))
 
-    (* only descendant locksets need to be printed *)
-    let pretty () (_, _, dl) = DlProd.pretty () dl
-    let show (_, _, dl) = DlProd.show dl
-    let to_yojson (_, _, dl) = DlProd.to_yojson dl
-    let printXml f (_, _, dl) = DlProd.printXml f dl
+    (* ego tid is already printed elsewhere *)
+    let pretty () (_, dl_dlg_lh) = DlLhProd.pretty () dl_dlg_lh
+    let show (_, dl_dlg_lh) = DlLhProd.show dl_dlg_lh
+    let to_yojson (_, dl_dlg_lh) = DlLhProd.to_yojson dl_dlg_lh
+    let printXml f (_, dl_dlg_lh) = DlLhProd.printXml f dl_dlg_lh
 
-    let should_print (_, _, (dl, dlg)) =
+    let should_print (_, (dl, dlg, lh)) =
       let ls_not_empty _ ls = not @@ Lockset.is_empty ls in
-      D.exists (ls_not_empty) dl
-      || G.exists (fun _ -> TidToLocksetMapTop.exists (ls_not_empty)) dlg
+      D.exists ls_not_empty dl
+      || G.exists (fun _ -> TidToLocksetMapTop.exists ls_not_empty) dlg
+      || Queries.LH.exists (fun l tids -> not @@ TIDs.is_empty tids) lh
   end
 
   let access man _ =
     let lh = man.ask Queries.MustlockHistory in
     let tid_lifted = man.ask Queries.CurrentThreadId in
     match tid_lifted with
-    | `Lifted tid -> tid, lh, (man.local, man.global tid)
-    | _ -> ThreadIdDomain.UnknownThread, Queries.LH.empty (), (D.empty (), G.empty ())
+    | `Lifted tid -> tid, (man.local, man.global tid, lh)
+    | _ -> ThreadIdDomain.UnknownThread, (D.empty (), G.empty (), Queries.LH.empty ())
 end
 
 let _ =