diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml new file mode 100644 index 0000000000..118dc2d590 --- /dev/null +++ b/src/analyses/creationLockset.ml @@ -0,0 +1,156 @@ +(** 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 + + @see https://github.com/goblint/analyzer/pull/1865 +*) + +open Analyses +module TID = ThreadIdDomain.Thread +module TIDs = ConcDomain.ThreadSet +module Lock = LockDomain.MustLock +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) + + let name () = "creationLockset" + let startstate _ = D.bot () + let exitstate _ = D.bot () + + (** register a global contribution: global.[child_tid] \supseteq [to_contribute] + @param man man at program point + @param to_contribute new edges from [child_tid] to ego thread to register + @param child_tid + *) + 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 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 = + let old_creation_lockset = G.find tid (man.global des_tid) in + (* Bot - {something} = Bot. This is exactly what we want in this case! *) + let updated_creation_lockset = Lockset.remove lock old_creation_lockset in + let to_contribute = G.singleton tid updated_creation_lockset in + man.sideg des_tid to_contribute + in + TIDs.iter shrink_locksets possibly_running_tids + + (** handle unlock of an unknown mutex. Assumes that any mutex could have been unlocked *) + let unknown_unlock man tid possibly_running_tids = + let evaporate_locksets des_tid = + let to_contribute = G.singleton tid (Lockset.empty ()) in + man.sideg des_tid to_contribute + in + TIDs.iter evaporate_locksets possibly_running_tids + + 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) + | _ -> ()) + | _ -> () + + module A = struct + (** ego tid * must-lockset * creation-lockset *) + include Printable.Prod3 (TID) (Lockset) (G) + + let name () = "creationLockset" + + (** checks if [cl1] has a mapping ([tp1] |-> [ls1]) + such that [ls1] and [ls2] are not disjoint and [tp1] != [t2] + @param cl1 creation-lockset of thread [t1] at first program point + @param t2 thread id at second program point + @param ls2 lockset at second program point + @returns whether [t1] must be running mutually exclusive with second program point + *) + let one_protected_inter_threaded_other_intra_threaded cl1 t2 ls2 = + G.exists (fun tp1 ls1 -> not (Lockset.disjoint ls1 ls2 || TID.equal tp1 t2)) cl1 + + (** checks if [cl1] has a member ([tp1] |-> [ls1]) and [cl2] has a member ([tp2] |-> [ls2]) + such that [ls1] and [ls2] are not disjoint and [tp1] != [tp2] + @param cl1 creation-lockset of first thread [t1] + @param cl2 creation-lockset of second thread [t2] + @returns whether [t1] and [t2] must be running mutually exclusive + *) + let both_protected_inter_threaded cl1 cl2 = + G.exists (one_protected_inter_threaded_other_intra_threaded cl1) cl2 + + let may_race (t1, ls1, cl1) (t2, ls2, cl2) = + not + (both_protected_inter_threaded cl1 cl2 + || one_protected_inter_threaded_other_intra_threaded cl1 t2 ls2 + || one_protected_inter_threaded_other_intra_threaded cl2 t1 ls1) + + let should_print (_t, _ls, cl) = not @@ G.is_empty cl + end + + let access man _ = + let tid_lifted = man.ask Queries.CurrentThreadId in + match tid_lifted with + | `Lifted tid -> + let lockset = man.ask Queries.MustLockset in + let creation_lockset = man.global tid in + tid, lockset, creation_lockset + | _ -> ThreadIdDomain.UnknownThread, Lockset.empty (), G.empty () +end + +let _ = + MCP.register_analysis + ~dep:[ "threadid"; "mutex"; "threadJoins"; "threadDescendants" ] + (module Spec : MCPSpec) diff --git a/src/analyses/mutexGhosts.ml b/src/analyses/mutexGhosts.ml index 98fd33d621..0007a6221b 100644 --- a/src/analyses/mutexGhosts.ml +++ b/src/analyses/mutexGhosts.ml @@ -61,11 +61,6 @@ struct let create_update = create_threadcreate end - let mustlock_of_addr (addr: LockDomain.Addr.t): LockDomain.MustLock.t option = - match addr with - | Addr mv when LockDomain.Mval.is_definite mv -> Some (LockDomain.MustLock.of_mval mv) - | _ -> None - let event man e oman = let verifier_atomic_addr = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var in begin match e with @@ -78,7 +73,7 @@ struct Locked.iter (fun lock -> Option.iter (fun lock -> man.sideg (V.lock lock) (G.create_lock true) - ) (mustlock_of_addr lock) + ) (LockDomain.MustLock.of_addr lock) ) locked ); ) @@ -91,7 +86,7 @@ struct Locked.iter (fun lock -> Option.iter (fun lock -> man.sideg (V.lock lock) (G.create_lock true) - ) (mustlock_of_addr lock) + ) (LockDomain.MustLock.of_addr lock) ) unlocked ); ) @@ -128,7 +123,7 @@ struct let (locked, unlocked, multithread) = G.node (man.global (V.node node)) in let variables' = Locked.fold (fun l acc -> - match mustlock_of_addr l with + match LockDomain.MustLock.of_addr l with | Some l when ghost_var_available man (Locked l) -> let variable = WitnessGhost.variable' (Locked l) in VariableSet.add variable acc @@ -138,7 +133,7 @@ struct in let updates = Locked.fold (fun l acc -> - match mustlock_of_addr l with + match LockDomain.MustLock.of_addr l with | Some l when ghost_var_available man (Locked l) -> let update = WitnessGhost.update' (Locked l) GoblintCil.one in update :: acc @@ -148,7 +143,7 @@ struct in let updates = Unlocked.fold (fun l acc -> - match mustlock_of_addr l with + match LockDomain.MustLock.of_addr l with | Some l when ghost_var_available man (Locked l) -> let update = WitnessGhost.update' (Locked l) GoblintCil.zero in update :: acc diff --git a/src/analyses/threadDescendants.ml b/src/analyses/threadDescendants.ml new file mode 100644 index 0000000000..22d7911fa4 --- /dev/null +++ b/src/analyses/threadDescendants.ml @@ -0,0 +1,42 @@ +(** thread descendants analysis [threadDescendants] + flow-insensitive construction of descendants may-set for every thread +*) + +open Analyses +module TID = ThreadIdDomain.Thread + +module Spec = struct + include IdentityUnitContextsSpec + module D = Lattice.Unit + + module V = struct + include TID + include StdV + end + + module G = ConcDomain.ThreadSet + + let name () = "threadDescendants" + let startstate _ = D.bot () + let exitstate _ = D.bot () + + let query man (type a) (x : a Queries.t) : a Queries.result = + match x with + | Queries.DescendantThreads t -> + let children = man.global t in + (G.fold + (fun e acc -> G.union (man.ask @@ Queries.DescendantThreads e) acc) + children + children + : G.t) + | _ -> Queries.Result.top x + + 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 -> man.sideg tid (G.singleton child_tid) + | _ -> () +end + +let _ = MCP.register_analysis ~dep:[ "threadid" ] (module Spec : MCPSpec) diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml index e7295f0b56..84978bb125 100644 --- a/src/cdomains/lockDomain.ml +++ b/src/cdomains/lockDomain.ml @@ -29,6 +29,11 @@ struct let of_mval ((v, o): Mval.t): t = (v, Offset.Poly.map_indices (fun i -> IndexDomain.to_int i |> Option.get) o) + let of_addr (addr : Addr.t) : t option = + match addr with + | Addr mv when Mval.is_definite mv -> Some (of_mval mv) + | _ -> None + let to_mval ((v, o): t): Mval.t = (v, Offset.Poly.map_indices (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) o) end diff --git a/src/domains/queries.ml b/src/domains/queries.ml index a5e9586551..6b85a2729c 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -146,6 +146,7 @@ type _ t = | YamlEntryGlobal: Obj.t * YamlWitnessType.Task.t -> YS.t t (** YAML witness entries for a global unknown ([Obj.t] represents [Spec.V.t]) and YAML witness task. *) | 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 type 'a result = 'a @@ -221,6 +222,7 @@ struct | YamlEntryGlobal _ -> (module YS) | GhostVarAvailable _ -> (module MayBool) | InvariantGlobalNodes -> (module NS) + | DescendantThreads _ -> (module ConcDomain.ThreadSet) (** Get bottom result for query. *) let bot (type a) (q: a t): a result = @@ -295,6 +297,7 @@ struct | YamlEntryGlobal _ -> YS.top () | GhostVarAvailable _ -> MayBool.top () | InvariantGlobalNodes -> NS.top () + | DescendantThreads _ -> ConcDomain.ThreadSet.top () end (* The type any_query can't be directly defined in Any as t, @@ -366,6 +369,7 @@ struct | Any (MustProtectingLocks _) -> 61 | Any (GhostVarAvailable _) -> 62 | Any InvariantGlobalNodes -> 63 + | Any (DescendantThreads _) -> 64 let rec compare a b = let r = Stdlib.compare (order a) (order b) in @@ -425,6 +429,7 @@ struct | Any (MaySignedOverflow e1), Any (MaySignedOverflow e2) -> CilType.Exp.compare e1 e2 | 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 (* only argumentless queries should remain *) | _, _ -> Stdlib.compare (order a) (order b) @@ -472,6 +477,7 @@ struct | Any (MaySignedOverflow e) -> CilType.Exp.hash e | Any (GasExhausted f) -> CilType.Fundec.hash f | Any (GhostVarAvailable v) -> WitnessGhostVar.hash v + | Any (DescendantThreads 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. *) @@ -540,6 +546,7 @@ struct | Any (GasExhausted f) -> Pretty.dprintf "GasExhausted %a" CilType.Fundec.pretty f | 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 end let to_value_domain_ask (ask: ask) = diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index 3283697120..92fa69c3b4 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -120,6 +120,7 @@ module ThreadAnalysis = ThreadAnalysis module ThreadJoins = ThreadJoins module MHPAnalysis = MHPAnalysis module ThreadReturn = ThreadReturn +module ThreadDescendants = ThreadDescendants (** {3 Other} *) @@ -131,6 +132,7 @@ module PthreadSignals = PthreadSignals module PthreadBarriers = PthreadBarriers module ExtractPthread = ExtractPthread module PthreadOnce = PthreadOnce +module CreationLockset = CreationLockset (** {2 Longjmp} diff --git a/tests/regression/53-races-mhp/10-lockset_inter_threaded_lock_racefree.c b/tests/regression/53-races-mhp/10-lockset_inter_threaded_lock_racefree.c new file mode 100644 index 0000000000..ef9de824dd --- /dev/null +++ b/tests/regression/53-races-mhp/10-lockset_inter_threaded_lock_racefree.c @@ -0,0 +1,27 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // NORACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is protected by mutex locked in main thread + global++; // NORACE + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + pthread_join(id2, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/53-races-mhp/11-both_inter_threaded_lock_racefree.c b/tests/regression/53-races-mhp/11-both_inter_threaded_lock_racefree.c new file mode 100644 index 0000000000..f60144bfe2 --- /dev/null +++ b/tests/regression/53-races-mhp/11-both_inter_threaded_lock_racefree.c @@ -0,0 +1,33 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id_main_child, id_1, id_1_child; + +void *t1_child_fun(void *arg) { // t1child is protected by mutex locked in t1 + global++; // NORACE + return NULL; +} + +void *tmain_child_fun(void *arg) { // tmainchild is protected by mutex locked in main thread + global++; // NORACE + return NULL; +} + +void *t1_fun(void *arg) { + pthread_mutex_lock(&mutex); + pthread_create(&id_1_child, NULL, t1_child_fun, NULL); + pthread_join(id_1_child, NULL); + pthread_mutex_unlock(&mutex); + return NULL; +} + +int main(void) { + pthread_create(&id_1, NULL, t1_fun, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id_main_child, NULL, tmain_child_fun, NULL); + pthread_join(id_main_child, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/53-races-mhp/12-lockset_inter_threaded_lock_transitive_racefree.c b/tests/regression/53-races-mhp/12-lockset_inter_threaded_lock_transitive_racefree.c new file mode 100644 index 0000000000..5148d30510 --- /dev/null +++ b/tests/regression/53-races-mhp/12-lockset_inter_threaded_lock_transitive_racefree.c @@ -0,0 +1,33 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2, id3; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // NORACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t3(void *arg) { + global++; // NORACE + return NULL; +} + +void *t2(void *arg) { // t2 is protected by mutex locked in main thread + pthread_create(&id3, NULL, t3, NULL); + pthread_join(id3, NULL); + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + pthread_join(id2, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/53-races-mhp/13-both_inter_threaded_lockset_transitive_racefree.c b/tests/regression/53-races-mhp/13-both_inter_threaded_lockset_transitive_racefree.c new file mode 100644 index 0000000000..84bd4a28a3 --- /dev/null +++ b/tests/regression/53-races-mhp/13-both_inter_threaded_lockset_transitive_racefree.c @@ -0,0 +1,45 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id_main_child, id_main_grand_child, id_1, id_1_child, id_1_grand_child; + +void *t1_grand_child_fun(void *arg) { // t1_grand_child is protected by mutex locked in t1 + global++; // NORACE + return NULL; +} + +void *t1_child_fun(void *arg) { + pthread_create(&id_1_grand_child, NULL, t1_grand_child_fun, NULL); + pthread_join(id_1_grand_child, NULL); + return NULL; +} + +void *t1_fun(void *arg) { + pthread_mutex_lock(&mutex); + pthread_create(&id_1_child, NULL, t1_child_fun, NULL); + pthread_join(id_1_child, NULL); + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *tmain_grand_child_fun(void *arg) { // tmain_grand_child is protected by mutex locked in main + global++; // NORACE + return NULL; +} + +void *tmain_child_fun(void *arg) { + pthread_create(&id_main_grand_child, NULL, tmain_grand_child_fun, NULL); + pthread_join(id_main_grand_child, NULL); + return NULL; +} + +int main(void) { + pthread_create(&id_1, NULL, t1_fun, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id_main_child, NULL, tmain_child_fun, NULL); + pthread_join(id_main_child, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/53-races-mhp/14-never_unlock_never_join_racefree.c b/tests/regression/53-races-mhp/14-never_unlock_never_join_racefree.c new file mode 100644 index 0000000000..1b40568852 --- /dev/null +++ b/tests/regression/53-races-mhp/14-never_unlock_never_join_racefree.c @@ -0,0 +1,25 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // NORACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is protected by mutex locked in main thread + global++; // NORACE + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/53-races-mhp/15-maybe_create_racefree.c b/tests/regression/53-races-mhp/15-maybe_create_racefree.c new file mode 100644 index 0000000000..d230a21902 --- /dev/null +++ b/tests/regression/53-races-mhp/15-maybe_create_racefree.c @@ -0,0 +1,28 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // NORACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is protected by mutex locked in main thread + global++; // NORACE + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + int maybe; + if (maybe) { + pthread_create(&id2, NULL, t2, NULL); + } + return 0; +} \ No newline at end of file diff --git a/tests/regression/53-races-mhp/16-convoluted_racefree.c b/tests/regression/53-races-mhp/16-convoluted_racefree.c new file mode 100644 index 0000000000..66d9f011c7 --- /dev/null +++ b/tests/regression/53-races-mhp/16-convoluted_racefree.c @@ -0,0 +1,38 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER, mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2, id3; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // NORACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t3(void *arg) { + global++; // NORACE + return NULL; +} + +void *t2(void *arg) { // t2 is protected by mutex locked in main thread + pthread_create(&id3, NULL, t3, NULL); + pthread_mutex_lock(&mutex); // irrelevant lock/unlock + pthread_mutex_unlock(&mutex); + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); // lock and unlock mutex before creation + pthread_mutex_unlock(&mutex); + pthread_mutex_lock(&mutex); + pthread_mutex_lock(&mutex1); + pthread_create(&id2, NULL, t2, NULL); + pthread_mutex_unlock(&mutex1); // unlock unrelated mutex before joining + pthread_join(id3, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/53-races-mhp/20-maybe_lock_racing.c b/tests/regression/53-races-mhp/20-maybe_lock_racing.c new file mode 100644 index 0000000000..2d4aed06e3 --- /dev/null +++ b/tests/regression/53-races-mhp/20-maybe_lock_racing.c @@ -0,0 +1,28 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since the mutex does not have to be locked during creation + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + int maybe; + if (maybe) { + pthread_mutex_lock(&mutex); + } + pthread_create(&id2, NULL, t2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/53-races-mhp/21-maybe_unlock_racing.c b/tests/regression/53-races-mhp/21-maybe_unlock_racing.c new file mode 100644 index 0000000000..4845e2fbfb --- /dev/null +++ b/tests/regression/53-races-mhp/21-maybe_unlock_racing.c @@ -0,0 +1,30 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since an unlock may happen before joining + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + int maybe; + if (maybe) { + pthread_mutex_unlock(&mutex); + } + pthread_join(id2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/53-races-mhp/22-random_mutex_unlock_racing.c b/tests/regression/53-races-mhp/22-random_mutex_unlock_racing.c new file mode 100644 index 0000000000..93c1d49657 --- /dev/null +++ b/tests/regression/53-races-mhp/22-random_mutex_unlock_racing.c @@ -0,0 +1,33 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER, mutex_alt = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since an unlock may happen before joining + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + pthread_mutex_lock(&mutex_alt); + pthread_mutex_t *mutex_ref = &mutex_alt; + int maybe; + if (maybe) { + mutex_ref = &mutex; + } + pthread_mutex_unlock(mutex_ref); + pthread_join(id2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/53-races-mhp/23-unknown_mutex_unlock_racing.c b/tests/regression/53-races-mhp/23-unknown_mutex_unlock_racing.c new file mode 100644 index 0000000000..0560e5bfe0 --- /dev/null +++ b/tests/regression/53-races-mhp/23-unknown_mutex_unlock_racing.c @@ -0,0 +1,28 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since an unlock could happen before joining + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + pthread_mutex_t *mutex_ref; + pthread_mutex_unlock(mutex_ref); // unlock of unknown mutex + pthread_join(id2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/53-races-mhp/24-maybe_join_racing.c b/tests/regression/53-races-mhp/24-maybe_join_racing.c new file mode 100644 index 0000000000..0f34d5c7c4 --- /dev/null +++ b/tests/regression/53-races-mhp/24-maybe_join_racing.c @@ -0,0 +1,30 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, joining may happen before unlocking + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + int maybe; + if (maybe) { + pthread_join(id2, NULL); + } + pthread_mutex_unlock(&mutex); + return 0; +} \ No newline at end of file diff --git a/tests/regression/53-races-mhp/25-lock_from_same_thread_one_lockset_one_interthreaded_racing.c b/tests/regression/53-races-mhp/25-lock_from_same_thread_one_lockset_one_interthreaded_racing.c new file mode 100644 index 0000000000..1d2b39cea9 --- /dev/null +++ b/tests/regression/53-races-mhp/25-lock_from_same_thread_one_lockset_one_interthreaded_racing.c @@ -0,0 +1,22 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1; + +// both accesses are protected by same mutex **locked in same thread** + +void *t1(void *arg) { + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_mutex_lock(&mutex); + pthread_create(&id1, NULL, t1, NULL); + global++; // RACE! + pthread_join(id1, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/53-races-mhp/26-lock_from_same_thread_both_interthreaded_racing.c b/tests/regression/53-races-mhp/26-lock_from_same_thread_both_interthreaded_racing.c new file mode 100644 index 0000000000..8b9409c80c --- /dev/null +++ b/tests/regression/53-races-mhp/26-lock_from_same_thread_both_interthreaded_racing.c @@ -0,0 +1,23 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +// both accesses are protected by same mutex **locked in same thread** + +void *tc(void *arg) { + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_mutex_lock(&mutex); + pthread_create(&id1, NULL, tc, NULL); + pthread_create(&id2, NULL, tc, NULL); + pthread_join(id1, NULL); + pthread_join(id2, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/53-races-mhp/27-ambiguous_context_racing.c b/tests/regression/53-races-mhp/27-ambiguous_context_racing.c new file mode 100644 index 0000000000..86eba5ba19 --- /dev/null +++ b/tests/regression/53-races-mhp/27-ambiguous_context_racing.c @@ -0,0 +1,36 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { + global++; // RACE! + return NULL; +} + +void evil(int x) { + if (x) { + pthread_mutex_lock(&mutex); + } + pthread_create(&id2, NULL, t2, NULL); +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + int maybe; + if (maybe) { + evil(0); + } else { + evil(1); + } + return 0; +} diff --git a/tests/regression/53-races-mhp/30-multiple_create_statements_racing.c b/tests/regression/53-races-mhp/30-multiple_create_statements_racing.c new file mode 100644 index 0000000000..2182060661 --- /dev/null +++ b/tests/regression/53-races-mhp/30-multiple_create_statements_racing.c @@ -0,0 +1,29 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since it is created/joined twice. The lock is released before the second join happens + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + pthread_join(id2, NULL); + pthread_create(&id2, NULL, t2, NULL); + pthread_mutex_unlock(&mutex); + pthread_join(id2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/53-races-mhp/31-diamond_racing.c b/tests/regression/53-races-mhp/31-diamond_racing.c new file mode 100644 index 0000000000..639c50f192 --- /dev/null +++ b/tests/regression/53-races-mhp/31-diamond_racing.c @@ -0,0 +1,39 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2, id3, id4_1, id4_2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t4(void *arg) { // t4 is not protected by mutex, since it is created twice and the creation in t2 does not happen with mutex locked + global++; // RACE! + return NULL; +} + +void *t3(void *arg) { + pthread_mutex_lock(&mutex); + pthread_create(&id4_2, NULL, t4, NULL); + pthread_join(id4_2, NULL); + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { + pthread_create(&id4_1, NULL, t4, NULL); + pthread_join(id4_1, NULL); + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_create(&id2, NULL, t2, NULL); + pthread_create(&id3, NULL, t3, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/53-races-mhp/32-cycle_racing.c b/tests/regression/53-races-mhp/32-cycle_racing.c new file mode 100644 index 0000000000..8873798d87 --- /dev/null +++ b/tests/regression/53-races-mhp/32-cycle_racing.c @@ -0,0 +1,39 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +// This program does not make any sense in practice (it produces a deadlock and if it did not, it wouldn't halt) +// We solely want to assert that the accesses to global race + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, idc1; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *tc1(void *arg); + +void *tc2(void *arg) { + pthread_t idc1; + pthread_mutex_lock(&mutex); + pthread_create(&idc1, NULL, tc1, NULL); + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *tc1(void *arg) { // tc1 is protected by tc2, but not by the main thread. + global++; // RACE! + pthread_t idc2; + pthread_create(&idc2, NULL, tc2, NULL); + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_create(&idc1, NULL, tc1, NULL); + return 0; +} \ No newline at end of file