Incremental TD3: reluctant function destabilization #369
Conversation
| (* record whether any function's start state changed. In that case do not use reluctant destabilization *) | ||
| let any_changed_start_state = ref false in |
There was a problem hiding this comment.
If earlyglobs is turned on and a global initializer changes, the start state of a start function changes but its context stays the same. To still trigger the reanalysis for the start function, a check is implemented at the beginning of the incremental preprocessing in the td3 solver to detect this and explicitly destabilize the start function. If this happens and the start function is already fully destabilized there is no need to apply reluctant destabilization on the changed functions afterwards.
There was a problem hiding this comment.
If
earlyglobsis turned on and a global initializer changes, the start state of a start function changes but its context stays the same.
If earlyglobs is on, the globals are never in the local states even, so changing a global initializer doesn't change the start state of the start function (nor its context). The change to the global initializer should just be destabilizing the global and thus everywhere its read.
Or do you mean when earlyglobs is off, because then globals are initially in the start state?
If this happens and the start function is already fully destabilized there is no need to apply reluctant destabilization on the changed functions afterwards.
The start state of a function changing is a function-specific property though. If one function's start state changes, but another's doesn't, then reluctant destabilization could still be applied to the latter. Changing one shouldn't prevent reluctant destabilization of others, but just the changed one.
Also, destabilizing a function entry that was already destabilized shouldn't really be doing anything: the first destabilize clears its infl, so the second one doesn't do anything anyway.
There was a problem hiding this comment.
If earlyglobs is on, the globals are never in the local states even, so changing a global initializer doesn't change the start state of the start function (nor its context).
There seems to be some inconsistent behavior now. If you run the following minimalistic example with the incremental config (i.e. privatization off) the function main has a changed start state (because of the changed global initializer) and is therefor destabilized during the preparation for the incremental run. The global g is not a member of the list st.
int g = 0; // change to g = 2;
int main() {
return 0;
}
This is the behavior of the incremental analysis as I know it and as it is described in the comments of the changed start state handling. I managed however to reconstruct what you described by turning privatization and the (probably not incremental compatible) mutex analysis on. Do you know if there was any recent change to the privatization that could affect this? Why are globals part of st with privatization turned on?
The start state of a function changing is a function-specific property though. If one function's start state changes, but another's doesn't, then reluctant destabilization could still be applied to the latter.
With the behavior I described above, a changed global initializer affects the start state of every start function so all of them are destabilized anyway. If it weren't like that, it would be nicer to make a distinction between which function's start state changed. The problem I see is, that one can't relate an arbitrary changed function to the start function it is (indirectly) being called from. So it would be difficult (at least efficiently) to tell whether the changed function needs to be solved separately as part of reluctant destabilization.
Also, destabilizing a function entry that was already destabilized shouldn't really be doing anything: the first
destabilizeclears itsinfl, so the second one doesn't do anything anyway.
The point is not to avoid the destabilization, but to avoid the function specific solve on a possibly outdated context. If the start function has been destabilized completely anyway, solving it with the top-down solver directly avoids unnecessary evaluations.
There was a problem hiding this comment.
If you run the following minimalistic example with the incremental config (i.e. privatization off) the function
mainhas a changed start state (because of the changed global initializer) and is therefor destabilized during the preparation for the incremental run. The globalgis not a member of the listst.
I've never been a fan of earlyglobs, so I'm not 100% sure what its expected behavior should be. But my understanding has been that it should from the beginning (global initialization) make global program variables into global constraint system variables, so g should be in st. Not being there and instead remaining in the entry state of the function sounds like an earlyglobs bug to me.
the (probably not incremental compatible) mutex analysis
I'm not sure why the mutex analysis should be incompatible with incremental because incremental analysis on the level of constraint systems shouldn't care whatsoever about the content of the constraint system.
The only problem currently (before #363) is that protecting locksets in global constraint variables cannot improve, but that should be all.
Do you know if there was any recent change to the privatization that could affect this?
No, but it could be a bug remaining from the time all the traces article privatization implementations were added. earlyglobs caused a bunch of annoying issues there, but those got fixed to the extent that the regression tests pass. Although there might still be some bug that wasn't caught by the tests then.
Why are globals part of
stwith privatization turned on?
Without earlyglobs, globals are kept in the local state just like all other variables. This allows them to be analyzed flow-sensitively. As long as the program is in single-threaded mode, they will be there.
What privatization does is that when multi-threaded mode is entered, they are removed from the local state and instead tracked flow-insensitively in the global invariant.
There was a problem hiding this comment.
Is there a reason to have such a set_start? Couldn't it just call side to set those, which wouldn't overwrite but would accumulate soundly?
The start values are a weird thing altogether: in #370 I realized I have to use them to construct transformed right-hand sides, which also join those desired start values. Because all they really are, is right-hand sides with a constant value.
There was a problem hiding this comment.
I'm not sure why the mutex analysis should be incompatible with incremental because incremental analysis on the level of constraint systems shouldn't care whatsoever about the content of the constraint system.
Sorry, I mixed this up. I was thinking about the ids of threads that seem to be based on the location of the function to be executed. So this would be a problem for the consistency of ids across different versions in an incremental run.
There was a problem hiding this comment.
Is there anything actionable left here? We need a long-term fix for these sorts of program harnessing type hacks, which is #178, but is there some direct fix needed to ensure earlyglobs publish is more robust? To me that seems out of scope for this pull request, or does this need fixing here and now?
There was a problem hiding this comment.
After the discussions and decision on Friday, no, there's no need to address these things here.
There was a problem hiding this comment.
Ok, I think I can merge this PR. For fixing the incremental analysis to handle globals in the start variables properly, I will open a new issue because it does not really relate to reluctant destabilization but rather to the incremental analysis in general.
|
Some very preliminary benchmarking on this is available here: It seems that this reluctant stuff should be on (although we should compare with how the aborting does and if these things play well together), but there is also some strange behavior on this one patch where I move the locking to cover also some initialization code. This removes a false alarm. The incremental is then is even with reluctance much slower than the from scratch computation. The brilliant script does not display the patches, so here's the problematic change: [Edit:] Wait, I should have looked at all of them before drawing some conclusions. Similar kind of performance also for a change that should not refine globals, unless the return value is checked and tons of fewer accesses happen?! |
sim642
changed the title
This pull request contains an improvement for the incremental analysis in the td3 solver (#351). With this, the changed functions are not destabilized right away anymore before solving once completely. Instead it is split as follows:
leqthen the old one.solveis called on the queried unknown. This ensures, that possibly new side-effects affecting the queried unknown are taken into account.Note that for this to work, it is necessary to adopt the previous ids for formal parameters of changed functions when possible. This way, the contexts of different versions for a function entry node of a changed function can coincide. Then the result from the separate solving phase for changed functions can actually be used and is not unnecessarily re-analyzed in the final
solve.A config parameter has been introduced to deactivate the reluctant destabilization when needed.