HB-relationship involving thread creations while mutexes are held

src/analyses/creationLockset.ml

@@ -1,8 +1,9 @@
 (** creation lockset analysis [creationLockset]
     constructs edges on the graph over all threads, where the edges are labelled with must-locksets:
     (t_1) ---L--> (t_0) is represented by global t_1 t_0 = L and means that t_1 is protected by all members of L from t_0
+    If L is bot, this does not represent "all mutexes". Instead, it indicates that t_1 is never (transitively) created from t_0
 
-    @see https://github.com/goblint/analyzer/pull/1865
+    @see Daniel Bund. "Leveraging the Potential of Inter-Threaded Locksets in Abstract Interpretation", B.Sc. thesis at TUM. Available upon request.
 *)
 
 open Analyses
@@ -14,13 +15,8 @@ module Lockset = LockDomain.MustLockset
 module Spec = struct
   include IdentityUnitContextsSpec
   module D = Lattice.Unit
-
-  module V = struct
-    include TID
-    include StdV
-  end
-
-  module G = MapDomain.MapBot (TID) (Lockset)
+  module V = TIDV
+  module G = Queries.CL
 
   let name () = "creationLockset"
   let startstate _ = D.bot ()
@@ -33,46 +29,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 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_mustset 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 +67,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.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
@@ -154,6 +125,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 _ =

src/analyses/descendantLockset.ml

@@ -0,0 +1,165 @@
+(** 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 Daniel Bund. "Leveraging the Potential of Inter-Threaded Locksets in Abstract Interpretation", B.Sc. thesis at TUM. Available upon request.
+*)
+
+open Analyses
+module TID = ThreadIdDomain.Thread
+module TIDs = ConcDomain.ThreadSet
+module Lockset = LockDomain.MustLockset
+
+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]
+      If [L] is bot, this does not represent "all mutexes". Instead, it indicates no (transitive) creation of [t_d] has happened
+  *)
+  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) (D)
+
+  module V = TIDV
+
+  let name () = "descendantLockset"
+  let startstate _ = D.empty ()
+  let exitstate _ = D.empty ()
+
+  let threadenter man ~multiple lval f args = [ D.empty () ]
+
+  let threadspawn_contribute_globals man tid must_ancestor_descendants =
+    let descendant_lockset = man.local in
+
+    (* intersect locksets, but return bot if any arg is bot *)
+    let lockset_inter_sticky_bot = function
+      | `Top, _ | _, `Top -> Lockset.bot ()
+      | ls1, ls2 -> Lockset.inter ls1 ls2
+    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_sticky_bot (l_cl, l_dl) in
+             D.add t_l l_inter acc)
+          descendant_lockset
+          (D.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 =
+        ThreadDescendants.must_ancestor_descendants_closure fman child_tid
+      in
+      threadspawn_contribute_globals man tid must_ancestor_descendants;
+      threadspawn_compute_local_contribution man tid must_ancestor_descendants
+    | _ -> man.local
+
+  let unlock man lock =
+    D.map (Lockset.remove lock) man.local
+
+  let unknown_unlock man =
+    D.map (fun _ -> Lockset.empty ()) man.local
+
+  let event man e _ =
+    match e with
+    | Events.Unlock addr ->
+      let lock_opt = LockDomain.MustLock.of_addr addr in
+      (match lock_opt with
+       | Some lock -> unlock man lock
+       | None -> unknown_unlock man)
+    | _ -> man.local
+
+  module A = struct
+    module DlLhProd = Printable.Prod3 (D) (G) (Queries.LH)
+
+    (** ego tid * (local descendant lockset * global descendant lockset * lock history) *)
+    include Printable.Prod (TID) (DlLhProd)
+
+    (** 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 (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
+
+    (** 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 -> happens_before (t, dl_map) (t2, lh2)) dlg1
+
+    let may_race (t1, (dl1, dlg1, lh1)) (t2, (dl2, dlg2, lh2)) =
+      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))
+
+    (* 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, lh)) =
+      let ls_not_empty _ ls = not @@ Lockset.is_empty ls in
+      D.exists ls_not_empty dl
+      || G.exists (fun _ -> D.exists ls_not_empty) dlg
+      || Queries.LH.exists (fun l tids -> not @@ TIDs.is_empty tids) lh
+  end
+
+  let access man _ =
+    let tid_lifted = man.ask Queries.CurrentThreadId in
+    match tid_lifted with
+    | `Lifted tid ->
+      let lh = man.ask Queries.MustlockHistory in
+      tid, (man.local, man.global tid, lh)
+    | _ -> ThreadIdDomain.UnknownThread, (D.empty (), G.empty (), Queries.LH.empty ())
+end
+
+let _ =
+  MCP.register_analysis
+    ~dep:[ "threadid"; "mutex"; "threadJoins"; "threadDescendants"; "mustlockHistory" ]
+    (module Spec : MCPSpec)

src/analyses/mustlockHistory.ml

@@ -0,0 +1,47 @@
+(** 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"
+  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" ] (module Spec : MCPSpec)

src/analyses/threadDescendants.ml

@@ -4,16 +4,41 @@
 
 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 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
+
+(** 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_mustset may_transitively_created_tids must_joined_tids
 
 module Spec = struct
   include IdentityUnitContextsSpec
   module D = Lattice.Unit
-
-  module V = struct
-    include TID
-    include StdV
-  end
-
+  module V = TIDV
   module G = ConcDomain.ThreadSet
 
   let name () = "threadDescendants"

src/analyses/threadJoins.ml

@@ -24,11 +24,7 @@ struct
   module D = Lattice.Prod(MustTIDsWithBot)(CleanExit)
   include Analyses.ValueContexts(D)
   module G = D
-  module V =
-  struct
-    include TID
-    include StdV
-  end
+  module V = TIDV
 
   (* transfer functions *)
   let threadreturn man =