analyzer
analyzer copied to clipboard
goblint
Draft: Fuzzy CFG Matching with Unchanged RHS Skipping
In incremental runs, match the CFGs for partially changed functions on a "best effort" basis. Then, in the solver, destabilize the entire function (by destabilizing the function entry). Together with "aborting" (skip evaluation for unchanged RHS), this might be expected to save evaluations: if all the RHS variables evaluate to the same values, the evaluation of the RHS can be looked up from the incremental data (or at least that's my current understanding).
Since this is based on the eager_destab_cheap_abort branch, it fails the same tests as https://github.com/goblint/analyzer/pull/738#issuecomment-1131582234, along with 04/02 rename_and_shuffle which was added later.
TODO:
- Does this cause any problems with #774?
- Does this provide performance benefits (pending evaluation results)
Note: This pull request is part of my Bachelor's Thesis
Does it maybe make sense to change the base of this to eager_destab_cheap_abort in order to get a cleaner diff here?
And thank you for your pull request, moving in the direction of even more incrementality is something which is greatly appreciated!
I haven't looked closely at this, but my preliminary question is whether this new diffing mechanism is strongly tied to #738. On first glance, it seems like they should be orthogonal. Or is it simply that this improved diffing is supposed to combine particularly well with #738 for performance improvement?
Or is it simply that this improved diffing is supposed to combine particularly well with https://github.com/goblint/analyzer/pull/738 for performance improvement?
Yes, technically this doesn't depend on #738. However, this isn't expected to improve performance without it, since "fuzzy" matches still require destabilizing the affected nodes.
I guess the branch eager_destab_cheap_abort was auto-deleted when it was merged, and this somehow closed this PR?
@stilscher this is now stale by over 9 months. What's your plan here?
I think the reason I never spent the time to finish this up was because 1. the performance benefits were very unclear, and 2. I was never entirely confident that there weren't any lingering bugs in the implementation.
It shouldn't be too much work to rebase and merge though.
Thanks for the update. Let's wait until Sarah is back from vacation, and then we can decide what to do with it. If we're not sure there's any actual benefits, we might also decide to close without merging, as this is a substantial amount of code that will also need to be maintained.
Yep, I have no issue with closing if there's no plan for further work in this direction.