Skip to content

Commit

Permalink
Generalize mutex-meet-tid privatization to arbitrary digest
Browse files Browse the repository at this point in the history
  • Loading branch information
@sim642
sim642 committed Nov 30, 2023
1 parent 69dd788 commit 5a7ea92
Show file tree
Hide file tree
Showing 3 changed files with 81 additions and 57 deletions.
45 changes: 24 additions & 21 deletions src/analyses/apron/relationPriv.apron.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -903,7 +903,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 @@ -913,21 +913,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 Digest.compatible ask current k then
LRD.join acc (Cluster.keep_only_protected_globals ask m v)
else
acc
Expand Down Expand Up @@ -1035,8 +1031,8 @@ struct
if not atomic then (
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 @@ -1090,8 +1086,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 All @@ -1102,8 +1098,8 @@ struct
let w' = W.filter (fun v -> not (is_unprotected_without ask v m)) w in
let rel_side = keep_only_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
let (lmust', l') = W.fold (fun g (lmust, l) ->
sideg (V.global g) (G.create_mutex sidev);
let lm = LLock.global g in
Expand Down Expand Up @@ -1191,8 +1187,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 @@ -1368,17 +1364,24 @@ end

let priv_module: (module S) Lazy.t =
lazy (
let module TIDDigest = ThreadDigest (
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
)
in
let module Priv: S =
(val match get_string "ana.relation.privatization" with
| "top" -> (module Top : S)
| "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 (TIDDigest) (NoCluster))
| "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (TIDDigest) (DownwardClosedCluster (Clustering12)))
| "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (TIDDigest) (ArbitraryCluster (Clustering2)))
| "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (TIDDigest) (ArbitraryCluster (ClusteringMax)))
| "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (TIDDigest) (DownwardClosedCluster (ClusteringPower)))
| _ -> failwith "ana.relation.privatization: illegal value"
)
in
Expand Down
39 changes: 21 additions & 18 deletions src/analyses/basePriv.ml
View file
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 Digest.compatible ask current 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 @@ -1798,12 +1794,19 @@ end

let priv_module: (module S) Lazy.t =
lazy (
let module TIDDigest = ThreadDigest (
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
)
in
let module Priv: S =
(val match get_string "ana.base.privatization" with
| "none" -> (module NonePriv: S)
| "mutex-oplus" -> (module PerMutexOplusPriv)
| "mutex-meet" -> (module PerMutexMeetPriv)
| "mutex-meet-tid" -> (module PerMutexMeetTIDPriv)
| "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (TIDDigest))
| "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: 36 additions & 18 deletions src/analyses/commonPriv.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -154,12 +154,44 @@ struct
end
end

module type Digest =
sig
include Printable.S

val current: Q.ask -> t
val compatible: Q.ask -> t -> t -> bool
end

module type PerMutexTidCommonArg = sig
val exclude_not_started: unit -> bool
val exclude_must_joined: unit -> bool
end

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

module TID = ThreadIdDomain.Thread

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

let compatible (ask: Q.ask) (current: t) (other: t) =
let must_joined = ask.f Queries.MustJoinedThreads in
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
end

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

Expand Down Expand Up @@ -196,7 +228,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 +250,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 Digest.compatible ask current k then
LD.join acc v
else
acc
Expand Down

0 comments on commit 5a7ea92

Please sign in to comment.