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

Add may-ever-have-been-locked digests for relational mutex-meet #1286

Closed
wants to merge 7 commits into from
Closed
Show file tree
Hide file tree
Changes from 6 commits
Commits
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
1 change: 1 addition & 0 deletions src/analyses/apron/relationPriv.apron.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1209,6 +1209,7 @@ let priv_module: (module S) Lazy.t =
| "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)))
| "mutex-meet-lock" -> (module PerMutexMeetPrivTID (LockDigest) (NoCluster))
| _ -> failwith "ana.relation.privatization: illegal value"
)
in
Expand Down
11 changes: 11 additions & 0 deletions src/analyses/commonPriv.ml
Original file line number Diff line number Diff line change
Expand Up @@ -185,6 +185,17 @@ struct
| _ -> true
end

module LockDigest: Digest =
struct
include PreValueDomain.AD

let current (ask: Q.ask) =
ask.f MayLocksDigest

let compatible (ask: Q.ask) (current: t) (other: t) =
true (* TODO *)
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is to still be implemented for the new digests. This is called $\mathsf{acc}$ in the paper, but is never defined there (?).

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

acc is defined p.17 and eq (7), but it is specific to one instance, namely this thread id one, where things that are compatible digest-wise may still be ruled out as they are "accounted-for" in the local state (e.g. contributions of threads that have been joined).

If one wants to speak at the level of digests, the appropriate notion is $[[u,act]]^\sharp_\mathcal{A}(A_0,A_1)$ being defined or not.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In the implementation this compatible is the only thing that filters any reads out. Also being called "compatible" probably mislead me to think that's all there is to it. I'll rename it to accounted_for in #1278.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The fact that the refinement should happen due to the lock operation of the digest itself, not accounted_for, somehow gets us back at analyses splitting each other's global unknowns.
Or naively, the relational analysis needs to repeat the exact same lock operations on the digests to see which raise Deadcode as the maylocksdigest analysis is already doing to find the new digests.

I suspect the only reasonable way is to implement digests as a functor around an analysis, just like the paper proposes, to have direct and full control over these things in one place.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I suspect the only reasonable way is to implement digests as a functor around an analysis, just like the paper proposes, to have direct and full control over these things in one place.

Actually even that doesn't seem to work because instead of $m_g$-s we implicitly lock and unlock them in each read_global/write_global. But each of those $\mathsf{lock}(m_g)$ operations has to split if there are multiple globals accessed in a single expression. The issue is that our ctx.split is final: for the split-off branch, no more operations in the transfer function are executed, but the actual variable read and $\mathsf{unlock}(m_g)$ also needs to be executed. Not to mention everything that happens after read_global returns to RelationAnalysis to do other global accesses or whatnot.

Even if these digests were fully embedded into the privatization like TIDs have been so far, the same problem comes up: read_global needs to split into all of these cases and continue executing each one. We'd need CPS or list monad or multi-shot continuations to achieve that, all of which are major fundamental design changes.

So I have no more realistic ideas on how to make these digests work at all. Unless anyone else does, we simply won't be able to implement them (especially in time for CAV).

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can discuss this at the next GobCon. Maybe shooting for the general solution is overly ambitious, and we could investigate how to incorporate specific digests?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This isn't just a matter of going for the general solution because all of these problems have come up even with the specific simple may-ever-have-been-locked digests. Any other non-ego-lane-derived will inevitably have the very same fundamental problems.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

True, but there might be slight generalizations of ego-lane derived digests that maybe limit what is transmitted at m_g locks, which may still be helpful.

The other thing is if we maybe are able to do some bookkeeping for these m_g locks and then dealy the actual split operation until later... But I'll have to think more deeply about it.

end

module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) =
struct
include ConfCheck.RequireThreadFlagPathSensInit
Expand Down
49 changes: 49 additions & 0 deletions src/analyses/mayLocksDigest.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
(** May lockset digest analysis ([maylocksdigest]). *)

open Analyses
open GoblintCil
module LF = LibraryFunctions

module Arg =
struct
module D = LockDomain.MayLocksetNoRW
module P = IdentityP (D)

module V =
struct
include StdV
include LockDomain.Addr
end
module G = SetDomain.Make (D)

