From 31323cd214123f40f3eac63a33a72298a84d2c73 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 30 Jan 2025 10:53:48 +0100 Subject: [PATCH 1/6] Add switch to not use mutexes in race detection --- src/analyses/mutexAnalysis.ml | 2 ++ src/config/options.schema.json | 13 +++++++++++++ 2 files changed, 15 insertions(+) diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index c712ca9644..996eca9954 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -267,6 +267,8 @@ struct include MustLocksetRW let name () = "lock" let may_race ls1 ls2 = + let use_lockset = GobConfig.get_bool "ana.race.digests.lockset" in + (not use_lockset) || (* not mutually exclusive *) not @@ exists (fun ((m1, w1) as l1) -> if w1 then diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 39c863ad49..a2aa7b8feb 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1105,6 +1105,19 @@ "description": "Report races for volatile variables.", "type": "boolean", "default": true + }, + "digests": { + "title": "ana.race.digests", + "type" : "object", + "properties" : { + "lockset" : { + "title": "ana.race.digests.lockset", + "description": "Use lockset digest for excluding data races.", + "type" : "boolean", + "default" : true + } + }, + "additionalProperties": false } }, "additionalProperties": false From d9bd9cadaec38dbe6f5b5a75d767864a968a2fbe Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 30 Jan 2025 11:28:50 +0100 Subject: [PATCH 2/6] Add option to disable thread digest --- src/analyses/threadId.ml | 5 ++++- src/config/options.schema.json | 6 ++++++ 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml index 53d070a056..d9724b2c2e 100644 --- a/src/analyses/threadId.ml +++ b/src/analyses/threadId.ml @@ -132,7 +132,10 @@ struct struct include Printable.Option (ThreadLifted) (struct let name = "nonunique" end) let name () = "thread" - let may_race (t1: t) (t2: t) = match t1, t2 with + let may_race (t1: t) (t2: t) = + let use_tid = GobConfig.get_bool "ana.race.digests.thread" in + (not use_tid) || + match t1, t2 with | Some t1, Some t2 when ThreadLifted.equal t1 t2 -> false (* only unique threads *) | _, _ -> true let should_print = Option.is_some diff --git a/src/config/options.schema.json b/src/config/options.schema.json index a2aa7b8feb..ecda257c92 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1115,6 +1115,12 @@ "description": "Use lockset digest for excluding data races.", "type" : "boolean", "default" : true + }, + "thread" : { + "title": "ana.race.digests.thread", + "description": "TODO! How does relate to the MHP one? Seems to hit only in one case", + "type" : "boolean", + "default" : true } }, "additionalProperties": false From 164e0c9ec341129755ffd644122592e9812bca84 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 30 Jan 2025 11:42:51 +0100 Subject: [PATCH 3/6] Add option for freshness --- src/analyses/mallocFresh.ml | 4 +++- src/config/options.schema.json | 6 ++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml index c226d7e6ce..4e7bd84571 100644 --- a/src/analyses/mallocFresh.ml +++ b/src/analyses/mallocFresh.ml @@ -64,7 +64,9 @@ struct struct include BoolDomain.Bool let name () = "fresh" - let may_race f1 f2 = not (f1 || f2) + let may_race f1 f2 = + let use_fresh = GobConfig.get_bool "ana.race.digests.fresh" in + (not use_fresh) || not (f1 || f2) let should_print f = f end let access man (a: Queries.access) = diff --git a/src/config/options.schema.json b/src/config/options.schema.json index ecda257c92..07d6bf974f 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1121,6 +1121,12 @@ "description": "TODO! How does relate to the MHP one? Seems to hit only in one case", "type" : "boolean", "default" : true + }, + "fresh" : { + "title": "ana.race.digests.fresh", + "description": "Use freshness analysis for excluding data races.", + "type" : "boolean", + "default" : true } }, "additionalProperties": false From 7ae5e0798b650160e46c9e209f3d98f0e875b4bc Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 30 Jan 2025 11:47:41 +0100 Subject: [PATCH 4/6] Add toggle for region / symbLocks --- src/analyses/region.ml | 5 ++++- src/analyses/symbLocks.ml | 4 +++- src/config/options.schema.json | 12 ++++++++++++ 3 files changed, 19 insertions(+), 2 deletions(-) diff --git a/src/analyses/region.ml b/src/analyses/region.ml index 0fb61059e2..d02df20d0d 100644 --- a/src/analyses/region.ml +++ b/src/analyses/region.ml @@ -64,7 +64,10 @@ struct struct include Printable.Option (Lvals) (struct let name = "no region" end) let name () = "region" - let may_race r1 r2 = match r1, r2 with + let may_race r1 r2 = + let use_region = GobConfig.get_bool "ana.race.digests.region" in + (not use_region) || + match r1, r2 with | None, _ | _, None -> false (* TODO: Should it happen in the first place that RegMap has empty value? Happens in 09-regions/34-escape_rc *) diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml index 0850fac317..9cf212b6b9 100644 --- a/src/analyses/symbLocks.ml +++ b/src/analyses/symbLocks.ml @@ -121,7 +121,9 @@ struct include SetDomain.Make (E) let name () = "symblock" - let may_race lp lp2 = disjoint lp lp2 + let may_race lp lp2 = + let use_symblocks = GobConfig.get_bool "ana.race.digests.symb_locks" in + (not use_symblocks) || disjoint lp lp2 let should_print lp = not (is_empty lp) end diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 07d6bf974f..e27e89ab92 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1127,6 +1127,18 @@ "description": "Use freshness analysis for excluding data races.", "type" : "boolean", "default" : true + }, + "region" : { + "title": "ana.race.digests.region", + "description": "Use region analysis for excluding data races.", + "type" : "boolean", + "default" : true + }, + "symb_locks" : { + "title": "ana.race.digests.symb_locks", + "description": "Use symb_locks analysis for excluding data races.", + "type" : "boolean", + "default" : true } }, "additionalProperties": false From 1273af27c33c1e42a7707c543df00e789ad6fb8d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 31 Jan 2025 14:10:38 +0100 Subject: [PATCH 5/6] Thread flag option --- src/analyses/threadFlag.ml | 4 +++- src/config/options.schema.json | 6 ++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml index 1e0ff7db9f..454ea28961 100644 --- a/src/analyses/threadFlag.ml +++ b/src/analyses/threadFlag.ml @@ -56,7 +56,9 @@ struct struct include BoolDomain.Bool let name () = "multi" - let may_race m1 m2 = m1 && m2 (* kill access when single threaded *) + let may_race m1 m2 = + let use_threadflag = GobConfig.get_bool "ana.race.digests.threadflag" in + (not use_threadflag) || (m1 && m2) (* kill access when single threaded *) let should_print m = not m end let access man _ = diff --git a/src/config/options.schema.json b/src/config/options.schema.json index e27e89ab92..808f11eaa8 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1139,6 +1139,12 @@ "description": "Use symb_locks analysis for excluding data races.", "type" : "boolean", "default" : true + }, + "threadflag" : { + "title": "ana.race.digests.threadflag", + "description": "Use threadflag analysis for excluding data races.", + "type" : "boolean", + "default" : true } }, "additionalProperties": false From aa976793a9b847521a204f9ce05ffa13a96f45a6 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 31 Jan 2025 14:16:51 +0100 Subject: [PATCH 6/6] Add `tid` and `joins` digest --- src/cdomains/mHP.ml | 12 +++++++----- src/config/options.schema.json | 12 ++++++++++++ 2 files changed, 19 insertions(+), 5 deletions(-) diff --git a/src/cdomains/mHP.ml b/src/cdomains/mHP.ml index afaf6d67e3..18aa1719fd 100644 --- a/src/cdomains/mHP.ml +++ b/src/cdomains/mHP.ml @@ -77,17 +77,19 @@ let must_be_joined other joined = (** May two program points with respective MHP information happen in parallel *) let may_happen_in_parallel one two = - let {tid=tid; created=created; must_joined=must_joined} = one in + let use_tid = GobConfig.get_bool "ana.race.digests.tid" in + let use_join = GobConfig.get_bool "ana.race.digests.join" in + let {tid; created; must_joined} = one in let {tid=tid2; created=created2; must_joined=must_joined2} = two in match tid,tid2 with | `Lifted tid, `Lifted tid2 -> - if (TID.is_unique tid) && (TID.equal tid tid2) then + if use_tid && (TID.is_unique tid) && (TID.equal tid tid2) then false - else if definitely_not_started (tid,created) tid2 || definitely_not_started (tid2,created2) tid then + else if use_tid && (definitely_not_started (tid,created) tid2 || definitely_not_started (tid2,created2) tid) then false - else if must_be_joined tid2 must_joined || must_be_joined tid must_joined2 then + else if use_tid && use_join && (must_be_joined tid2 must_joined || must_be_joined tid must_joined2) then false - else if exists_definitely_not_started_in_joined (tid,created) must_joined2 || exists_definitely_not_started_in_joined (tid2,created2) must_joined then + else if use_tid && use_join && (exists_definitely_not_started_in_joined (tid,created) must_joined2 || exists_definitely_not_started_in_joined (tid2,created2) must_joined) then false else true diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 808f11eaa8..6bcab0d253 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1145,6 +1145,18 @@ "description": "Use threadflag analysis for excluding data races.", "type" : "boolean", "default" : true + }, + "tid" : { + "title": "ana.race.digests.tid", + "description": "Use tid analysis for excluding data races.", + "type" : "boolean", + "default" : true + }, + "join" : { + "title": "ana.race.digests.join", + "description": "Use join analysis for excluding data races.", + "type" : "boolean", + "default" : true } }, "additionalProperties": false