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.

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

Optimize none base privatization, add eager Vojdani privatization #1552

Open
wants to merge 13 commits into
base: master
Choose a base branch
from
208 changes: 164 additions & 44 deletions src/analyses/basePriv.ml
Original file line number Diff line number Diff line change
Expand Up @@ -101,12 +101,12 @@ module DigestWrapper(Digest: Digest):PrivatizationWrapper = functor (GBase:Latt
end)


(* No Privatization *)
(** No Privatization. *)
module NonePriv: S =
struct
include NoFinalize

module G = BaseDomain.VD
module G = VD
module V = VarinfoV
module D = Lattice.Unit

Expand All @@ -117,63 +117,80 @@ struct
let lock ask getg st m = st
let unlock ask getg sideg st m = st

let escape ask getg sideg st escaped = st
let enter_multithreaded ask getg sideg st = st
let threadenter = old_threadenter
let threadspawn ask getg sideg st = st

let iter_sys_vars getg vq vf =
match vq with
| VarQuery.Global g -> vf g
| _ -> ()


let read_global ask getg (st: BaseComponents (D).t) x =
let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
getg x

let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
if invariant then (
(* Do not impose invariant, will not hold without privatization *)
if M.tracing then M.tracel "set" ~var:x.vname "update_one_addr: BAD! effect = '%B', or else is private! " (not invariant);
st
)
else (
(* Here, an effect should be generated, but we add it to the local
* state, waiting for the sync function to publish it. *)
(* Copied from MainFunctor.update_variable *)
if ((get_bool "exp.volatiles_are_top") && (is_always_unknown x)) then
{st with cpa = CPA.add x (VD.top ()) st.cpa}
michael-schwarz marked this conversation as resolved.
Show resolved Hide resolved
else
{st with cpa = CPA.add x v st.cpa}
)
let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
if not invariant then
sideg x v;
st

let sync ask getg sideg (st: BaseComponents (D).t) reason =
(* For each global variable, we create the side effect *)
let side_var (v: varinfo) (value) (st: BaseComponents (D).t) =
if M.tracing then M.traceli "globalize" ~var:v.vname "Tracing for %s" v.vname;
let res =
if is_global ask v then begin
if M.tracing then M.tracec "globalize" "Publishing its value: %a" VD.pretty value;
sideg v value;
{st with cpa = CPA.remove v st.cpa}
end else
st
in
if M.tracing then M.traceu "globalize" "Done!";
res
let branched_sync () =
(* required for branched thread creation *)
CPA.fold (fun x v (st: BaseComponents (D).t) ->
if is_global ask x then (
sideg x v;
{st with cpa = CPA.remove x st.cpa}
)
else
st
) st.cpa st
in
(* We fold over the local state, and side effect the globals *)
CPA.fold side_var st.cpa st
match reason with
| `Join when ConfCheck.branched_thread_creation () ->
branched_sync ()
| `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
branched_sync ()
| `Join
| `JoinCall _
| `Return
| `Normal
| `Init
| `Thread ->
st

let escape ask getg sideg (st: BaseComponents (D).t) escaped =
let cpa' = CPA.fold (fun x v acc ->
if EscapeDomain.EscapedVars.mem x escaped then (
sideg x v;
CPA.remove x acc
)
else
acc
) st.cpa st.cpa
in
{st with cpa = cpa'}

let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) =
CPA.fold (fun x v (st: BaseComponents (D).t) ->
if is_global ask x then (
sideg x v;
{st with cpa = CPA.remove x st.cpa}
)
else
st
) st.cpa st

let threadenter ask st = st
let threadspawn ask get set st = st

let thread_join ?(force=false) ask get e st = st
let thread_return ask get set tid st = st

let iter_sys_vars getg vq vf =
match vq with
| VarQuery.Global g ->
vf g;
| _ -> ()

let invariant_global ask getg g =
ValueDomain.invariant_global getg g

let invariant_vars ask getg st = []
end


module PerMutexPrivBase =
struct
include NoFinalize
Expand Down Expand Up @@ -683,6 +700,108 @@ struct
end


(** Vojdani privatization with eager reading. *)
module VojdaniPriv: S =
struct
include NoFinalize
include ConfCheck.RequireMutexActivatedInit
open Protection

module D = Lattice.Unit
module G = VD
module V = VarinfoV

let startstate () = ()

let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
if is_unprotected ask ~write:false x then
VD.join (CPA.find x st.cpa) (getg x)
else
CPA.find x st.cpa

