TD3: optimize destabilization by aborting transfer function when unchanged

[sim642]

This is an attempt to optimize destabilization by making the resolving reluctant (not the destabilization).

The problem and intuition is that when something gets destabilized, the propagating changes might not change everything all the way to the end of the program (or a called variable). At some point the result might be unchanged, but the outer solve call will still evaluate the transfer function once more to observe that each layer going up is unchanged. If all the inputs to the transfer function (computation tree) are unchanged, then this is unnecessary computation (the result will be the same as before).

The trick is the following: if all dependencies (in destab_dep) of a variable are unchanged, then the last eval will raise AbortEq, which will be caught outside the transfer function. This is necessary because if something has changed, then the only way to know the new dependencies (which may be different) is to evaluate the black box of the transfer function.
The functions solve, simple_solve and eval are changed to return a boolean indicating whether a change occurred or not.

This is still not sufficient to behave correctly because a destabilized variable might be solved (and thus made stable again) before another influenced variable of it is solved again. Thus the changed value might incorrectly appear as unchanged.

To combat this problem, a front (in destab_front) of destabilized variables is tracked. Initially it consists of the first layer of destablized variables (the rest are still destabilized recursively, but not added to the front). When a variable in the front changes (during a later solve), it pushes the front forward to its influences variables (before destabilization, in destab_infl). If however it doesn't change, then the front dies out there and all destabilized variables after the died front never have to be reevaluated.

TODO

• Add back support for space variant. (Can be enabled without abort, fails with abort.)
• Benchmark.
• Optimize FromSpec to first getl all values for Cfg.prev before executing any of the transfer functions. This could provide earlier abort opportunities.
• Figure out how to combine with Incremental TD3: restart destabilized side-effected variables #363 to merge to interactive.

[sim642]

Here's a performance comparison of no-abort (x-axis) vs abort (y-axis, without abort-verify) on sv-benchmarks SoftwareSystems+ConcurrencySafety with 60s timeout:

So almost always this provides a performance boost of up to 1.5 times. The few outliars, last I checked, are those weird cases where we nondeterministically have ERROR (verify).

After the final fixes at this point, running with abort-verify confirms no illegal abortions (pun intended), but similar benchmarks also show that it's not worth keeping enabled all the time because it defeats the gain by abort.

[sim642]

I tried optimizing FromSpec to get all CFG predecessor values before executing any of their transfer functions (which matters at join points), but it didn't seem to make a noticeable difference.

Interestingly it introduced 6 outliars where a stack overflow turned into a simple timeout:

So somehow this reordering of things in the right-hand sides changes the solving enough to not recurse so deep. I'm not sure how exactly though.

[sim642]

Merging into the branch interactive for better experimentation.