Skip to content
This repository has been archived by the owner on Apr 25, 2024. It is now read-only.

Kill kore-rpc with SIGINT instead of SIGTERM #298

Merged
merged 3 commits into from
Mar 24, 2023
Merged

Conversation

tothtamas28
Copy link
Collaborator

@tothtamas28 tothtamas28 self-assigned this Mar 24, 2023
@tothtamas28 tothtamas28 marked this pull request as ready for review March 24, 2023 15:03
@rv-jenkins rv-jenkins merged commit 48b4ea9 into master Mar 24, 2023
@rv-jenkins rv-jenkins deleted the kore-rpc-kill branch March 24, 2023 15:25
@jberthold
Copy link
Member

jberthold commented Mar 26, 2023

Thanks for changing this! Besides the issues with remaining temporary directories, we also could not get profiling data from the back-end when it was killed forcefully. Using SIGINT is the recommended way to terminate a backend program gracefully.

rv-jenkins pushed a commit that referenced this pull request Mar 28, 2024
Closes runtimeverification/kontrol#375.

Related: #298,
#317

Using `SIGINT` or a [SIGTERM
handler](runtimeverification/hs-backend-booster@bc7c1b0)
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.

---------

Co-authored-by: devops <devops@runtimeverification.com>
PetarMax pushed a commit that referenced this pull request Mar 28, 2024
Closes runtimeverification/kontrol#375.

Related: #298,
#317

Using `SIGINT` or a [SIGTERM
handler](runtimeverification/hs-backend-booster@bc7c1b0)
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.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 9, 2024
Closes runtimeverification/kontrol#375.

Related: runtimeverification/pyk#298,
runtimeverification/pyk#317

Using `SIGINT` or a [SIGTERM
handler](runtimeverification/hs-backend-booster@bc7c1b0)
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.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 9, 2024
…on/pyk#298)

Workaround for
runtimeverification/haskell-backend#3557

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 9, 2024
Closes runtimeverification/kontrol#375.

Related: runtimeverification/pyk#298,
runtimeverification/pyk#317

Using `SIGINT` or a [SIGTERM
handler](runtimeverification/hs-backend-booster@bc7c1b0)
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.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 9, 2024
…on/pyk#298)

Workaround for
runtimeverification/haskell-backend#3557

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 9, 2024
Closes runtimeverification/kontrol#375.

Related: runtimeverification/pyk#298,
runtimeverification/pyk#317

Using `SIGINT` or a [SIGTERM
handler](runtimeverification/hs-backend-booster@bc7c1b0)
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.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 10, 2024
…on/pyk#298)

Workaround for
runtimeverification/haskell-backend#3557

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 10, 2024
Closes runtimeverification/kontrol#375.

Related: runtimeverification/pyk#298,
runtimeverification/pyk#317

Using `SIGINT` or a [SIGTERM
handler](runtimeverification/hs-backend-booster@bc7c1b0)
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.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 10, 2024
…on/pyk#298)

Workaround for
runtimeverification/haskell-backend#3557

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 10, 2024
Closes runtimeverification/kontrol#375.

Related: runtimeverification/pyk#298,
runtimeverification/pyk#317

Using `SIGINT` or a [SIGTERM
handler](runtimeverification/hs-backend-booster@bc7c1b0)
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.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants