Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Sep 29, 2021

This is an attempt to restart destabilized side-effected variables (at least globals, but could also be function entry nodes in presence of partial contexts) to bottom when loading previous results. This allows globals (and especially their protecting locksets) to improve after fixing the program.

At loading time, obsolete nodes are destabilized with a special destabilize_with_side function instead. This requires knowing infl for side effects (in side_infl) but also dependencies for side effects (in side_dep) to replay the unchanged ones. Both additional mappings are constructed during reachability at saving time.

TODO

  • Decide whether to just restart globals or also function entry nodes. The former requires ugly FromSpec-specific hack inside TD3.
  • Benchmark on larger programs.

@vesalvojdani
Copy link
Member

vesalvojdani commented Oct 4, 2021

I think unmarshalling version.data is stuck... can you try doing this in the bench repo:

../analyzer/goblint --enable kernel linux/drivers/char/applicom.c --enable incremental.save --enable printstats -v
../analyzer/goblint --enable kernel linux/drivers/char/applicom.c --enable incremental.load --enable printstats -v

Can you reproduce it?

@sim642 sim642 mentioned this pull request Oct 4, 2021
2 tasks
sim642 added 2 commits October 4, 2021 17:57
This currently still works with restart_only_globals=true, because destabilize_with_side follows all side effects nevertheless.
@sim642 sim642 changed the base branch from master to interactive October 6, 2021 08:17
@sim642 sim642 marked this pull request as ready for review October 6, 2021 08:18
@sim642
Copy link
Member Author

sim642 commented Oct 6, 2021

We decided to start merging some of these together into the branch interactive for better experimentation.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants