From 94ed26dc4ff9046f31edcf99d428a95c5df28b05 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 20 Jan 2022 15:59:19 +0200 Subject: [PATCH 1/3] Add race test where all accesses don't race --- .../53-races-mhp/03-not-created_rc.c | 29 +++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 tests/regression/53-races-mhp/03-not-created_rc.c diff --git a/tests/regression/53-races-mhp/03-not-created_rc.c b/tests/regression/53-races-mhp/03-not-created_rc.c new file mode 100644 index 0000000000..d746f14419 --- /dev/null +++ b/tests/regression/53-races-mhp/03-not-created_rc.c @@ -0,0 +1,29 @@ +#include +#include + +int myglobal; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + return NULL; +} + +void *t_fun2(void *arg) { + pthread_mutex_lock(&mutex1); + myglobal=myglobal+1; // RACE! + pthread_mutex_unlock(&mutex1); + return NULL; +} + +int main(void) { + pthread_t id, id2; + pthread_create(&id, NULL, t_fun, NULL); // enter multithreaded + myglobal = 5; // NORACE + + pthread_create(&id2, NULL, t_fun2, NULL); + pthread_mutex_lock(&mutex2); + myglobal=myglobal+1; // RACE! + pthread_mutex_unlock(&mutex2); + return 0; +} From 309cd2b1e9cd5fd5ea9b3104138ae1de99002f58 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 20 Jan 2022 16:05:05 +0200 Subject: [PATCH 2/3] Filter non-racing accesses of racing variable --- src/domains/access.ml | 53 +++++++++++++++++++++++++++---------------- 1 file changed, 34 insertions(+), 19 deletions(-) diff --git a/src/domains/access.ml b/src/domains/access.ml index 50047222a1..73d3fada5b 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -333,8 +333,16 @@ struct let pretty = pretty end ) + + let conf (conf, _, _, _, _) = conf +end +module AS = +struct + include SetDomain.Make (A) + + let max_conf accs = + accs |> elements |> List.map A.conf |> List.max end -module AS = SetDomain.Make (A) module T = struct include Printable.Std @@ -377,28 +385,34 @@ module LVOpt = Printable.Option (LV) (struct let name = "NONE" end) (* Check if two accesses may race and if yes with which confidence *) let may_race (conf,w,loc,e,a) (conf2,w2,loc2,e2,a2) = if not w && not w2 then - None (* two read/read accesses do not race *) + false (* two read/read accesses do not race *) else if not (MCPAccess.A.may_race a a2) then - None (* analysis-specific information excludes race *) + false (* analysis-specific information excludes race *) else - Some (max conf conf2) + true -let check_safe accs = +let filter_may_race accs = let accs = AS.elements accs in let cart = List.cartesian_product accs accs in - let conf = List.filter_map (fun (x,y) -> if A.compare x y <= 0 then may_race x y else None) cart in - if conf = [] then - None - else - let maxconf = List.max conf in - Some maxconf + List.fold_left (fun acc (x, y) -> + if A.compare x y <= 0 && may_race x y then + AS.add y (AS.add x acc) + else + acc + ) (AS.empty ()) cart let is_all_safe = ref true (* Commenting your code is for the WEAK! *) let incr_summary safe vulnerable unsafe (lv, ty) accs = (* ignore(printf "Checking safety of %a:\n" d_memo (ty,lv)); *) - let safety = check_safe accs in + let race_accs = filter_may_race accs in + let safety = + if AS.is_empty race_accs then + None + else + Some (AS.max_conf race_accs) + in match safety with | None -> incr safe | Some n when n >= 100 -> is_all_safe := false; incr unsafe @@ -407,7 +421,7 @@ let incr_summary safe vulnerable unsafe (lv, ty) accs = let print_accesses (lv, ty) accs = let allglobs = get_bool "allglobs" in let debug = get_bool "dbg.debug" in - let msgs () = + let msgs race_accs = let h (conf,w,loc,e,a) = let atyp = if w then "write" else "read" in let d_msg () = dprintf "%s with %a (conf. %d)" atyp MCPAccess.A.pretty a conf in @@ -419,12 +433,13 @@ let print_accesses (lv, ty) accs = in (doc, Some loc) in - AS.elements accs + AS.elements race_accs |> List.map h in - match check_safe accs with - | None -> + match filter_may_race accs with + | race_accs when AS.is_empty race_accs -> if allglobs then - M.msg_group Success ~category:Race "Memory location %a (safe)" d_memo (ty,lv) (msgs ()) - | Some n -> - M.msg_group Warning ~category:Race "Memory location %a (race with conf. %d)" d_memo (ty,lv) n (msgs ()) + M.msg_group Success ~category:Race "Memory location %a (safe)" d_memo (ty,lv) (msgs accs) + | race_accs -> + let conf = AS.max_conf race_accs in + M.msg_group Warning ~category:Race "Memory location %a (race with conf. %d)" d_memo (ty,lv) conf (msgs (if allglobs then accs else race_accs)) From 814cd1127477753ac8b400ace879648ba0cc39a7 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 20 Jan 2022 16:06:32 +0200 Subject: [PATCH 3/3] Update test race annotations for filtered accesses --- tests/regression/04-mutex/27-base_rc.c | 2 +- tests/regression/04-mutex/35-trylock_rc.c | 2 +- tests/regression/10-synch/12-join_rc.c | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/regression/04-mutex/27-base_rc.c b/tests/regression/04-mutex/27-base_rc.c index 0c931c4c24..1bf243b5f8 100644 --- a/tests/regression/04-mutex/27-base_rc.c +++ b/tests/regression/04-mutex/27-base_rc.c @@ -9,7 +9,7 @@ void bad() { } void good() { pthread_mutex_lock(&gm); - global++; // RACE + global++; // NORACE (MHP) pthread_mutex_unlock(&gm); } diff --git a/tests/regression/04-mutex/35-trylock_rc.c b/tests/regression/04-mutex/35-trylock_rc.c index a56620ac66..5956a7345d 100644 --- a/tests/regression/04-mutex/35-trylock_rc.c +++ b/tests/regression/04-mutex/35-trylock_rc.c @@ -49,7 +49,7 @@ void *monitor_thread (void *arg) { if (status != EBUSY) { if (status != 0) err_abort (status, "Trylock mutex"); - printf ("Counter is %ld\n", counter/SPIN); // RACE + printf ("Counter is %ld\n", counter/SPIN); // NORACE (MHP) status = pthread_mutex_unlock (&mutex); if (status != 0) err_abort (status, "Unlock mutex"); diff --git a/tests/regression/10-synch/12-join_rc.c b/tests/regression/10-synch/12-join_rc.c index 62a3a035ff..3cfc07fc5d 100644 --- a/tests/regression/10-synch/12-join_rc.c +++ b/tests/regression/10-synch/12-join_rc.c @@ -18,7 +18,7 @@ int main(void) { for (i=0; i<10; i++) pthread_create(&id[i], NULL, t_fun, NULL); pthread_mutex_lock(&mutex); - myglobal=myglobal+1; // RACE + myglobal=myglobal+1; // NORACE (MHP) pthread_mutex_unlock(&mutex); for (i=0; i<9; i++) pthread_join(id[i], NULL);