Exit STM workers quietly on lost master connection (flaky output/Partac.v on Windows CI) - #22286
Exit STM workers quietly on lost master connection (flaky output/Partac.v on Windows CI)#22286JasonGross wants to merge 1 commit into
Conversation
When the master tears down a worker's channels, the worker does not
always observe End_of_file: on Windows the socket read fails with
WSAECONNRESET ("An existing connection was forcibly closed by the
remote host") or WSAECONNABORTED, and on Unix a write to the dead
master fails with EPIPE ("Broken pipe"), all surfacing as Sys_error
(possibly wrapped in MarshalError). These took the loud "Slave:
critical exception" / "Fatal marshal error" branches of the worker
main loop instead of the quiet "connection lost" one, and the message
races into the master's output, e.g. making output/Partac.v fail
intermittently on Windows CI:
260:tactic:1:1:0] Slave: critical exception: System error:
"An existing connection was forcibly closed by the remote host."
Treat connection-loss Sys_errors like End_of_file.
Co-Authored-By: Claude Fable 5 <[email protected]>
Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
coqbot-app
Bot
added
the
needs: full CI
| 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 -> |
There was a problem hiding this comment.
Grepping the error message is below my standards, also because these things are translated using LOCALE.
Just catch any Sys_error.
| CEphemeron.clean () | ||
| with | ||
| | MarshalError s when connection_lost s -> | ||
| stm_prerr_endline "connection lost"; flush_all (); exit 2 |
There was a problem hiding this comment.
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.
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.
I don't understand how printing "connection lost" is less flaky than printing "marshall error whatever"
There was a problem hiding this comment.
Please avoid spamming PRs, you can just link to your branch instead
There was a problem hiding this comment.
I don't understand how printing "connection lost" is less flaky than printing "marshall error whatever"
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?)
Please avoid spamming PRs, you can just link to your branch instead
Apologies, and noted for the future.
There was a problem hiding this comment.
My understanding is that sometimes we get the message and sometimes we don't
There was a problem hiding this comment.
Well, if there is a test depending on the string, we can change it depending on the error code. That is fine to me.
3 participants
Written by Claude (Anthropic AI) at the request of and under the supervision of @JasonGross.
Problem
STM workers whose master goes away do not always see
End_of_file. On Windows, the master closing the socket is observed by the worker's blocking read as WSAECONNRESET ("An existing connection was forcibly closed by the remote host.") or WSAECONNABORTED; on Unix, a write (e.g. of feedback) to a dead master fails with EPIPE ("Broken pipe"). All of these surface asSys_error— possibly wrapped inMarshalErrorby the (un)marshalling helpers — and take the loudSlave: critical exception:/Fatal marshal error:branches of the worker main loop instead of the quietconnection lostone.The loud message races into the master's output. Concretely, this makes
output/Partac.vfail intermittently on Windows CI (seen on this run for #22266, whose diff is unrelated Ltac2 stdlib additions):Fix
Recognize the connection-loss
Sys_errortexts (ECONNRESET/EPIPE/WSAECONNRESET/WSAECONNABORTED) in the worker main loop, in both the rawSys_errorposition and theMarshalError-wrapped position, and exit through the same quiet path asEnd_of_file(the message is still printed with-debug misc, likeconnection losttoday). Real worker crashes keep the loud reporting.The strings are matched on the strerror text since the exceptions come out of
in_channel/out_channeloperations asSys_errorrather thanUnix.Unix_error.🤖 Generated with Claude Code
https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw