Minimal write-only restarting is insufficient: add ana.malloc.include-node
#647
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Turns out #634, which performs minimal restarting for write-only globals like accesses, is insufficient to even guarantee from-scratch consistency of write-only globals. Hence there's no from-scratch consistency of race warnings either!
Problems
mallocnodesIn
tests/incremental/13-restart-write/04-malloc-node.cthe incremental run gives two memory locations (old and new malloc) instead of just the expected one. This causes an inconsistency in the number of race warnings because the number of memory locations isn't even consistent (not to mention anything about their raciness).This is because
allocvariables are based on the node ofmalloc, which changes if the function is incrementally changed.The possible solution for this is to not include nodes in
allocvariables, just like the disabling ofana.thread.include-nodedoesn't include them in thread IDs. But thenallocvariables would be just per-function, so allmallocdata from a single function gets joined together. If two different types of data are stored, then we immediately get value domain supertop, which is far from ideal.EDIT: I have now added
ana.malloc.include-node, which does fix this specific problem.Broader issue
We've seen the node-based things be a problem for incrementality in thread IDs and now
allocvariables, but the issue is much more general. It really means that nothing should be based on nodes since incremental changes may change their IDs. This possibly also includes access collecting (which refer to nodes as their origin), but maybe more things which don't immediately pop into mind.So really what we need is very fine-grained update, which keeps statement IDs for everything that didn't actually change and simply removes/adds IDs for actually removed/added statements.
Indirect access removal
In
tests/incremental/13-restart-write/05-race-call-remove.cthe incremental run has a race, whereas it should not. When the call to a function accessing the global in a racy way is removed, then minimal write-only restarting doesn't get rid of that access, because it doesn't originate from a changed function. The destabilization of the old copy doesn't destabilize anything infoo, because normal destabilization only followsinfl, but notside_infl.The possible solution for this is something like the transitive sides restarting with
destabilize_with_side, but slightly weaker: it doesn't need to restart anything, but only destabilize viainflandside_infl.This also fixes the above
mallocnode issue on the original knot_comb race benchmark, but doubles the basic incremental runtime from 15s to 30s (from-scratch is ~60s). Despite just being more extensive destabilization, it causes a lot more recomputation, which aborting doesn't even help with.Broader issue
This again is not just specific to write-only restarting, but incremental postsolving in general. To avoid reevaluating everything we make the assumption that all
superstableunknowns are reachable and don't prune them. But that's an overapproximation of the reachable unknowns, since in the call removal case it similarly would still think that the unknowns offooare reachable since they never get destabilized. Destabilization alongside_inflwould also fix that, but at the same high cost.