You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The function halt_execution is supposed to halt the execution asap. However, the current halt_execution function doesn't seem to force the solver to terminate. When the solver timeout is set to a very large amount and the query generated somehow takes a long time to compute, halt_execution is not working if KLEE got stuck in solver call. If watchdog is enabled, it would just result in SIGKILL which should be improved. A solution to address this for forked solver mode is to simply send signal to the forked solver pid.
The text was updated successfully, but these errors were encountered:
@251 Good point. There's no comment or documentation that I can see for halt_execution, so in OP I described the expected behavior of this function. What you've described is exactly the current behavior which is not consistent with my expectation. In any case, the statement that watchdog should be improved to terminate gracefully when stuck in solver class should still be correct. With your comment, the potential solutions are:
let halt_execution kill the solver
implement another function that watchdog will call when halt_execution doesn't halt the execution within watchdog's timeout
@251 Do you agree and may I know if you have plan to address this?
The function
halt_execution
is supposed to halt the execution asap. However, the currenthalt_execution
function doesn't seem to force the solver to terminate. When the solver timeout is set to a very large amount and the query generated somehow takes a long time to compute,halt_execution
is not working if KLEE got stuck in solver call. If watchdog is enabled, it would just result in SIGKILL which should be improved. A solution to address this for forked solver mode is to simply send signal to the forked solver pid.The text was updated successfully, but these errors were encountered: