Incremental TD3: limit side-effected restarting using fuel

[sim642]

The fuel works as follows:

• 0 fuel never restarts a side-effected unknown,
• positive fuel restarts side-effected unknowns up to recursion depth (only counting side effect destabilizations),
• negative fuel simply means infinite fuel (internally represented by None), which by default gives the previous side-effected restarting behavior.

In the added incremental test, 1 fuel is enough to restart and remove the accesses from the only copy of the changed function and thus cause race warnings to disappear as expected. Maybe 1 fuel is sufficient for minimal automatic restarting for race warnings.
Other incremental tests which require between 1 and 3 fuel.

[sim642]

This fuel parameter spawns a new side quest: tuning the fuel allows tuning the runtime vs precision of the incremental analysis all of a sudden.

[vesalvojdani]

Would it be possible to limit fuel consumption to side-effects to shared variables only? This concept would be more meaningful and familiar if it corresponded more directly to placing bounds on the scheduler.

[sim642]

Would it be possible to limit fuel consumption to side-effects to shared variables only? This concept would be more meaningful and familiar if it corresponded more directly to placing bounds on the scheduler.

I added the option incremental.restart.sided.fuel-only-global for that.

[sim642]

Our bench results with fuel-only-global are now here: https://goblint.cs.ut.ee/simmo-results/bench_result-fuel-only-global/.
In this case 1 fuel is enough for everything there to achieve results equivalent to infinite fuel, so the intuition seems to be right. The downside is that it basically degrades to infinite fuel in terms of performance as well since it's essentially 1 fuel for global invariant and infinite fuel for function entry side effects. So the performance culprit of global restarting doesn't seem to be infinite "context changes" in this destabilization but rather the call stack depth.

[sim642]

Given #634, the question is whether we still want to have this option or not.
I suppose a fuel-based solution could also work for the second problem in #647 to have a destabilize_with_side_infl that's bounded by fuel.

[sim642]

I just brought this PR up to date with all the interactive branch improvements and noticed that the restarting of write-only unknowns during postprocessing was actually doing some of the restarting that a few of the previously added fuel tests were checking (so the tests didn't pass or didn't check anything meaningful about fuel).

Hence I added another option to disable the write-only restarting during postprocessing.
But now I'm very confused about #703 and this because:

1. With Restarting of Access globals as a baseline for the incremental solver #703 and incremental postsolver disabled, we were still restarting the write-only during postprocessing here, even with the non-incremental postsolver.
2. But if this is the case, then isn't Restarting of Access globals as a baseline for the incremental solver #703 completely redundant because for the comparison benchmark one can just disable the incremental postsolver, but have this restarting still take place, without having to have any only-access and fuel things for the general side effect restarting.

cc: @michael-schwarz

[michael-schwarz]

Ok, now I am confused. We want to have three possible settings:

1. No incremental post-solver at all, restarting of accesses globals (by destabilizing everything that has a side-effect on an access global)
2. Incremental post-solver without our write-only global insight (by destabilizing everything that has a side-effect on an access global)
3. Incremental post-solver with our write-only global insight (by not explicitly destabilizing things that have a side-effect on an access global, and reusing side-effects from unknowns that remain superstable & reachable)

It seems to me that we need special handling for the second thing here? What am I missing?

[sim642]

I agree with the sequence of settings:

• 1 → 2 enables incremental postsolver,
• 2 → 3 enables write-only restarting during postprocessing (as opposed to preprocessing, which gives us the general restarting).

My point is that at the time, there was no option to disable write-only restarting during postprocessing (it was unconditionally enabled). I only added such option here in this PR later.
This means that configurations 1 and 2 were impossible to achieve on the interactive branch. With general restarting enabled, but limited to only-access, and disabling your destab-with-side (or similarly using fuel 1), the write-only unknowns got restarted twice: first during the preprocessing restarting and then also during the postprocessing restarting.

So indeed, to get that sequence of changes we need fuel 1 only-access restarting, but it also means those benchmarks were even more flawed than just the issue with destab-with-side ending up with excessive restarting.
When writing my previous comment, I think I implicitly assumed there wasn't another flaw and so only a single direct benchmark comparison like 1 → 3 made sense in my head, which is how I also got confused and thought neither destab-with-side nor fuel would be necessary.

Anyway, I'll go forward with getting fuel merged to interactive as decided last week, but this realization means that the incremental.restart.write-only option (added just here) is also crucial for doing the re-benchmarking. I hope this doesn't cause a difference in results (the enabled and accidentally excessive destab-with-side only-access restarting probably dominates the special write-only restarting).