[crucible] Add deadman timeout for online solver actions #617
Conversation
Fixes #439 by implementing a parallel timeout operation (at 1 second longer than the timeout requested of the solver itself) whose expiration causes the solver process to be killed. This helps with issue 439 because Yices encounters some internal divergence issue that is not stopped by the specified timeout value (demonstrable by running the crux-llvm test-data/golden/strlen_test2 with the Yices solver option). This also helps provide timeout management for solvers that do not provide a built-in timeout capability (like Boolector).
|
Note that this requires GaloisInc/what4#83 |
| then doAction | ||
| else let deadmanTimeoutPeriod = (fromInteger $ | ||
| getGoalTimeoutInMilliSeconds | ||
| (solverGoalTimeout p) + 1000) * 1000 |
There was a problem hiding this comment.
This multiplication by 1000 is suspicious... is threadDelay in microseconds? If so, let's comment about that.
There was a problem hiding this comment.
I like the idea of this, although I'm always a little suspicious of any changes to the process handling, as it's easy to have unintended effects. Have you tested that everything works as it should? Solvers get killed when they need to and not when they don't? Do keyboard interrupts still work correctly, etc?
There was a problem hiding this comment.
I'm really happy to have this functionality, but would also second @robdockins concern. We should make sure we test this as thoroughly as possible.
|
A note we discussed on a bug triage call: last time I was working on timeouts for yices, I think I saw that it has different handling of signals if you are using the MCSAT backend vs the standard backend. I think that it could swallow signals sometimes, which might be something we need to report upstream. |
|
Just a note, the timeout should be handled at the what4 level, although there may be associated handling here. There is a what4 change in progress, but not yet submitted. |
Fixes #439 by implementing
a parallel timeout operation (at 1 second longer than the timeout
requested of the solver itself) whose expiration causes the solver
process to be killed.
This helps with issue 439 because Yices encounters some internal
divergence issue that is not stopped by the specified timeout
value (demonstrable by running the crux-llvm
test-data/golden/strlen_test2 with the Yices solver option).
This also helps provide timeout management for solvers that do not
provide a built-in timeout capability (like Boolector).