HB-relationship involving thread creations while mutexes are held #1913

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open

dabund24 wants to merge 28 commits into goblint:master from dabund24:descendant-locksets

src/analyses/creationLockset.ml

-Original file line number
+Diff line change
@@ Expand Up / @@ -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 ()
@@ Expand All / @@ -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 =
@@ Expand All / @@ -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
@@ Expand Down Expand Up / @@ -148,6 +123,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 _ =
@@ Expand Down @@

src/analyses/descendantLockset.ml

-Original file line number
+Diff line change
@@ -0,0 +1,180 @@
+    (** 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
+    module Lockset = LockDomain.MustLockset
+    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)
+      module V = struct
+        include TID
+        include StdV
+      end
+      let name () = "descendantLockset"
+      let startstate _ = D.empty ()
+      let exitstate _ = D.empty ()
+      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 =
+            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 unlock man possibly_running_tids lock =
+        TIDs.fold
+          (fun des_tid ->
+             let old_value = D.find des_tid man.local in
+             let new_value = Lockset.remove lock old_value in
+             D.add des_tid new_value)
+          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
+        | Events.Unlock addr ->
+          let tid_lifted = man.ask Queries.CurrentThreadId in
+          (match tid_lifted with
+           | `Lifted tid ->
+             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
+              | None -> unknown_unlock man possibly_running_tids)
+           | _ -> man.local)
+        | _ -> 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)
+        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 (
+            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) (module TidToLocksetMapTop))
+            dlg1
+        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))
+        (* 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 _ -> 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, (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

-Original file line number
+Diff line change
@@ -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

-Original file line number
+Diff line change
@@ Expand Up / @@ -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
@@ Expand Down @@

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

HB-relationship involving thread creations while mutexes are held #1913

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!

Uh oh!

Uh oh!

HB-relationship involving thread creations while mutexes are held #1913

Are you sure you want to change the base?

Uh oh!

HB-relationship involving thread creations while mutexes are held #1913

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!

Uh oh!

Uh oh!