Restarting of Access globals as a baseline for the incremental solver #703
Assignees
Labels
Comments
The crucial difference is that there was no incremental postsolving before, so all the accesses had to be regenerated each time.
Prior to incremental postsolving, there were even no unknowns for accesses, but it was all done ad-hoc. So effectively they used to be all restarted (the incrementally loaded run started with no accesses) and all recalculated (by the non-incremental postsolver). So if I understand the idea correctly, it's exactly what they did, but it was all implicit because the access tables were a global OCaml data structure that simply wasn't marshaled. Or am I misunderstanding something?
Just like I described above, at the time of the previous paper, the non-incremental postsolver implicitly reset all of them to empty sets. Now with non-incremental postsolver, we also reset all of them to empty sets (by not reusing any of |
|
Decision at GobCon was to write a story about it, implement it (which hopefully should be very simple) and then decide. |
|
fixed and merged back. |
|
We used this for the smtprc story in hopes to get minimal restarting of not write-only unknowns, but just globals. Somehow this wasn't any faster than full restarting. After the deadline I also tried to go through the smtprc story using fuel 1 to achieve minimal restarting (available on In #721 (comment) you also say:
So it really seems like there's some problem with that option, not doing what is intended and degrading to full restarting. On smtprc it seems to do all the same restarts as full restarting, just in a different order. smtprc storyWith this (#721)Using Restarts after patch 1
Restarts after patch 2
With fuel (#629)Using Restarts after patch 1
Restarts after patch 2
cc: @vesalvojdani |
|
Strange! I can't really look into it today, but will hopefully do so soon |
|
I looked into it and here's the problem. The added Hence one would want to copy the same check to diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 02a45c47c..3d829a25e 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -592,9 +592,12 @@ module WP =
(not restart_only_globals || Node.equal (S.Var.node x) (Function Cil.dummyFunDec)) && (not (S.Var.is_write_only x))
in
+ let restarted = ref false in
+
if not (VS.is_empty w) && should_restart then (
(* restart side-effected var *)
restart_leaf x;
+ restarted := true;
(* add side_dep to front to prevent them from being aborted *)
destabilize_front ~front:true x w;
@@ -621,7 +624,10 @@ module WP =
if tracing then trace "sol2" "stable remove %a\n" S.Var.pretty_trace y;
HM.remove stable y;
HM.remove superstable y;
- destabilize_with_side ~side_fuel ~front:false y
+ if not !restarted || restart_destab_with_sides then
+ destabilize_with_side ~side_fuel ~front:false y
+ else
+ destabilize_normal ~front:false y
) w;
(* destabilize side infl *)
smtprc with this patchRestarts after patch 1
Restarts after patch 2
The restarts now are much more reasonable and closer to the fuel 1 ones, although surprisingly still not exactly the same. Instead of two restarts of fuel 1 for patch 1 of smtprc, this makes five restarts, including Seems to me like #629 is still better at limiting this by only needing a single check at |
|
@stilscher @jerhard Did we use this for any of the evaluations in the paper and is this still needed in light of #629? |
|
From one of the latest interactive discussions on Slack, this could be achieved using:
Thus the broken |
sim642
added a commit
that referenced
this issue
Aug 4, 2022
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
@stilscher discussed this with Helmut yesterday, and at some point I also joined the discussion.
The issue we currently face is that we try to sell the non-restarting of access globals as a contribution (c.f. read-only globals). However, already in the basic setting without the incremental post-solver we are smart about these accesses in that we only really collect them during postsolving, which already is part of the insight we want to sell.
So for comparison, we were thinking about implementing a more naive approach:
If we implement this, this gives us a natural testbed for selective restarting and also shows that just the Seidl, Vogler, Erhard incrementality is not enough, as it (without our insight) requires restarting of access globals, which is not something they do in their paper.
I think this sort of restarting ought to be easy to implement, as we already collect the dependencies during the access analysis anyway. I think to showcase the difference, it would even suffice to reset because that's what is needed conceptually and then still simply collect in the verification phase, as we iterate over the entire system anyway when the incremental post-solver is off.
WDYT @sim642 @vesalvojdani ?
And perhaps a stupid side question: In the setting without the incremental post-solver, do we actually reset the access globals to
bot, or are we truly just accumulating race warnings without it?The text was updated successfully, but these errors were encountered: