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

Generalize mutex-meet-tid privatization to arbitrary digest #1278

Merged
merged 5 commits into from
Jan 11, 2024
Merged

Generalize mutex-meet-tid privatization to arbitrary digest #1278

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
a392323
Generalize mutex-meet-tid privatization to arbitrary digest
sim642 Nov 30, 2023
6dfc08f
Simplify CommonPriv.ThreadDigest
sim642 Nov 30, 2023
05198f9
Avoid MustJoinedThreads query in ThreadDigest if not needed
sim642 Nov 30, 2023
bda139f
Rename Digest.compatible -> accounted_for
sim642 Dec 5, 2023
0704cd5
Flip Digest.accounted_for implementation to match name
sim642 Dec 5, 2023
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
34 changes: 15 additions & 19 deletions src/analyses/apron/relationPriv.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -844,7 +844,7 @@ struct
end

(** Per-mutex meet with TIDs. *)
module PerMutexMeetPrivTID (Cluster: ClusterArg): S = functor (RD: RelationDomain.RD) ->
module PerMutexMeetPrivTID (Digest: Digest) (Cluster: ClusterArg): S = functor (RD: RelationDomain.RD) ->
struct
open CommonPerMutex(RD)
include MutexGlobals
Expand All @@ -854,21 +854,17 @@ struct
module Cluster = NC
module LRD = NC.LRD

include PerMutexTidCommon(struct
let exclude_not_started () = GobConfig.get_bool "ana.relation.priv.not-started"
let exclude_must_joined () = GobConfig.get_bool "ana.relation.priv.must-joined"
end)(LRD)
include PerMutexTidCommon (Digest) (LRD)

module AV = RD.V
module P = UnitP

let name () = "PerMutexMeetPrivTID(" ^ (Cluster.name ()) ^ (if GobConfig.get_bool "ana.relation.priv.must-joined" then ",join" else "") ^ ")"

let get_relevant_writes (ask:Q.ask) m v =
let current = ThreadId.get_current ask in
let must_joined = ask.f Queries.MustJoinedThreads in
let current = Digest.current ask in
GMutex.fold (fun k v acc ->
if compatible ask current must_joined k then
if not (Digest.accounted_for ask ~current ~other:k) then
LRD.join acc (Cluster.keep_only_protected_globals ask m v)
else
acc
Expand Down Expand Up @@ -946,8 +942,8 @@ struct
(* unlock *)
let rel_side = RD.keep_vars rel_local [g_var] in
let rel_side = Cluster.unlock (W.singleton g) rel_side in
let tid = ThreadId.get_current ask in
let sidev = GMutex.singleton tid rel_side in
let digest = Digest.current ask in
let sidev = GMutex.singleton digest rel_side in
sideg (V.global g) (G.create_global sidev);
let l' = L.add lm rel_side l in
let rel_local' =
Expand Down Expand Up @@ -984,8 +980,8 @@ struct
else
let rel_side = keep_only_protected_globals ask m rel in
let rel_side = Cluster.unlock w rel_side in
let tid = ThreadId.get_current ask in
let sidev = GMutex.singleton tid rel_side in
let digest = Digest.current ask in
let sidev = GMutex.singleton digest rel_side in
sideg (V.mutex m) (G.create_mutex sidev);
let lm = LLock.mutex m in
let l' = L.add lm rel_side l in
Expand Down Expand Up @@ -1069,8 +1065,8 @@ struct
in
let rel_side = RD.keep_vars rel g_vars in
let rel_side = Cluster.unlock (W.top ()) rel_side in (* top W to avoid any filtering *)
let tid = ThreadId.get_current ask in
let sidev = GMutex.singleton tid rel_side in
let digest = Digest.current ask in
let sidev = GMutex.singleton digest rel_side in
sideg V.mutex_inits (G.create_mutex sidev);
(* Introduction into local state not needed, will be read via initializer *)
(* Also no side-effect to mutex globals needed, the value here will either by read via the initializer, *)
Expand Down Expand Up @@ -1208,11 +1204,11 @@ let priv_module: (module S) Lazy.t =
| "protection" -> (module ProtectionBasedPriv (struct let path_sensitive = false end))
| "protection-path" -> (module ProtectionBasedPriv (struct let path_sensitive = true end))
| "mutex-meet" -> (module PerMutexMeetPriv)
| "mutex-meet-tid" -> (module PerMutexMeetPrivTID (NoCluster))
| "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (DownwardClosedCluster (Clustering12)))
| "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (ArbitraryCluster (Clustering2)))
| "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (ArbitraryCluster (ClusteringMax)))
| "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (DownwardClosedCluster (ClusteringPower)))
| "mutex-meet-tid" -> (module PerMutexMeetPrivTID (ThreadDigest) (NoCluster))
| "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (ThreadDigest) (DownwardClosedCluster (Clustering12)))
| "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (ThreadDigest) (ArbitraryCluster (Clustering2)))
| "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (ThreadDigest) (ArbitraryCluster (ClusteringMax)))
| "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (ThreadDigest) (DownwardClosedCluster (ClusteringPower)))
| _ -> failwith "ana.relation.privatization: illegal value"
)
in
Expand Down
32 changes: 14 additions & 18 deletions src/analyses/basePriv.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -391,14 +391,11 @@ struct
st
end

