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

kore-rpc ending normally says user-interupted #317

Closed
ehildenb opened this issue Mar 30, 2023 · 5 comments
Closed

kore-rpc ending normally says user-interupted #317

ehildenb opened this issue Mar 30, 2023 · 5 comments

Comments

@ehildenb
Copy link
Member

Because we're sending SIGINT instead of SIGTERM to the kore-rpc, we're getting a weird message even on normal exit:

image

Could we instead, either:

  • Go back to SIGTERM, or
  • Add an explicit shutdown message to the RPC server that we call?

Related: #298
Related: runtimeverification/haskell-backend#3557

@tothtamas28
Copy link
Collaborator

The proper fix is to undo #298 , but for that the server needs to handle the SIGTERM signal gracefully.

@goodlyrottenapple
Copy link
Member

This is a known issue in the Haskell runtime system which seems unadressed to this day. There appear to be a couple of workarounds like this one: IntersectMBO/cardano-node#3641

However, can't tell whether this would actually prevent the error above from being thrown.

@jberthold
Copy link
Member

The proper fix is to undo #298 , but for that the server needs to handle the SIGTERM signal gracefully.

I think we should keep SIGINT, as only this will clean up all resources in the correct way. Translating SIGTERM to SIGINT internally as in the PR which @goodlyrottenapple found may be an option if for some reason we should not keep SIGINT, but I would not see why.

we're getting a weird message even on normal exit:

If the concern is just the appearance of an error in the logs, we can probably catch UserInterrupt and print something more comforting instead.

@tothtamas28
Copy link
Collaborator

tothtamas28 commented Mar 31, 2023

we can probably catch UserInterrupt and print something more comforting instead

If there's no simple way to process both SIGINT and SIGTERM on the backend, I'm fine with this workaround.

@ehildenb
Copy link
Member Author

I believe this is addressed at this point? I haven't seen the error message in logs for a while, and I am indeed comforted by that.

rv-jenkins pushed a commit that referenced this issue 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 issue 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 issue 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 issue 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 issue 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 issue 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 issue 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.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

4 participants