Forbid `sideg` in `query` by sim642 · Pull Request #214 · goblint/analyzer

sim642 · 2021-05-04T10:23:25Z

As I mentioned in #211 (comment), MCP2 intends to group side effects from multiple analyses to the same global variable together. I guess the intent is to make one sideg call to the solver with all the DomListLattice components filled instead of doing multiple sideg calls where each one has a DomListLattice with just a single non-bot component.

Before

When tracing some #183 things, I noticed that this doesn't seem to be happening. For example on this line with lockset {mutex1}:

analyzer/tests/regression/13-privatized/01-priv_nr.c

Line 13 in 4feae9f

glob1 = -10;

The solver first gets a side effect from mutex analysis:

%%% sol2: side to glob1 on 01-priv_nr.c:4 (wpx: true) from node 5 "assert(glob1 == -10);" on 01-priv_nr.c:14 ## value: [readwrite * write:({mutex1}, {mutex1}),
                                                                                                                        Unit:(),
                                                                                                                        Unit:(),
                                                                                                                        Unit:(),
                                                                                                                        Unit:(),
                                                                                                                        unprotected * protected:(Uninitialized, Uninitialized),
                                                                                                                        Unit:()]

After which some "init", "side widen" and "destabilize" take place. And after that the solver gets a separate side effect from base analysis:

%%% sol2: side to glob1 on 01-priv_nr.c:4 (wpx: true) from node 5 "assert(glob1 == -10);" on 01-priv_nr.c:14 ## value: [unprotected * protected:((-10), Uninitialized),
                                                                                                                        readwrite * write:(All mutexes, All mutexes),
                                                                                                                        Unit:(),
                                                                                                                        Unit:(),
                                                                                                                        Unit:(),
                                                                                                                        Unit:(),
                                                                                                                        Unit:()]

This isn't supposed to be happening because they both happen during the same MCP2.assign evaluation: base side effects the unprotected value, mutex side effects the protecting locksets.

Problem

Mutex analysis side effects the protecting locksets in part_access, which is since #162 called by query:

analyzer/src/analyses/mutexAnalysis.ml

Lines 78 to 87 in 4feae9f

    
           let part_access ctx e v w = 
        
             (*privatization*) 
        
             begin match v with 
        
               | Some v -> 
        
                 if not (Lockset.is_bot ctx.local) then 
        
                   let ls = Lockset.filter snd ctx.local in 
        
                   let el = P.effect_fun ~write:w ls in 
        
                   ctx.sideg v el 
        
               | None -> M.warn "Write to unknown address: privatization is unsound." 
        
             end;

This query is made in the ctx given to mutex analysis's assign:

analyzer/src/analyses/mutexAnalysis.ml

Lines 151 to 155 in 4feae9f

    
           let do_access (ctx: (D.t, G.t, C.t) ctx) (w:bool) (reach:bool) (conf:int) (e:exp) = 
        
             let open Queries in 
        
             let part_access ctx (e:exp) (vo:varinfo option) (w: bool) = 
        
               let open Access in 
        
               match ctx.ask (PartAccess {exp=e; var_opt=vo; write=w}) with

The ctx for the assign of mutex analysis is defined in MCP2 to do ask via query in MCP2:

analyzer/src/analyses/mCP.ml

Lines 560 to 573 in 4feae9f

    
           let assign (ctx:(D.t, G.t, C.t) ctx) l e = 
        
             let spawns = ref [] in 
        
             let splits = ref [] in 
        
             let sides  = ref [] in 
        
             let emits = ref [] in 
        
             let f post_all (n,(module S:MCPSpec),d) = 
        
               let ctx' : (S.D.t, S.G.t, S.C.t) ctx = 
        
                 { local  = obj d 
        
                 ; node   = ctx.node 
        
                 ; prev_node = ctx.prev_node 
        
                 ; control_context = ctx.control_context 
        
                 ; context = (fun () -> ctx.context () |> assoc n |> obj) 
        
                 ; edge   = ctx.edge 
        
                 ; ask    = query ctx

As the last snippet of code shows, whatever side effects that query makes, they don't get added into the sides list in assign, which is what is later grouped. That's why the access side effects bypass this grouping. I checked back at #162 and this behavior was present even before that change, so that PR didn't introduce this.

After

This is easily fixed by forbidding sideg in query and moving that part of part_access around to record the lockset with the assign's ctx, not the query one. Since access partitioning was refactored in #162, this has been a roundabout way to record the access anyway. No other queries use sideg anyway.

After these changes, the two side effects do get properly grouped:

%%% sol2: side to glob1 on 01-priv_nr.c:4 (wpx: true) from node 5 "assert(glob1 == -10);" on 01-priv_nr.c:14 ## value: [readwrite * write:({mutex1}, {mutex1}),
                                                                                                                        Unit:(),
                                                                                                                        unprotected * protected:((-10), Uninitialized),
                                                                                                                        Unit:(),
                                                                                                                        Unit:(),
                                                                                                                        Unit:(),
                                                                                                                        Unit:()]

I don't know whether this might slightly improve performance due to the solver not having to destabilize the same things multiple times.

… (=)

vogler · 2021-05-04T12:21:47Z

