Optimize TD3 to not unnecessarily store bottom for just eval-ed variables by sim642 · Pull Request #349 · goblint/analyzer

sim642 · 2021-09-20T07:57:55Z

This was revealed by #345.
Simply get-ing/eval-ing global constraint variables added bottom to rho.
This unnecessarily increases rho with default values.

This PR changes TD3 such that it doesn't store those bottoms eagerly when a constraint variable is just read and never receives a real value. Thus most HM.find rho are wrapped with catching Not_found to return bottom. Is there maybe some reason I'm not aware of why TD3 doesn't use implicit bottom values already?

There were a few places where HM.mem rho was used, for which it matters whether the bottom value has been added or not. From what I can tell, these are just for the space variant and actually correspond to HM.mem wpoint, which is how those checks are presented in the TD3 paper.

I added two static variables to tune the bottom insertion behavior of init such that the old behavior can easily be toggled as well.

…bles This was revealed by #345. Simply get-ing/eval-ing global constraint variables added bottom to rho. This unnecessarily increases rho with default values. An an unintended consequence, the bottom values for all dead local variables also never get stored.

This is the best of both worlds: 1. no stored bot for just read globals, 2. stored bot for dead code (to avoid recomputation).

sim642 · 2021-09-20T08:01:37Z

src/solvers/td3.ml