module PerMutexMeetTIDPriv: S =
module PerMutexMeetTIDPriv (Digest: Digest): S =
struct
open Queries.Protection
include PerMutexMeetPrivBase
include PerMutexTidCommon(struct
let exclude_not_started () = GobConfig.get_bool "ana.base.priv.not-started"
let exclude_must_joined () = GobConfig.get_bool "ana.base.priv.must-joined"
end)(CPA)
include PerMutexTidCommon (Digest) (CPA)

let iter_sys_vars getg vq vf =
match vq with
Expand All @@ -425,11 +422,10 @@ struct
r

let get_relevant_writes (ask:Q.ask) m v =
let current = ThreadId.get_current ask in
let must_joined = ask.f Queries.MustJoinedThreads in
let current = Digest.current ask in
let is_in_Gm x _ = is_protected_by ~protection:Weak ask m x in
GMutex.fold (fun k v acc ->
if compatible ask current must_joined k then
if not (Digest.accounted_for ask ~current ~other:k) then
CPA.join acc (CPA.filter is_in_Gm v)
else
acc
Expand Down Expand Up @@ -474,8 +470,8 @@ struct
CPA.add x v st.cpa
in
if M.tracing then M.tracel "priv" "WRITE GLOBAL SIDE %a = %a\n" CilType.Varinfo.pretty x VD.pretty v;
let tid = ThreadId.get_current ask in
let sidev = GMutex.singleton tid (CPA.singleton x v) in
let digest = Digest.current ask in
let sidev = GMutex.singleton digest (CPA.singleton x v) in
let l' = L.add lm (CPA.singleton x v) l in
let is_recovered_st = ask.f (Queries.MustBeSingleThreaded {since_start = false}) && not @@ ask.f (Queries.MustBeSingleThreaded {since_start = true}) in
let l' = if is_recovered_st then
Expand Down Expand Up @@ -517,8 +513,8 @@ struct
{st with cpa = cpa'; priv = (w',lmust,l)}
else
let is_in_Gm x _ = is_protected_by ~protection:Weak ask m x in
let tid = ThreadId.get_current ask in
let sidev = GMutex.singleton tid (CPA.filter is_in_Gm st.cpa) in
let digest = Digest.current ask in
let sidev = GMutex.singleton digest (CPA.filter is_in_Gm st.cpa) in
sideg (V.mutex m) (G.create_mutex sidev);
let lm = LLock.mutex m in
let l' = L.add lm (CPA.filter is_in_Gm st.cpa) l in
Expand Down Expand Up @@ -568,13 +564,13 @@ struct

