diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml index 2f2a1bb0fb..56c615aa53 100644 --- a/src/analyses/pthreadBarriers.ml +++ b/src/analyses/pthreadBarriers.ml @@ -22,7 +22,20 @@ struct module V = VarinfoV module TID = ThreadIdDomain.Thread - module Waiters = SetDomain.ToppedSet (MHP) (struct let topname = "All MHP" end) + + module MHPplusLock = struct + module Locks = LockDomain.MustLockset + + include Printable.Prod (MHP) (Locks) + let name () = "MHPplusLock" + + let mhp (mhp1, l1) (mhp2, l2) = + MHP.may_happen_in_parallel mhp1 mhp2 && Locks.is_empty (Locks.inter l1 l2) + + let may_be_non_unique_thread (mhp, _) = MHP.may_be_non_unique_thread mhp + end + + module Waiters = SetDomain.ToppedSet (MHPplusLock) (struct let topname = "All MHP" end) module Multiprocess = BoolDomain.MayBool module G = Lattice.Prod3 (Multiprocess) (Capacity) (Waiters) @@ -43,15 +56,16 @@ struct let barriers = possible_vinfos ask barrier in let mhp = MHP.current ask in let handle_one b = - man.sideg b (Multiprocess.bot (), Capacity.bot (), Waiters.singleton mhp); + let locks = man.ask (Queries.MustLockset) in + man.sideg b (Multiprocess.bot (), Capacity.bot (), Waiters.singleton (mhp, locks)); let addr = ValueDomain.Addr.of_var b in let (multiprocess,capacity, waiters) = man.global b in let may_run = if multiprocess then true else - let relevant_waiters = Waiters.filter (fun other -> MHP.may_happen_in_parallel mhp other) waiters in - if Waiters.exists MHP.may_be_non_unique_thread relevant_waiters then + let relevant_waiters = Waiters.filter (fun other -> MHPplusLock.mhp (mhp, locks) other) waiters in + if Waiters.exists MHPplusLock.may_be_non_unique_thread relevant_waiters then true else let count = Waiters.cardinal relevant_waiters in @@ -61,7 +75,7 @@ struct let min_cap = (BatOption.default Z.zero (Capacity.I.minimal c)) in if Z.leq min_cap Z.one then true - else if min_cap = Z.of_int 2 && count = 1 then + else if min_cap = Z.of_int 2 && count >= 1 then true else if Z.geq (Z.of_int (count + 1)) min_cap then (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that @@ -73,7 +87,7 @@ struct let candidates = BatList.n_cartesian_product lists in List.exists (fun candidate -> let pairwise = BatList.cartesian_product candidate candidate in - List.for_all (fun (a,b) -> MHP.may_happen_in_parallel a b) pairwise + List.for_all (fun (a,b) -> MHPplusLock.mhp a b) pairwise ) candidates else false diff --git a/tests/regression/82-barrier/07-lockset.c b/tests/regression/82-barrier/07-lockset.c new file mode 100644 index 0000000000..d1c68f3d7f --- /dev/null +++ b/tests/regression/82-barrier/07-lockset.c @@ -0,0 +1,39 @@ +// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers' +#include +#include +#include + +int g; + +pthread_barrier_t barrier; +pthread_mutex_t mutex; + +void* f1(void* ptr) { + pthread_mutex_lock(&mutex); + pthread_barrier_wait(&barrier); + pthread_mutex_unlock(&mutex); + return NULL; +} + +int main(int argc, char const *argv[]) +{ + int top; + int i = 0; + + pthread_barrier_init(&barrier, NULL, 2); + + pthread_t t1; + pthread_create(&t1,NULL,f1,NULL); + + if(top) { + pthread_mutex_lock(&mutex); + pthread_barrier_wait(&barrier); + // Deadlocks + pthread_mutex_unlock(&mutex); + i = 1; + } + + __goblint_check(i == 0); + + return 0; +} diff --git a/tests/regression/82-barrier/08-lockset-more.c b/tests/regression/82-barrier/08-lockset-more.c new file mode 100644 index 0000000000..a33ecc1a78 --- /dev/null +++ b/tests/regression/82-barrier/08-lockset-more.c @@ -0,0 +1,47 @@ +// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers' +#include +#include +#include + +int g; + +pthread_barrier_t barrier; +pthread_mutex_t mutex; + +void* f1(void* ptr) { + pthread_mutex_lock(&mutex); + pthread_barrier_wait(&barrier); + pthread_mutex_unlock(&mutex); + return NULL; +} + +void* f2(void* ptr) { + pthread_mutex_lock(&mutex); + pthread_barrier_wait(&barrier); + pthread_mutex_unlock(&mutex); + return NULL; +} + +int main(int argc, char const *argv[]) +{ + int top; + int i = 0; + + pthread_barrier_init(&barrier, NULL, 2); + + pthread_t t1; + pthread_create(&t1,NULL,f1,NULL); + + pthread_t t2; + pthread_create(&t2,NULL,f2,NULL); + + + if(top) { + pthread_barrier_wait(&barrier); + i = 1; + } + + __goblint_check(i == 0); //UNKNOWN! + + return 0; +}