sim642
commented
2 years ago 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.
The crucial difference is that there was no incremental postsolving before, so all the accesses had to be regenerated each time.
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.
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?
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?
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 rho_write). So AFAIK accesses have never been accumulated like how the global values and protecting sets have.
michael-schwarz
@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?