-        (* if HM.mem called y then (init y; let y' = HM.find_default l y (S.Dom.bot ()) in HM.replace rho y y'; HM.remove l y; y') else *)
+        if S.system y = None then (init y; add_infl y x; try HM.find rho y with Not_found -> S.Dom.bot ()) else
+        if not space || HM.mem wpoint y then (solve y Widen; add_infl y x; try HM.find rho y with Not_found -> S.Dom.bot ()) else
+        if HM.mem called y then (init y; HM.remove l y; add_infl y x; try HM.find rho y with Not_found -> S.Dom.bot ()) else


This HM.mem called y case doesn't exist in the TD3 paper. Is it some optimization? If so, then maybe there should be an explanatory comment.

sim642 · 2021-09-20T08:05:28Z

src/solvers/td3.ml

-          HM.replace rho x (S.Dom.bot ())
+          if init_bot_all || (init_bot_rhs && S.system x <> None) then
+            HM.replace rho x (S.Dom.bot ())
+          (* TODO: fix new_var_event repeatedly triggering when init-ing multiple times without value *)


it looks like the solver variable counting happens very primitively by incrementing a counter:

analyzer/src/solvers/generic.ml

Lines 207 to 209 in 5a434cd

let new_var_event x =

Goblintutil.vars := !Goblintutil.vars + 1;

if tracing then trace "sol" "New %a\n" Var.pretty_trace x

Seems to me like this could just be HM.length rho, which would fix the new issue.

michael-schwarz · 2021-09-22T09:07:06Z

To recap from Gobcon yesterday: The bottoms that are inserted are meaningful in that the hashtable for a partial (post-)solution should be closed, i.e. not depend on any implicit bottoms for any unknown.
If this is the case, the domain of the hashtable actually contains the information that these are the only unknowns that were queried by the solver during the computation of the fixpoint.

From a purely practical standpoint, I guess the question is whether one wants to introduce an option that still makes this optimization, in case one is not interested in the domain. I think this something we should then only consider if it leads to improved performance of the solver, quicker marshaling, or some other measurable improvement.

sim642 · 2021-09-22T11:26:19Z

To recap from Gobcon yesterday: The bottoms that are inserted are meaningful in that the hashtable for a partial (post-)solution should be closed, i.e. not depend on any implicit bottoms for any unknown.
If this is the case, the domain of the hashtable actually contains the information that these are the only unknowns that were queried by the solver during the computation of the fixpoint.

In the space variant, the solution hashtable isn't closed anyway and missing keys might even correspond to non-bottom values. And the paper goes through all the trouble to define the closure of such solution to make it meaningful. Surely the reasoning for closing only bottoms is much simpler since it requires no transfer function evaluations (and resolving between wpoint).
So I don't think it makes things any more sophisticated than it already is.

Moreover, we already make this assumption of implicit bottoms in the partial solution all over the place: Verify2, Reachability, Control, etc. They all wrap solution lookups in such a way, so this behavior has clearly been part of Goblint's design.

EDIT 1: Even TD3 itself, before these changes, follows this convention in some places:

analyzer/src/solvers/td3.ml

Lines 334 to 338 in 139734d

    
           let check_side x y d = 
        
             HM.replace visited y (); 
        
             let mem = HM.mem rho y in 
        
             let d' = try HM.find rho y with Not_found -> S.Dom.bot () in 
        
             if not (S.Dom.leq d d') then ignore @@ Pretty.printf "TDFP Fixpoint not reached in restore step at side-effected variable (mem: %b) %a from %a: %a not leq %a\n" mem S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty d S.Dom.pretty d'

analyzer/src/solvers/td3.ml

Lines 390 to 391 in 139734d

    
           and one_constraint f = 
        
             ignore (f (fun x -> one_var x; try HM.find rho x with Not_found -> ignore @@ Pretty.printf "reachability: one_constraint: could not find variable %a\n" S.Var.pretty_trace x; S.Dom.bot ()) (fun x _ -> one_var x))

analyzer/src/solvers/td3.ml

Lines 473 to 475 in 139734d

    
           let old_rho = (Serialize.unmarshal file_in: solver_data).rho in 
        
           let eq r s = 
        
             let leq r s = HM.fold (fun k v acc -> acc && (try S.Dom.leq v (HM.find s k) with Not_found -> false)) r true

So it's not even consistent within TD3 itself and that's why it seems like this was intended, but left uncompleted at some point.

EDIT 2: To drive this even further, the TD3 article doesn't even have init. In the published version, them being bottom is implicit, but in the unpublished extended version this defaulting is explicit: Map.create (fun () -> ⊥).

michael-schwarz · 2022-08-08T12:43:25Z

Do we want to do something with this or close it? I would vote for only merging this if we can show it to have significant performance impact.

michael-schwarz · 2022-09-16T16:10:55Z

@stilscher @jerhard @sim642 Opinions on whether we should mege (with a special option) or close this?

sim642 · 2022-09-16T16:47:24Z

I think it's not worth complicating things by having another option for this feature, which probably made no performance difference. But I'll have a closer look before closing.

sim642 · 2022-09-20T08:12:46Z

I cherry-picked 1f4bd6e onto master because it's orthogonal cleanup, but let's leave the rest for now.

sim642 added 8 commits September 17, 2021 15:59

Distribute TD3 eval add_infl into simple_solve

703a88e

Inline TD3 simple_solve into eval

bc9adb6

Remove now unnecessary one_constraint warning from TD3

b585d42

Change rho checks to wpoint checks in TD3 eval to match article

1f4bd6e

Add intermediate TD3 init bot behavior

b994a08

This is the best of both worlds: 1. no stored bot for just read globals, 2. stored bot for dead code (to avoid recomputation).

Merge branch 'either-lattice' into td3-noinit

02038c4

Update TD3 init bot after Either -> Lift2 lattice change

5a434cd

sim642 added the performance Analysis time, memory usage label Sep 20, 2021

sim642 requested a review from vogler September 20, 2021 07:57

sim642 commented Sep 20, 2021

View reviewed changes

sim642 closed this Sep 20, 2022

sim642 mentioned this pull request Apr 17, 2025

Narrowing of globals in TD #1636

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Optimize TD3 to not unnecessarily store bottom for just eval-ed variables#349

Optimize TD3 to not unnecessarily store bottom for just eval-ed variables#349
sim642 wants to merge 8 commits intomasterfrom
td3-noinit

sim642 commented Sep 20, 2021

Uh oh!

sim642 Sep 20, 2021

Uh oh!

sim642 Sep 20, 2021

Uh oh!

michael-schwarz commented Sep 22, 2021 •

edited

Loading

Uh oh!

sim642 commented Sep 22, 2021 •

edited

Loading

Uh oh!

michael-schwarz commented Aug 8, 2022

Uh oh!

michael-schwarz commented Sep 16, 2022

Uh oh!

sim642 commented Sep 16, 2022

Uh oh!

sim642 commented Sep 20, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

	let new_var_event x =
	Goblintutil.vars := !Goblintutil.vars + 1;
	if tracing then trace "sol" "New %a\n" Var.pretty_trace x

Conversation

sim642 commented Sep 20, 2021

Uh oh!

sim642 Sep 20, 2021

Choose a reason for hiding this comment

Uh oh!

sim642 Sep 20, 2021

Choose a reason for hiding this comment

Uh oh!

michael-schwarz commented Sep 22, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

michael-schwarz commented Aug 8, 2022

Uh oh!

michael-schwarz commented Sep 16, 2022

Uh oh!

sim642 commented Sep 16, 2022

Uh oh!

sim642 commented Sep 20, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

michael-schwarz commented Sep 22, 2021 •

edited

Loading

sim642 commented Sep 22, 2021 •

edited

Loading