let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
if not invariant then (
if is_unprotected ask ~write:false x then
sideg x v;
if !earlyglobs then (* earlyglobs workaround for 13/60 *)
sideg x v (* TODO: is this needed for anything? 13/60 doesn't work for other reasons *)
);
{st with cpa = CPA.add x v st.cpa}

let lock ask getg (st: BaseComponents (D).t) m =
let cpa' = CPA.mapi (fun x v ->
if is_protected_by ask ~write:false m x && is_unprotected ask ~write:false x then (* is_in_Gm *)
VD.join (CPA.find x st.cpa) (getg x)
else
v
) st.cpa
in
{st with cpa = cpa'}

let unlock ask getg sideg (st: BaseComponents (D).t) m =
CPA.iter (fun x v ->
if is_protected_by ask ~write:false m x then ( (* is_in_Gm *)
if is_unprotected_without ask ~write:false x m then (* is_in_V' *)
sideg x v
)
) st.cpa;
st

let sync ask getg sideg (st: BaseComponents (D).t) reason =
let branched_sync () =
(* required for branched thread creation *)
CPA.iter (fun x v ->
if is_global ask x && is_unprotected ask ~write:false x then
sideg x v
) st.cpa;
st
in
match reason with
| `Join when ConfCheck.branched_thread_creation () ->
branched_sync ()
| `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
branched_sync ()
| `Join
| `JoinCall _
| `Return
| `Normal
| `Init
| `Thread ->
st

let escape ask getg sideg (st: BaseComponents (D).t) escaped =
CPA.iter (fun x v ->
if EscapeDomain.EscapedVars.mem x escaped then
sideg x v
) st.cpa;
st

let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) =
CPA.iter (fun x v ->
if is_global ask x then
sideg x v
) st.cpa;
st

let threadenter ask st = st
let threadspawn ask get set st = st

let thread_join ?(force=false) ask get e st = st
let thread_return ask get set tid st = st

let iter_sys_vars getg vq vf =
match vq with
| VarQuery.Global g ->
vf g;
| _ -> ()

let invariant_global ask getg g =
ValueDomain.invariant_global getg g

let invariant_vars ask getg st = protected_vars ask
end


module type PerGlobalPrivParam =
sig
(** Whether to also check unprotectedness by reads for extra precision. *)
Expand Down Expand Up @@ -1909,6 +2028,7 @@ let priv_module: (module S) Lazy.t =
let module Priv: S =
(val match get_string "ana.base.privatization" with
| "none" -> (module NonePriv: S)
| "vojdani" -> (module VojdaniPriv: S)
| "mutex-oplus" -> (module PerMutexOplusPriv)
| "mutex-meet" -> (module PerMutexMeetPriv)
| "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (ThreadDigest))
Expand Down
8 changes: 4 additions & 4 deletions src/analyses/commonPriv.ml
Original file line number Diff line number Diff line change
Expand Up @@ -82,22 +82,22 @@ end
module Protection =
struct
open Q.Protection
let is_unprotected ask ?(protection=Strong) x: bool =
let is_unprotected ask ?(write=true) ?(protection=Strong) x: bool =
let multi = if protection = Weak then ThreadFlag.is_currently_multi ask else ThreadFlag.has_ever_been_multi ask in
(!GobConfig.earlyglobs && not multi && not (is_excluded_from_earlyglobs x)) ||
(
multi &&
ask.f (Q.MayBePublic {global=x; write=true; protection})
ask.f (Q.MayBePublic {global=x; write; protection})
)

let is_unprotected_without ask ?(write=true) ?(protection=Strong) x m: bool =
(if protection = Weak then ThreadFlag.is_currently_multi ask else ThreadFlag.has_ever_been_multi ask) &&
ask.f (Q.MayBePublicWithout {global=x; write; without_mutex=m; protection})

let is_protected_by ask ?(protection=Strong) m x: bool =
let is_protected_by ask ?(write=true) ?(protection=Strong) m x: bool =
is_global ask x &&
not (VD.is_immediate_type x.vtype) &&
ask.f (Q.MustBeProtectedBy {mutex=m; global=x; write=true; protection})
ask.f (Q.MustBeProtectedBy {mutex=m; global=x; write; protection})

let protected_vars (ask: Q.ask): varinfo list =
LockDomain.MustLockset.fold (fun ml acc ->
Expand Down
4 changes: 2 additions & 2 deletions src/config/options.schema.json
Original file line number Diff line number Diff line change
Expand Up @@ -759,9 +759,9 @@
"privatization": {
"title": "ana.base.privatization",
"description":
"Which privatization to use? none/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/lock-tid/write/write-tid/write+lock/write+lock-tid",
"Which privatization to use? none/vojdani/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/lock-tid/write/write-tid/write+lock/write+lock-tid",
"type": "string",
"enum": ["none", "mutex-oplus", "mutex-meet", "protection", "protection-tid", "protection-atomic", "protection-read", "protection-read-tid", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "lock-tid", "write", "write-tid", "write+lock", "write+lock-tid", "mutex-meet-tid"],
"enum": ["none", "vojdani", "mutex-oplus", "mutex-meet", "protection", "protection-tid", "protection-atomic", "protection-read", "protection-read-tid", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "lock-tid", "write", "write-tid", "write+lock", "write+lock-tid", "mutex-meet-tid"],
"default": "protection-read"
},
"priv": {
Expand Down
12 changes: 11 additions & 1 deletion src/framework/constraints.ml
Original file line number Diff line number Diff line change
Expand Up @@ -81,8 +81,18 @@ struct
ignore (getl (Function fd, c))
| exception Not_found ->
(* unknown function *)
M.error ~category:Imprecise ~tags:[Category Unsound] "Created a thread from unknown function %s" f.vname
M.error ~category:Imprecise ~tags:[Category Unsound] "Created a thread from unknown function %s" f.vname;
(* actual implementation (e.g. invalidation) is done by threadenter *)
(* must still sync for side effects, e.g. old sync-based none privatization soundness in 02-base/51-spawn-special *)
sim642 marked this conversation as resolved.
Show resolved Hide resolved
let rec sync_ctx =
{ ctx with
ask = (fun (type a) (q: a Queries.t) -> S.query sync_ctx q);
local = d;
prev_node = Function dummyFunDec;
}
in
(* TODO: more accurate ctx? *)
ignore (sync sync_ctx)
michael-schwarz marked this conversation as resolved.
Show resolved Hide resolved
) ds
in
(* ... nice, right! *)
Expand Down
Loading