From e6277f83d7afbd29429fe52e77d4f2a72f79b652 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 1 Nov 2024 11:43:48 +0200 Subject: [PATCH 1/4] =?UTF-8?q?Add=20test=20to=20show=20that=20our=20Min?= =?UTF-8?q?=C3=A9=20with=20W=20should=20partition=20it=20by=20lockset?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../13-privatized/95-mine-W-part-by-S.c | 32 ++++++ .../13-privatized/95-mine-W-part-by-S.t | 99 +++++++++++++++++++ 2 files changed, 131 insertions(+) create mode 100644 tests/regression/13-privatized/95-mine-W-part-by-S.c create mode 100644 tests/regression/13-privatized/95-mine-W-part-by-S.t diff --git a/tests/regression/13-privatized/95-mine-W-part-by-S.c b/tests/regression/13-privatized/95-mine-W-part-by-S.c new file mode 100644 index 0000000000..610fd475e7 --- /dev/null +++ b/tests/regression/13-privatized/95-mine-W-part-by-S.c @@ -0,0 +1,32 @@ +// PARAM: --set ana.base.privatization mine-W +#include +#include + +int g, h; +pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t B = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + pthread_mutex_lock(&A); + g = 5; + pthread_mutex_unlock(&A); + + pthread_mutex_lock(&B); + // __goblint_check(g == 5); // UNKNOWN! (data race, so weak read) + h = 6; + pthread_mutex_unlock(&B); + return NULL; +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + pthread_mutex_lock(&A); + g = 8; + pthread_mutex_lock(&B); + __goblint_check(g == 8); + pthread_mutex_unlock(&B); + pthread_mutex_unlock(&A); + return 0; +} diff --git a/tests/regression/13-privatized/95-mine-W-part-by-S.t b/tests/regression/13-privatized/95-mine-W-part-by-S.t new file mode 100644 index 0000000000..8a13d5b957 --- /dev/null +++ b/tests/regression/13-privatized/95-mine-W-part-by-S.t @@ -0,0 +1,99 @@ +Miné succeeds: + + $ goblint --set ana.base.privatization mine 95-mine-W-part-by-S.c + [Success][Assert] Assertion "g == 8" will succeed (95-mine-W-part-by-S.c:28:3-28:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 17 + dead: 0 + total lines: 17 + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 0 + total memory locations: 2 + +Miné without thread IDs even succeeds: + + $ goblint --set ana.base.privatization mine-nothread 95-mine-W-part-by-S.c + [Success][Assert] Assertion "g == 8" will succeed (95-mine-W-part-by-S.c:28:3-28:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 17 + dead: 0 + total lines: 17 + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 0 + total memory locations: 2 + +TODO: Our Miné with W should also succeed, but doesn't: + + $ goblint --set ana.base.privatization mine-W 95-mine-W-part-by-S.c + [Warning][Assert] Assertion "g == 8" is unknown. (95-mine-W-part-by-S.c:28:3-28:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 17 + dead: 0 + total lines: 17 + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 0 + total memory locations: 2 + +The noinit variant makes no difference: + + $ goblint --set ana.base.privatization mine-W-noinit 95-mine-W-part-by-S.c + [Warning][Assert] Assertion "g == 8" is unknown. (95-mine-W-part-by-S.c:28:3-28:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 17 + dead: 0 + total lines: 17 + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 0 + total memory locations: 2 + + + +Protection-Based succeeds: + + $ goblint --set ana.base.privatization protection 95-mine-W-part-by-S.c + [Success][Assert] Assertion "g == 8" will succeed (95-mine-W-part-by-S.c:28:3-28:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 17 + dead: 0 + total lines: 17 + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 0 + total memory locations: 2 + +Write-Centered succeeds: + + $ goblint --set ana.base.privatization write 95-mine-W-part-by-S.c + [Success][Assert] Assertion "g == 8" will succeed (95-mine-W-part-by-S.c:28:3-28:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 17 + dead: 0 + total lines: 17 + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 0 + total memory locations: 2 + +TODO Lock-Centered should also succeed, but doesn't: + + $ goblint --set ana.base.privatization lock 95-mine-W-part-by-S.c + [Warning][Assert] Assertion "g == 8" is unknown. (95-mine-W-part-by-S.c:28:3-28:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 17 + dead: 0 + total lines: 17 + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 0 + total memory locations: 2 From 8197c184b8d54e9f9745f81a50130b32d80bbaac Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 1 Nov 2024 12:00:35 +0200 Subject: [PATCH 2/4] Partition mine-W W set by lockset --- src/analyses/basePriv.ml | 17 ++++++++++++----- .../13-privatized/95-mine-W-part-by-S.c | 2 +- .../13-privatized/95-mine-W-part-by-S.t | 6 +++--- 3 files changed, 16 insertions(+), 9 deletions(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 946b8f8cc5..0ff8ca5bee 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -1135,9 +1135,9 @@ struct include SetDomain.ToppedSet (Basetype.Variables) (struct let topname = "All variables" end) let name () = "W" end - module D = W + module D = MapDomain.MapBot (MustLockset) (W) - let startstate () = W.empty () + let startstate () = D.empty () let read_global ask getg (st: BaseComponents (D).t) x = let s = current_lockset ask in @@ -1154,7 +1154,7 @@ struct if not invariant && not (!earlyglobs && is_excluded_from_earlyglobs x) then sideg (V.global x) (G.create_weak (GWeak.singleton s v)); let w' = if not invariant then - W.add x st.priv + D.join st.priv (D.singleton s (W.singleton x)) else st.priv (* No need to add invariant to W because it doesn't matter for reads after invariant, only unlocks. *) in @@ -1173,7 +1173,14 @@ struct let unlock ask getg sideg (st: BaseComponents (D).t) m = let s = MustLockset.remove m (current_lockset ask) in - let is_in_W x _ = W.mem x st.priv in + let w = D.fold (fun s' w acc -> + if MustLockset.mem m s' then + W.join w acc + else + acc + ) st.priv (W.empty ()) + in + let is_in_W x _ = W.mem x w in let side_cpa = CPA.filter is_in_W st.cpa in sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa)); st @@ -1194,7 +1201,7 @@ struct CPA.fold (fun x v (st: BaseComponents (D).t) -> if is_global ask x then ( sideg (V.global x) (G.create_weak (GWeak.singleton (MustLockset.empty ()) v)); - {st with priv = W.add x st.priv} (* TODO: is this add necessary? *) + {st with priv = D.join st.priv (D.singleton (MustLockset.empty ()) (W.singleton x))} (* TODO: is this add necessary? *) ) else st diff --git a/tests/regression/13-privatized/95-mine-W-part-by-S.c b/tests/regression/13-privatized/95-mine-W-part-by-S.c index 610fd475e7..3c714f1d48 100644 --- a/tests/regression/13-privatized/95-mine-W-part-by-S.c +++ b/tests/regression/13-privatized/95-mine-W-part-by-S.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.base.privatization mine-W +// PARAM: --set ana.base.privatization mine-W-noinit #include #include diff --git a/tests/regression/13-privatized/95-mine-W-part-by-S.t b/tests/regression/13-privatized/95-mine-W-part-by-S.t index 8a13d5b957..a189d217ab 100644 --- a/tests/regression/13-privatized/95-mine-W-part-by-S.t +++ b/tests/regression/13-privatized/95-mine-W-part-by-S.t @@ -26,7 +26,7 @@ Miné without thread IDs even succeeds: unsafe: 0 total memory locations: 2 -TODO: Our Miné with W should also succeed, but doesn't: +Our Miné with W doesn't succeed with W partitioning due to initialization: $ goblint --set ana.base.privatization mine-W 95-mine-W-part-by-S.c [Warning][Assert] Assertion "g == 8" is unknown. (95-mine-W-part-by-S.c:28:3-28:26) @@ -40,10 +40,10 @@ TODO: Our Miné with W should also succeed, but doesn't: unsafe: 0 total memory locations: 2 -The noinit variant makes no difference: +But the noinit variant succeeds: $ goblint --set ana.base.privatization mine-W-noinit 95-mine-W-part-by-S.c - [Warning][Assert] Assertion "g == 8" is unknown. (95-mine-W-part-by-S.c:28:3-28:26) + [Success][Assert] Assertion "g == 8" will succeed (95-mine-W-part-by-S.c:28:3-28:26) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 17 dead: 0 From ba7ff17d68f23bae064533fd943a541f5d7987e1 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 1 Nov 2024 12:24:08 +0200 Subject: [PATCH 3/4] Try to fix lock privatization precision with a may-V map --- src/analyses/basePriv.ml | 31 ++++++++++++------- .../13-privatized/95-mine-W-part-by-S.t | 4 +-- 2 files changed, 22 insertions(+), 13 deletions(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 0ff8ca5bee..f5173b9445 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -1227,6 +1227,12 @@ struct let name () = "V" end + module DV2 = + struct + include MapDomain.MapBot_LiftTop (LockDomain.MustLock) (MayVars) + let name () = "V2" + end + module L = struct include MapDomain.MapBot_LiftTop (LockDomain.MustLock) (MinLocksets) @@ -1242,7 +1248,7 @@ struct open Locksets open LockCenteredD - module D = Lattice.Prod (DV) (L) + module D = Lattice.Prod3 (DV) (DV2) (L) module Wrapper = Wrapper (G) module UnwrappedG = G @@ -1251,7 +1257,7 @@ struct let invariant_global ask getg = invariant_global ask (Wrapper.getg ask getg) let invariant_vars ask getg = invariant_vars ask (Wrapper.getg ask getg) - let startstate () = (DV.bot (), L.bot ()) + let startstate () = (DV.bot (), DV2.bot (), L.bot ()) let lockset_init = MustLockset.all () @@ -1265,7 +1271,7 @@ struct let read_global ask getg (st: BaseComponents (D).t) x = let getg = Wrapper.getg ask getg in let s = current_lockset ask in - let (vv, l) = st.priv in + let (vv, vv2, l) = st.priv in let d_cpa = CPA.find x st.cpa in let d_sync = L.fold (fun m bs acc -> if not (MustVars.mem x (DV.find m vv)) then @@ -1309,10 +1315,11 @@ struct let sideg = Wrapper.sideg ask sideg in let getg = Wrapper.getg ask getg in let s = current_lockset ask in - let (vv, l) = st.priv in - let v' = L.fold (fun m _ acc -> - DV.add m (MustVars.add x (DV.find m acc)) acc - ) l vv + let (vv, vv2, l) = st.priv in + let (v', v2') = L.fold (fun m _ (acc1, acc2) -> + DV.add m (MustVars.add x (DV.find m acc1)) acc1, + DV2.add m (MayVars.add x (DV2.find m acc2)) acc2 + ) l (vv, vv2) in let cpa' = CPA.add x v st.cpa in if not invariant && not (!earlyglobs && is_excluded_from_earlyglobs x) then ( @@ -1320,20 +1327,22 @@ struct sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton s v)) (* Unlock after invariant will still side effect refined value from CPA, because cannot distinguish from non-invariant write. *) ); - {st with cpa = cpa'; priv = (v', l)} + {st with cpa = cpa'; priv = (v', v2', l)} let lock ask getg (st: BaseComponents (D).t) m = let s = current_lockset ask in - let (v, l) = st.priv in + let (v, v2, l) = st.priv in let v' = DV.add m (MustVars.empty ()) v in + let v2' = DV2.add m (MayVars.empty ()) v2 in let l' = L.add m (MinLocksets.singleton s) l in - {st with priv = (v', l')} + {st with priv = (v', v2', l')} let unlock ask getg sideg (st: BaseComponents (D).t) m = let sideg = Wrapper.sideg ask sideg in let getg = Wrapper.getg ask getg in let s = MustLockset.remove m (current_lockset ask) in - let is_in_G x _ = is_global ask x in + let (_, v2, _) = st.priv in + let is_in_G x _ = is_global ask x && MayVars.mem x (DV2.find m v2) in let side_cpa = CPA.filter is_in_G st.cpa in let side_cpa = CPA.mapi (fun x v -> let v = distr_init getg x v in diff --git a/tests/regression/13-privatized/95-mine-W-part-by-S.t b/tests/regression/13-privatized/95-mine-W-part-by-S.t index a189d217ab..4c23b13d91 100644 --- a/tests/regression/13-privatized/95-mine-W-part-by-S.t +++ b/tests/regression/13-privatized/95-mine-W-part-by-S.t @@ -84,10 +84,10 @@ Write-Centered succeeds: unsafe: 0 total memory locations: 2 -TODO Lock-Centered should also succeed, but doesn't: +Lock-Centered (with may-V) also succeeds: $ goblint --set ana.base.privatization lock 95-mine-W-part-by-S.c - [Warning][Assert] Assertion "g == 8" is unknown. (95-mine-W-part-by-S.c:28:3-28:26) + [Success][Assert] Assertion "g == 8" will succeed (95-mine-W-part-by-S.c:28:3-28:26) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 17 dead: 0 From d4478382c3e65fce99ed031f1d22968b902aeed5 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 27 Nov 2024 13:40:59 +0200 Subject: [PATCH 4/4] =?UTF-8?q?Partition=20W=20by=20m=20not=20S=20in=20Min?= =?UTF-8?q?=C3=A9's=20analysis?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/analyses/basePriv.ml | 68 ++++++++++++++++++---------------------- 1 file changed, 31 insertions(+), 37 deletions(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index f5173b9445..6d7fa6b8b9 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -956,6 +956,12 @@ struct (* weak: G -> (2^M -> D) *) (* sync: M -> (2^M -> (G -> D)) *) include AbstractLockCenteredBase (VD) (CPA) + + module W = + struct + include MapDomain.MapBot (LockDomain.MustLock) (MayVars) + let name () = "W" + end end module MinePrivBase = @@ -1130,14 +1136,9 @@ struct include LockCenteredBase open Locksets - module W = - struct - include SetDomain.ToppedSet (Basetype.Variables) (struct let topname = "All variables" end) - let name () = "W" - end - module D = MapDomain.MapBot (MustLockset) (W) + module D = W - let startstate () = D.empty () + let startstate () = W.empty () let read_global ask getg (st: BaseComponents (D).t) x = let s = current_lockset ask in @@ -1153,8 +1154,11 @@ struct let cpa' = CPA.add x v st.cpa in if not invariant && not (!earlyglobs && is_excluded_from_earlyglobs x) then sideg (V.global x) (G.create_weak (GWeak.singleton s v)); - let w' = if not invariant then - D.join st.priv (D.singleton s (W.singleton x)) + let w' = if not invariant then ( + MustLockset.fold (fun m acc -> + W.join acc (W.singleton m (MayVars.singleton x)) + ) s st.priv + ) else st.priv (* No need to add invariant to W because it doesn't matter for reads after invariant, only unlocks. *) in @@ -1169,18 +1173,13 @@ struct acc ) (G.sync (getg (V.mutex m))) st.cpa in + (* Could set W m to empty here (like Lock-Centered) but Miné doesn't and mentions this over-approximation. *) {st with cpa = cpa'} let unlock ask getg sideg (st: BaseComponents (D).t) m = let s = MustLockset.remove m (current_lockset ask) in - let w = D.fold (fun s' w acc -> - if MustLockset.mem m s' then - W.join w acc - else - acc - ) st.priv (W.empty ()) - in - let is_in_W x _ = W.mem x w in + let w = W.find m st.priv in + let is_in_W x _ = MayVars.mem x w in let side_cpa = CPA.filter is_in_W st.cpa in sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa)); st @@ -1201,7 +1200,7 @@ struct CPA.fold (fun x v (st: BaseComponents (D).t) -> if is_global ask x then ( sideg (V.global x) (G.create_weak (GWeak.singleton (MustLockset.empty ()) v)); - {st with priv = D.join st.priv (D.singleton (MustLockset.empty ()) (W.singleton x))} (* TODO: is this add necessary? *) + st ) else st @@ -1227,12 +1226,6 @@ struct let name () = "V" end - module DV2 = - struct - include MapDomain.MapBot_LiftTop (LockDomain.MustLock) (MayVars) - let name () = "V2" - end - module L = struct include MapDomain.MapBot_LiftTop (LockDomain.MustLock) (MinLocksets) @@ -1248,7 +1241,7 @@ struct open Locksets open LockCenteredD - module D = Lattice.Prod3 (DV) (DV2) (L) + module D = Lattice.Prod3 (DV) (W) (L) module Wrapper = Wrapper (G) module UnwrappedG = G @@ -1257,7 +1250,7 @@ struct let invariant_global ask getg = invariant_global ask (Wrapper.getg ask getg) let invariant_vars ask getg = invariant_vars ask (Wrapper.getg ask getg) - let startstate () = (DV.bot (), DV2.bot (), L.bot ()) + let startstate () = (DV.bot (), W.bot (), L.bot ()) let lockset_init = MustLockset.all () @@ -1271,7 +1264,7 @@ struct let read_global ask getg (st: BaseComponents (D).t) x = let getg = Wrapper.getg ask getg in let s = current_lockset ask in - let (vv, vv2, l) = st.priv in + let (vv, _, l) = st.priv in let d_cpa = CPA.find x st.cpa in let d_sync = L.fold (fun m bs acc -> if not (MustVars.mem x (DV.find m vv)) then @@ -1315,11 +1308,11 @@ struct let sideg = Wrapper.sideg ask sideg in let getg = Wrapper.getg ask getg in let s = current_lockset ask in - let (vv, vv2, l) = st.priv in - let (v', v2') = L.fold (fun m _ (acc1, acc2) -> + let (vv, w, l) = st.priv in + let (v', w') = L.fold (fun m _ (acc1, acc2) -> DV.add m (MustVars.add x (DV.find m acc1)) acc1, - DV2.add m (MayVars.add x (DV2.find m acc2)) acc2 - ) l (vv, vv2) + W.add m (MayVars.add x (W.find m acc2)) acc2 + ) l (vv, w) in let cpa' = CPA.add x v st.cpa in if not invariant && not (!earlyglobs && is_excluded_from_earlyglobs x) then ( @@ -1327,22 +1320,23 @@ struct sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton s v)) (* Unlock after invariant will still side effect refined value from CPA, because cannot distinguish from non-invariant write. *) ); - {st with cpa = cpa'; priv = (v', v2', l)} + {st with cpa = cpa'; priv = (v', w', l)} let lock ask getg (st: BaseComponents (D).t) m = let s = current_lockset ask in - let (v, v2, l) = st.priv in + let (v, w, l) = st.priv in let v' = DV.add m (MustVars.empty ()) v in - let v2' = DV2.add m (MayVars.empty ()) v2 in + let w' = W.add m (MayVars.empty ()) w in let l' = L.add m (MinLocksets.singleton s) l in - {st with priv = (v', v2', l')} + {st with priv = (v', w', l')} let unlock ask getg sideg (st: BaseComponents (D).t) m = let sideg = Wrapper.sideg ask sideg in let getg = Wrapper.getg ask getg in let s = MustLockset.remove m (current_lockset ask) in - let (_, v2, _) = st.priv in - let is_in_G x _ = is_global ask x && MayVars.mem x (DV2.find m v2) in + let (_, w, _) = st.priv in + let w = W.find m w in + let is_in_G x _ = is_global ask x && MayVars.mem x w in (* TODO: is_global check unnecessary? *) let side_cpa = CPA.filter is_in_G st.cpa in let side_cpa = CPA.mapi (fun x v -> let v = distr_init getg x v in