-
Notifications
You must be signed in to change notification settings - Fork 744
Exit STM workers quietly on lost master connection (flaky output/Partac.v on Windows CI) #22286
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Open
JasonGross
wants to merge
1
commit into
rocq-prover:master
Choose a base branch
from
JasonGross:quiet-worker-connection-loss
base: master
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
+18
−0
Open
Changes from all commits
Commits
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -282,6 +282,20 @@ module Make(T : Task) () = struct | |
| let slave_handshake () = | ||
| Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc) | ||
|
|
||
| (* The master going away while we read from or write to it is not | ||
| always observed as [End_of_file]: reads can fail with a connection | ||
| reset (in particular on Windows, where the master closing the | ||
| socket resets it) and writes with a broken pipe, both showing up | ||
| as [Sys_error] with the corresponding strerror text. *) | ||
| let connection_lost msg = | ||
| let contains what = CString.string_contains ~where:msg ~what in | ||
| contains "Connection reset by peer" || | ||
| contains "Broken pipe" || | ||
| (* WSAECONNRESET *) | ||
| contains "forcibly closed by the remote host" || | ||
| (* WSAECONNABORTED *) | ||
| contains "aborted by the software in your host machine" | ||
|
|
||
| let pp_pid pp = Pp.(str (Spawned.process_id () ^ " ") ++ pp) | ||
|
|
||
| let debug_with_pid = Feedback.(function | ||
|
|
@@ -309,10 +323,14 @@ module Make(T : Task) () = struct | |
| marshal_response (Option.get !slave_oc) response; | ||
| CEphemeron.clean () | ||
| with | ||
| | MarshalError s when connection_lost s -> | ||
| stm_prerr_endline "connection lost"; flush_all (); exit 2 | ||
| | MarshalError s -> | ||
| stm_pr_err Pp.(prlist str ["Fatal marshal error: "; s]); flush_all (); exit 2 | ||
| | End_of_file -> | ||
| stm_prerr_endline "connection lost"; flush_all (); exit 2 | ||
| | Sys_error s when connection_lost s -> | ||
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Grepping the error message is below my standards, also because these things are translated using LOCALE. Just catch any |
||
| stm_prerr_endline "connection lost"; flush_all (); exit 2 | ||
| | e -> | ||
| stm_pr_err Pp.(seq [str "Slave: critical exception: "; print e]); | ||
| flush_all (); exit 1 | ||
|
|
||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Here as well, I don't see the advantage of printing "connection lost" over "marshal error" and returning the same error code. please remove this hunk.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I guess the alternative is adapting the test-suite runner to filter out these sorts of messages so that the test involving par is less flaky on Windows? Or adding support for expect tests with multiple alternatives and adding all the various alternatives we might see? I'll have Fable prepare two alternate PRs for each of these strategies, we can see which one is better
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't understand how printing "connection lost" is less flaky than printing "marshall error whatever"
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please avoid spamming PRs, you can just link to your branch instead
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
My understanding of the flakiness is that the behavior of the test is always the same, but the error message varies depending on thread interleaving. (Does this seem correct?)
Apologies, and noted for the future.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
My understanding is that sometimes we get the message and sometimes we don't
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Well, if there is a test depending on the string, we can change it depending on the error code. That is fine to me.