Restarting of Access globals as a baseline for the incremental solver #703
Description
@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:
- Without this insight that it suffices to collect accesses during postsolving, we would already collect them during the fixpoint iteration.
- Then, to make sure that (at least some) of the warnings can actually go away, we would have to selectively restart those access globals that received side-effects from changed functions (potentially more, but I guess for a practical evaluation it would suffice to do those for now)
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?