let add (ctx: (D.t, G.t, D.t, V.t) ctx) (l,r) =
let l's = ctx.global l in
G.iter (fun l' ->
if not (D.mem l ctx.local && not (D.mem l l')) then
ctx.split (D.add l (D.union ctx.local l')) []
) l's;
if D.mem l ctx.local then
raise Deadcode
else
D.add l ctx.local (* for initial empty *)

let remove (ctx: (D.t, G.t, D.t, V.t) ctx) l =
ctx.sideg l (G.singleton ctx.local);
ctx.local
end

module Spec =
struct
include LocksetAnalysis.MakeMay (Arg)
let name () = "maylocksdigest"

let threadenter ctx ~multiple lval f args = [ctx.local]

let query (ctx: (D.t, _, _, _) ctx) (type a) (q: a Queries.t): a Queries.result =
match q with
| MayLocksDigest -> ctx.local
| _ -> Queries.Result.top q
end

let _ =
MCP.register_analysis ~dep:["mutexEvents"] (module Spec : MCPSpec)
2 changes: 1 addition & 1 deletion src/common/util/options.schema.json
Original file line number Diff line number Diff line change
Expand Up @@ -921,7 +921,7 @@
"description":
"Which relation privatization to use? top/protection/protection-path/mutex-meet/mutex-meet-tid/mutex-meet-tid-cluster12/mutex-meet-tid-cluster2/mutex-meet-tid-cluster-max/mutex-meet-tid-cluster-power",
"type": "string",
"enum": ["top", "protection", "protection-path", "mutex-meet", "mutex-meet-tid", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power"],
"enum": ["top", "protection", "protection-path", "mutex-meet", "mutex-meet-tid", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power", "mutex-meet-lock"],
"default": "mutex-meet"
},
"priv": {
Expand Down
5 changes: 5 additions & 0 deletions src/domains/queries.ml
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,7 @@ type _ t =
| MayBePublicWithout: maybepublicwithout -> MayBool.t t
| MustBeProtectedBy: mustbeprotectedby -> MustBool.t t
| MustLockset: AD.t t
| MayLocksDigest: AD.t t
| MustBeAtomic: MustBool.t t
| MustBeSingleThreaded: {since_start: bool} -> MustBool.t t
| MustBeUniqueThread: MustBool.t t
Expand Down Expand Up @@ -200,6 +201,7 @@ struct
| MustTermAllLoops -> (module MustBool)
| IsEverMultiThreaded -> (module MayBool)
| TmpSpecial _ -> (module ML)
| MayLocksDigest -> (module AD)

(** Get bottom result for query. *)
let bot (type a) (q: a t): a result =
Expand Down Expand Up @@ -268,6 +270,7 @@ struct
| MustTermAllLoops -> MustBool.top ()
| IsEverMultiThreaded -> MayBool.top ()
| TmpSpecial _ -> ML.top ()
| MayLocksDigest -> AD.top ()
end

(* The type any_query can't be directly defined in Any as t,
Expand Down Expand Up @@ -333,6 +336,7 @@ struct
| Any IsEverMultiThreaded -> 55
| Any (TmpSpecial _) -> 56
| Any (IsAllocVar _) -> 57
| Any MayLocksDigest -> 58

let rec compare a b =
let r = Stdlib.compare (order a) (order b) in
Expand Down Expand Up @@ -489,6 +493,7 @@ struct
| Any MustTermAllLoops -> Pretty.dprintf "MustTermAllLoops"
| Any IsEverMultiThreaded -> Pretty.dprintf "IsEverMultiThreaded"
| Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv
| Any MayLocksDigest -> Pretty.dprintf "MayLocksDigest"
end

let to_value_domain_ask (ask: ask) =
Expand Down
41 changes: 41 additions & 0 deletions tests/regression/46-apron2/58-lock-digest.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
// PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-lock --set ana.activated[+] maylocksdigest --set ana.path_sens[+] maylocksdigest --set ana.path_sens[+] threadflag
#include <pthread.h>
#include <goblint.h>

int g, h;
pthread_mutex_t a = PTHREAD_MUTEX_INITIALIZER;

void *t2(void *arg) {
pthread_mutex_lock(&a);
// wrong in more-traces!
__goblint_check(h < g); // TODO
pthread_mutex_unlock(&a);
return NULL;
}

void *t1(void *arg) {
pthread_t x;
pthread_create(&x, NULL, t2, NULL);

pthread_mutex_lock(&a);
h = 11; g = 12;
pthread_mutex_unlock(&a);
return NULL;
}

void *t0(void *arg) {
return NULL;
}

int main() {
pthread_t x;
pthread_create(&x, NULL, t0, NULL); // go multithreaded

pthread_mutex_lock(&a);
h = 9;
g = 10;
pthread_mutex_unlock(&a);

pthread_create(&x, NULL, t1, NULL);
return 0;
}