Incremental TD3: fix start variables

[stilscher]

Closes #384

In the past, start variables only contained functions at the point where the solver data is prepared for an incremental run in TD3. This has changed with the newer privatizations. They no longer need to rely on sync to side-effect globals that were temporarily added to the start states. Instead globals can be immediately added to the start variables when the global initializers are run. Because of this, the start variables might now also contain globals when the preparation for the incremental run is executed.

In this PR, the data preparation for the incremental run was adapted to also handle globals in start variables properly. It keeps the checking for changed start states because these are necessary for the incremental analysis to still work with older privatizations and options like ana.context.base.int where globals are part of the start state but neither in the start variables nor the context before the actual solve. The PR contains the following changes:

• propagating changes in the global initializers with side for globals that are in the start variables
• with globals possibly being part of the start variables and not the start state or context, overwriting the start states in general is faulty because writes to a global in an unchanged function are not re-analyzed in an incremental run and their effect might then be lost. Therefore, a start state is only overwritten when the corresponding start function needs to be destabilized because of a changed start state
• exclude globals that might be contained in the start variables from the check for a changed start state
• provide incremental test cases that are fixed with this PR

[sim642]

I'm always reluctant (pun intended) to add such constraint-system specific hacks into our supposedly generic local solvers. Why can't they all be treated equal? Sure, the printed comments here would be wrong to speak of just functions, but other than that what would break?

Also, this check makes another specialization which makes subtle assumptions about what we are querying the solver for. Namely, in the generic setting there's no reason that the queried variables (vs) and the starting variables (st) have to come in exactly matching pairs of variables corresponding to functions.

[jerhard]

Why can't they all be treated equal?

The problem is whether or not one should do a set_start, which overwrites the value in rho with the value that is associated to the unknown in st and adds the unknown to stable. For function start points this makes sense, as a complete reanalysis for a start function is required anyway, if its start state changes.
For globals with changed start value, resetting their value in rho to the new start value is a problem, because the unknowns that side-effect to them are not automatically destabilized.

[sim642]

But why not do side for all of them, both globals and function entries? Sure, that joins with the previous value, but only when the context of the function start also stays the same.

Having set_start overwrite instead of join (in side) for function entries is some kind of limited form of restarting (#363) which only restarts the start variables and nothing else. Is that really such a significant precision improvement?

[jerhard]

Having set_start overwrite instead of join (in side) for function entries is some kind of limited form of restarting (#363) which only restarts the start variables and nothing else.

#363 indeed seems to subsume the set_start for functions, though one cannot currently configure #363 in a manner so that it only does this restarting for start functions. But probably that is not needed?

[jerhard]

Regarding whether #363 completely subsumes the desirable behavior here: In case the analyzed code is multi-threaded or earlyglobs is activated, if the start state of a start function changes, one has to re-analyze starting from the end to start of the changed start function anyway. But still the resetting that #363 does, might required some additional rounds of evaluations as globals start from their start value.

@sim642 Would it make sense in #363 to split the option "incremental.restart.sided.only-global" into "incremental.restart.sided.globals" and "incremental.restart.sided.funs"? Then one could replicate the behavior from this PR by setting "incremental.restart.sided.globals"=false and "incremental.restart.sided.funs"=true.

[sim642]

I could do that. only-global was intended to be experimented with first to even determine whether it's a distinction worth making in terms of performance and precision.

Just restarting function entries wouldn't exactly give the behavior from here, because the question is what happens with function entries, which aren't the start function, but do get destabilized from something else. #363 would also restart those, this one wouldn't.

So the restarting that's done here is even more limited (in all sensible cases to just main). The question is whether this even more limited form of restarting is worth considering at all.
Maybe it is in case global initializers are in the start state and changed, so you want to overwrite those (instead of joining), but not restart any other functions.

[jerhard]

@stilscher and I discussed this today. We would go for the solution that does side for all variables, including start functions. Otherwise there are some complications in the code for which we don't really know whether they pay out in practice.

[jerhard]

Did checking whether any start state changed, and only doing the reluctant destabilization then have a significant impact on the experiments?
One could do a similar check if the side were to return a boolean indicating whether the side effect changed something.

[jerhard]

I guess we can just merge this as-is, to fix the issue; and later possibly look at it again.

[stilscher]

I just compared both variations on a very small example (first 50 commits of figlet). Applying reluctant destabilization only when no start state changed seemed not to be beneficial there. Time wise there is almost no difference. The average evaluations are greater. And it gives a reduced number of evaluations only for 4 commits whereas for another 10 commits the number of evaluations increases.

[stilscher]

And even though the code for checking whether a start functions start state changed was removed by now anyway, I just noticed that in order for the code in 3d7c0ed to work correctly, one would need a call to set_start also for the new start functions.