Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

mine-W privatization undermines Miné, lock is less precise than mine/protection #1613

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

mine-W privatization undermines Miné, lock is less precise than mine/protection #1613

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
e6277f8
Add test to show that our Miné with W should partition it by lockset
sim642 Nov 1, 2024
8197c18
Partition mine-W W set by lockset
sim642 Nov 1, 2024
ba7ff17
Try to fix lock privatization precision with a may-V map
sim642 Nov 1, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
48 changes: 32 additions & 16 deletions src/analyses/basePriv.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -1220,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)
Expand All @@ -1235,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
Expand All @@ -1244,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 ()

Expand All @@ -1258,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
Expand Down Expand Up @@ -1302,31 +1315,34 @@ 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 (
let v = distr_init getg x v in
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
Expand Down
32 changes: 32 additions & 0 deletions tests/regression/13-privatized/95-mine-W-part-by-S.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
// PARAM: --set ana.base.privatization mine-W-noinit
#include <pthread.h>
#include <goblint.h>

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;
}
99 changes: 99 additions & 0 deletions tests/regression/13-privatized/95-mine-W-part-by-S.t
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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

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)
[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

But the noinit variant succeeds:

$ goblint --set ana.base.privatization mine-W-noinit 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



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

Lock-Centered (with may-V) also succeeds:

$ goblint --set ana.base.privatization lock 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
Loading