LGTM

I don't know whether this might slightly improve performance due to the solver not having to destabilize the same things multiple times.

What's our biggest benchmark with mutexes? Could compare evals.

sim642 · 2021-05-04T16:25:24Z

What's our biggest benchmark with mutexes? Could compare evals.

I tried it on smtproc_comb.c which is the slowest one to analyze in our traces paper at least and there the evals counts before and after have no difference.

I remember when I did the tracing outputs above, that between the two side effects there was init and destabilize, but TD3 at least didn't go into solving anything else. So the difference might not come from actual evaluations, but just avoiding doing duplicate destabilizations. I guess it also depends on how the solver works (i.e. orders the recomputation) and might be a meaningful difference with some other solver.

Based on single runs on that benchmark it went 11.4s → 11.0s, but this could be a total coincidence as well.

I might do a complete rerun with this change on the traces paper benchmarks to get a wider view, but I don't expect there to be too big of a difference.

michael-schwarz · 2021-05-05T08:01:19Z

LGTM as well!

sim642 · 2021-05-05T09:07:35Z

As an extra sanity check I reran the SAS21 benchmarks with this change merged in. The relative time differences are here:

	protection	mine-W	lock	write	write+lock
ctrace	-5.38%	-2.84%	-3.77%	-6.45%	-2.25%
pfscan	-6.09%	-6.37%	-6.48%	-3.15%	-4.86%
knot	6.98%	-2.48%	-4.35%	-1.47%	-3.35%
aget	-1.51%	-3.79%	-7.33%	-4.34%	-7.48%

ypbind	-3.36%	-8.56%	-7.29%	-9.24%	-8.72%
smtprc	-2.23%	-1.22%	-3.77%	-5.01%	-5.24%
iowarrior	-3.68%	0.05%	-1.54%	-1.44%	-0.76%
w83977af	-11.63%	-2.89%	-7.44%	-10.04%	-7.75%
adutux	-6.27%	-11.12%	-6.67%	-4.97%	-5.97%
tegra20	-8.51%	0.80%	-3.16%	-0.90%	-1.69%
marvell1	-10.00%	-12.80%	-9.01%	-8.93%	-9.23%
marvell2	-8.56%	-9.67%	-5.67%	-7.02%	-5.08%
nsc	-16.67%	-8.80%	-8.09%	-12.20%	-11.69%

So there is some general performance improvement, which is more pronounced on some benchmarks.

sim642 added 3 commits May 4, 2021 12:55

Forbid sideg in query

bd3d588

Fix mutex analysis to not sideg for protecting locksets in query

b390d24

Rename MCP.assoc_split_eq argument to avoid potential confusion about…

3daa4ad

… (=)

sim642 added the bug label May 4, 2021

Add comment about sideg being forbidden in query

096dbc4

sim642 added the performance Analysis time, memory usage label May 5, 2021

sim642 merged commit 11dcafd into master May 5, 2021

sim642 deleted the query-no-sideg branch May 5, 2021 11:13

sim642 mentioned this pull request Sep 10, 2021

Make malloc-ed variables non-unique #345

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Forbid `sideg` in `query`#214

Forbid `sideg` in `query`#214
sim642 merged 4 commits intomasterfrom
query-no-sideg

sim642 commented May 4, 2021 •

edited

Loading

Uh oh!

vogler commented May 4, 2021

Uh oh!

sim642 commented May 4, 2021 •

edited

Loading

Uh oh!

michael-schwarz commented May 5, 2021

Uh oh!

sim642 commented May 5, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

	let part_access ctx e v w =
	(privatization)
	begin match v with
	\| Some v ->
	if not (Lockset.is_bot ctx.local) then
	let ls = Lockset.filter snd ctx.local in
	let el = P.effect_fun ~write:w ls in
	ctx.sideg v el
	\| None -> M.warn "Write to unknown address: privatization is unsound."
	end;

	let do_access (ctx: (D.t, G.t, C.t) ctx) (w:bool) (reach:bool) (conf:int) (e:exp) =
	let open Queries in
	let part_access ctx (e:exp) (vo:varinfo option) (w: bool) =
	let open Access in
	match ctx.ask (PartAccess {exp=e; var_opt=vo; write=w}) with

	let assign (ctx:(D.t, G.t, C.t) ctx) l e =
	let spawns = ref [] in
	let splits = ref [] in
	let sides = ref [] in
	let emits = ref [] in
	let f post_all (n,(module S:MCPSpec),d) =
	let ctx' : (S.D.t, S.G.t, S.C.t) ctx =
	{ local = obj d
	; node = ctx.node
	; prev_node = ctx.prev_node
	; control_context = ctx.control_context
	; context = (fun () -> ctx.context () \|> assoc n \|> obj)
	; edge = ctx.edge
	; ask = query ctx

Conversation

sim642 commented May 4, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Before

Problem

After

Uh oh!

vogler commented May 4, 2021

Uh oh!

sim642 commented May 4, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

michael-schwarz commented May 5, 2021

Uh oh!

sim642 commented May 5, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

sim642 commented May 4, 2021 •

edited

Loading

sim642 commented May 4, 2021 •

edited

Loading