let escape ask getg sideg (st: BaseComponents (D).t) escaped =
let escaped_cpa = CPA.filter (fun x _ -> EscapeDomain.EscapedVars.mem x escaped) st.cpa in
let tid = ThreadId.get_current ask in
let sidev = GMutex.singleton tid escaped_cpa in
let digest = Digest.current ask in
let sidev = GMutex.singleton digest escaped_cpa in
sideg V.mutex_inits (G.create_mutex sidev);
let cpa' = CPA.fold (fun x v acc ->
if EscapeDomain.EscapedVars.mem x escaped (* && is_unprotected ask x *) then (
if M.tracing then M.tracel "priv" "ESCAPE SIDE %a = %a\n" CilType.Varinfo.pretty x VD.pretty v;
let sidev = GMutex.singleton tid (CPA.singleton x v) in
let sidev = GMutex.singleton digest (CPA.singleton x v) in
sideg (V.global x) (G.create_global sidev);
CPA.remove x acc
)
Expand All @@ -587,8 +583,8 @@ struct
let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) =
let cpa = st.cpa in
let cpa_side = CPA.filter (fun x _ -> is_global ask x) cpa in
let tid = ThreadId.get_current ask in
let sidev = GMutex.singleton tid cpa_side in
let digest = Digest.current ask in
let sidev = GMutex.singleton digest cpa_side in
sideg V.mutex_inits (G.create_mutex sidev);
(* Introduction into local state not needed, will be read via initializer *)
(* Also no side-effect to mutex globals needed, the value here will either by read via the initializer, *)
Expand Down Expand Up @@ -1795,7 +1791,7 @@ let priv_module: (module S) Lazy.t =
| "none" -> (module NonePriv: S)
| "mutex-oplus" -> (module PerMutexOplusPriv)
| "mutex-meet" -> (module PerMutexMeetPriv)
| "mutex-meet-tid" -> (module PerMutexMeetTIDPriv)
| "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (ThreadDigest))
| "protection" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false end))
| "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true end))
| "mine" -> (module MinePriv)
Expand Down
54 changes: 33 additions & 21 deletions src/analyses/commonPriv.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -154,12 +154,38 @@ struct
end
end

module type PerMutexTidCommonArg = sig
val exclude_not_started: unit -> bool
val exclude_must_joined: unit -> bool
module type Digest =
sig
include Printable.S

val current: Q.ask -> t
val accounted_for: Q.ask -> current:t -> other:t -> bool
end

module PerMutexTidCommon (Conf:PerMutexTidCommonArg) (LD:Lattice.S) =
module ThreadDigest: Digest =
struct
include ThreadIdDomain.ThreadLifted

module TID = ThreadIdDomain.Thread

let current (ask: Q.ask) =
ThreadId.get_current ask

let accounted_for (ask: Q.ask) ~(current: t) ~(other: t) =
match current, other with
| `Lifted current, `Lifted other ->
if TID.is_unique current && TID.equal current other then
true (* self-read *)
else if GobConfig.get_bool "ana.relation.priv.not-started" && MHP.definitely_not_started (current, ask.f Q.CreatedThreads) other then
true (* other is not started yet *)
else if GobConfig.get_bool "ana.relation.priv.must-joined" && MHP.must_be_joined other (ask.f Queries.MustJoinedThreads) then
true (* accounted for in local information *)
else
false
| _ -> false
end

module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) =
struct
include ConfCheck.RequireThreadFlagPathSensInit

Expand Down Expand Up @@ -196,7 +222,7 @@ struct

(* Map from locks to last written values thread-locally *)
module L = MapDomain.MapBot_LiftTop (LLock) (LD)
module GMutex = MapDomain.MapBot_LiftTop (ThreadIdDomain.ThreadLifted) (LD)
module GMutex = MapDomain.MapBot_LiftTop (Digest) (LD)
module GThread = Lattice.Prod (LMust) (L)

module G =
Expand All @@ -218,24 +244,10 @@ struct

module D = Lattice.Prod3 (W) (LMust) (L)

let compatible (ask:Q.ask) current must_joined other =
match current, other with
| `Lifted current, `Lifted other ->
if (TID.is_unique current) && (TID.equal current other) then
false (* self-read *)
else if Conf.exclude_not_started () && MHP.definitely_not_started (current, ask.f Q.CreatedThreads) other then
false (* other is not started yet *)
else if Conf.exclude_must_joined () && MHP.must_be_joined other must_joined then
false (* accounted for in local information *)
else
true
| _ -> true

let get_relevant_writes_nofilter (ask:Q.ask) v =
let current = ThreadId.get_current ask in
let must_joined = ask.f Queries.MustJoinedThreads in
let current = Digest.current ask in
GMutex.fold (fun k v acc ->
if compatible ask current must_joined k then
if not (Digest.accounted_for ask ~current ~other:k) then
LD.join acc v
else
acc
Expand Down
Loading