search

runtimeverification / pyk

Python tools for the K Framework
BSD 3-Clause "New" or "Revised" License
13 stars 2 forks source link

Use `SIGTERM` to stop server #1034

Closed palinatolmach closed 7 months ago

palinatolmach commented 7 months ago

Closes https://github.com/runtimeverification/kontrol/issues/375.

Related: https://github.com/runtimeverification/pyk/pull/298, https://github.com/runtimeverification/pyk/issues/317

Using SIGINT or a SIGTERM handler causes some sort of a deadlock in the booster, making Kontrol hang. Based on our experiments, switching to SIGTERM seems to fix this issue.

The disadvantage, as mentioned by @goodlyrottenapple and @jberthold, is that we won't get the SMT transcript or any other logs that haven't been flushed to file when the SIGTERM is received; however, it would address a major usability issue in view of the upcoming workshop next week, at least as a temporary solution.

goodlyrottenapple commented 7 months ago

Could we make the SIGTERM conditional on e.g. verbosity or the smt transcript option? That way we mitigate most of the downsides of using SIGTERM

palinatolmach commented 7 months ago

Thanks @goodlyrottenapple and @tothtamas28! I modified it to send SIGINT if --solver-transcript is present in server command, and use terminate() otherwise. It'd be cleaner if --solver-transcript was exposed as an option in pyk and a field in KoreServer — I'll open a separate issue on it, if that's ok. Update: done — https://github.com/runtimeverification/k/issues/4176.