Timeouts are broken #946
Comments
|
Indeed, I have independently reached the same error when implementing the steps limit (#936). |
This is a hotfix while we figure out a proper way forward for OCamlPro#946 so that Alt-Ergo doesn't randomly crash due to timeouts in the meantime.
This is a hotfix while we figure out a proper way forward for #946 so that Alt-Ergo doesn't randomly crash due to timeouts in the meantime.
|
From the outside, we should not be able to use an environment that is in an invalid state (unknown reason = Timeout or StepLimit). |
This requires that invalid environments would necessarily throw an exception when doing something incorrect, and would not be able to silently return an incorrect model (or, worse, to incorrectly report Hm. I am thinking that we might be able to do something by blocking the timeout signal while mutating the SAT (and re-instating it before doing theory propagation). This would allow to have "safe points" inside the SAT to raise the timeout exception, ensuring that we can't end up in an invalid state (along with a "hard" timeout that would bypass that, I guess). I have been looking at the |
|
Although actually I am not sure this would be very smart, because #798 intend to introduce (backtrackable) mutable state in the theory as well 🙃 What we can definitely do is have a "soft" timeout variant that we check periodically (e.g. after each propagation) instead of using a signal, which would be safe to resume from (but also we might overstep a bit). To my knowledge this is how other solvers (at least Z3 and CVC5) do things — there is both a "hard" timeout similar to the one that we currently have that just kills the solver, and a "soft" timeout similar to what I describe above. |
It would not return silently an incorrect model, as the unknown reason would still be Timeout. We can warn the user that the model may be invalid in that case.
This looks very dangerous considering there may be a large set of side effects to perform in order to have a consistent environment and there is no easy way to bound the calculation time of these effects (maybe I'm wrong, but I have a bad feeling about this). |
I will maybe wait for this before starting to work on this issue |
That is true, it should work. I don't think we would need an additional warning, either. Hm. I think in the abstract I would prefer using a soft timer (i.e. regularly checking that we have not overstepped the limit) because it feels more stable (does not depend on whether the timeout was reached within a small critical section) but it is also more work, so your suggestion is probably better in the current situation.
To be clear I was not proposing we only do this, but to do it as part of a two-timers scenario (so that if the "outer" time limit is exceeded we just full stop everything as we do currently). But as I said above, if we go for a two-timers scenario, explicit checking of the soft timer is better.
This was an offer but I did not start working on it, and we have since determined that it was not the way forward, so go ahead! |
Actually, we should always warn the user if we don't test the model, as there is no guarantee the model is sound (though I agree the model after timeout has less chance to be sound than a model computed in time) |
The user is warned by the fact that we reply "unknown" and not "sat", though. There are no requirements on models produced after an "unknown" reply; the SMT-LIB states explicitly page 64 that "The model A is required to satisfy all currently asserted |
Timeouts were disabled in satml_frontend (check OCamlPro#946); this PR re-enables them with a generic exception catcher wrapping calls to a possibly invalid environment.
|
Following discussion at the users' club meeting: we should implement a soft timeout. The right place to check for the soft timeout is probably roughly where we increment the step counters. (Taking this one) |
It looks like some of the recent changes (I'd guess either #829 or #861 is the source) have broken timeout support badly. The core of the issue is that, since timeouts can occur at any allocation point and satML uses imperative state, it is deeply incorrect to keep using a satML solver after a timeout, because it can be in an arbitrary intermediate state that has no guarantee to be valid.
It looks like we can, because the satML solver is wrapped in a "persistent" satML-frontend, but in fact the frontend just shares the imperative state (a design flaw in itself, but mostly irrelevant here).
When a timeout is reached, we cannot keep the model around at all. This is probably also the case with step limits, so tagging @Stevendeo who has been looking at that. In both cases I don't think we have a choice but to throw the model away.
There are multiple places where this has an impact:
model_gen_on_timeoutlogic cannot be used for satMLTimeoutexception into anI_dont_know, we cannot keep the same satML environment, as it might be in an invalid state. I think that the only thing we can do in the current architecture is return an empty model, but we do need to be careful that that empty model does not contain any assertions. Alternatively, we can have a newInvalidstatus instead ofUnknownto keep track of that.On
/data/smtlib/2022/QF_BV/sage/app12/bench_4308.smt2with--timelimit 1I get the crash below. Removing the conversions fromUtil.TimeouttoI_dont_knowin the satML-frontend fixes the issue.The text was updated successfully, but these errors were encountered: