Bound the frame write so a wedged server cannot freeze the client - #10
Conversation
![cubic-dev-ai[bot]](https://avatars.githubusercontent.com/in/1082092?s=60&v=4){kind=small}
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
Fixed in bb239e3: the transport now poisons itself on any write that did With the fix the same experiment fails the second send in 7.8 µs and the |
There was a problem hiding this comment.
2 issues found across 1 file
Prompt for AI agents (unresolved issues)
Check if these issues are valid — if so, understand the root cause of each and fix them. If appropriate, use sub-agents to investigate and fix each issue separately.
<file name="src/frama-c/transport.rs">
<violation number="1" location="src/frama-c/transport.rs:45">
P2: When a request timeout is shorter than 10 seconds, a backpressured POLL write can exceed that deadline and return only after `WRITE_TIMEOUT`. Pass the remaining request duration to the frame write and cap it at `WRITE_TIMEOUT` so the poll loop enforces its caller's timeout.</violation>
<violation number="2" location="src/frama-c/transport.rs:91">
P1: After a regular client operation times out while writing, the first `reload_project` cannot recover the session. `ensure_main_spawned` still sees `MainFramaCState.poisoned == false`, attempts an in-place reload on this poisoned transport, returns `BrokenPipe`, and only then marks the state poisoned; propagate transport failure to the session state or respawn when this transport is poisoned.</violation>
</file>
Reply with feedback, questions, or to request a fix.
Re-trigger cubic
| /// completion can have left a partial frame in the socket, and no | ||
| /// later frame may follow it on this stream. | ||
| async fn poison(&mut self, error: FramaCError) -> FramaCError { | ||
| self.poisoned = true; |
There was a problem hiding this comment.
P1: After a regular client operation times out while writing, the first reload_project cannot recover the session. ensure_main_spawned still sees MainFramaCState.poisoned == false, attempts an in-place reload on this poisoned transport, returns BrokenPipe, and only then marks the state poisoned; propagate transport failure to the session state or respawn when this transport is poisoned.
Prompt for AI agents
Check if this issue is valid — if so, understand the root cause and fix it. At src/frama-c/transport.rs, line 91:
<comment>After a regular client operation times out while writing, the first `reload_project` cannot recover the session. `ensure_main_spawned` still sees `MainFramaCState.poisoned == false`, attempts an in-place reload on this poisoned transport, returns `BrokenPipe`, and only then marks the state poisoned; propagate transport failure to the session state or respawn when this transport is poisoned.</comment>
<file context>
@@ -56,4 +82,22 @@ impl Transport {
+ /// completion can have left a partial frame in the socket, and no
+ /// later frame may follow it on this stream.
+ async fn poison(&mut self, error: FramaCError) -> FramaCError {
+ self.poisoned = true;
+ let _ = self.stream.shutdown().await;
+ error
</file context>
| let frame = codec::encode_frame(payload); | ||
| self.stream.write_all(&frame).await?; | ||
| Ok(()) | ||
| match tokio::time::timeout(WRITE_TIMEOUT, self.stream.write_all(&frame)).await { |
There was a problem hiding this comment.
P2: When a request timeout is shorter than 10 seconds, a backpressured POLL write can exceed that deadline and return only after WRITE_TIMEOUT. Pass the remaining request duration to the frame write and cap it at WRITE_TIMEOUT so the poll loop enforces its caller's timeout.
Prompt for AI agents
Check if this issue is valid — if so, understand the root cause and fix it. At src/frama-c/transport.rs, line 45:
<comment>When a request timeout is shorter than 10 seconds, a backpressured POLL write can exceed that deadline and return only after `WRITE_TIMEOUT`. Pass the remaining request duration to the frame write and cap it at `WRITE_TIMEOUT` so the poll loop enforces its caller's timeout.</comment>
<file context>
@@ -17,19 +33,29 @@ impl Transport {
let frame = codec::encode_frame(payload);
- self.stream.write_all(&frame).await?;
- Ok(())
+ match tokio::time::timeout(WRITE_TIMEOUT, self.stream.write_all(&frame)).await {
+ Ok(Ok(())) => Ok(()),
+ Ok(Err(e)) => Err(self.poison(FramaCError::Io(e)).await),
</file context>
There was a problem hiding this comment.
1 existing issue remains and 1 new issue found across 1 file
Prompt for AI agents (unresolved issues)
Check if these issues are valid — if so, understand the root cause of each and fix them. If appropriate, use sub-agents to investigate and fix each issue separately.
<file name="src/frama-c/transport.rs">
<violation number="1" location="src/frama-c/transport.rs:57">
P2: A wedged-write timeout is reported as `FramaCError::Timeout`, which `src/error.rs` maps to diagnostic code `WpTimeout` and the `mcp_server_timeout` triage message "The MCP request timed out before a WP goal reported prover timeout." That misclassifies this new failure: the cause is a stuck socket write and a now-poisoned transport that needs a Frama-C respawn, not a WP prover timeout. The PR notes users must recover by restarting/respawning, but the surfaced diagnostic actively points them at a prover timeout instead. Use a distinct error (or an `Io` error with `ErrorKind::TimedOut`) so the write/poison path is diagnosable apart from a genuine WP timeout.</violation>
</file>
Requires human review: Auto-approval blocked because this review re-detected 1 unresolved issue already reported by Cubic.
Re-trigger cubic
| match tokio::time::timeout(WRITE_TIMEOUT, self.stream.write_all(&frame)).await { | ||
| Ok(Ok(())) => Ok(()), | ||
| Ok(Err(e)) => Err(self.poison(FramaCError::Io(e)).await), | ||
| Err(_) => Err(self.poison(FramaCError::Timeout(WRITE_TIMEOUT)).await), |
There was a problem hiding this comment.
P2: A wedged-write timeout is reported as FramaCError::Timeout, which src/error.rs maps to diagnostic code WpTimeout and the mcp_server_timeout triage message "The MCP request timed out before a WP goal reported prover timeout." That misclassifies this new failure: the cause is a stuck socket write and a now-poisoned transport that needs a Frama-C respawn, not a WP prover timeout. The PR notes users must recover by restarting/respawning, but the surfaced diagnostic actively points them at a prover timeout instead. Use a distinct error (or an Io error with ErrorKind::TimedOut) so the write/poison path is diagnosable apart from a genuine WP timeout.
Prompt for AI agents
Check if this issue is valid — if so, understand the root cause and fix it. At src/frama-c/transport.rs, line 57:
<comment>A wedged-write timeout is reported as `FramaCError::Timeout`, which `src/error.rs` maps to diagnostic code `WpTimeout` and the `mcp_server_timeout` triage message "The MCP request timed out before a WP goal reported prover timeout." That misclassifies this new failure: the cause is a stuck socket write and a now-poisoned transport that needs a Frama-C respawn, not a WP prover timeout. The PR notes users must recover by restarting/respawning, but the surfaced diagnostic actively points them at a prover timeout instead. Use a distinct error (or an `Io` error with `ErrorKind::TimedOut`) so the write/poison path is diagnosable apart from a genuine WP timeout.</comment>
<file context>
@@ -17,19 +42,29 @@ impl Transport {
+ match tokio::time::timeout(WRITE_TIMEOUT, self.stream.write_all(&frame)).await {
+ Ok(Ok(())) => Ok(()),
+ Ok(Err(e)) => Err(self.poison(FramaCError::Io(e)).await),
+ Err(_) => Err(self.poison(FramaCError::Timeout(WRITE_TIMEOUT)).await),
+ }
}
</file context>
|
Thank @Suzu1Dev for contributing! |
2 participants
Problem
Transport::send_frame(src/frama-c/transport.rs) writes withwrite_alland no timeout. Every send happens while holding theFramaCClientmutex, and the poll loop that enforces request timeouts sends through this same path every 100 ms. If the Frama-C process stops draining its socket (wedged in a computation or a deadlocked plugin), the kernel socket buffer fills with poll frames,write_allblocks forever, and the client mutex is never released. Every later MCP tool call then blocks on that mutex: the server freezes silently, and the very mechanism meant to bound request time is what deadlocks.Reproduction
A Unix-socket peer that accepts and never reads stands in for a wedged Frama-C. Driving
Transport::send_framewith 1 MiB frames:Operation timeout after 10sat 10.0 sFix
Wrap the write in a 10 s
tokio::time::timeoutand surfaceFramaCError::Timeouton expiry. 10 s is far above any legitimate stall: a healthy server drains its socket promptly and the poll frames are tens of bytes. On the reload path the existing poison logic inensure_main_spawnedrespawns the instance; other tools now surface the timeout to the caller instead of hanging forever.Testing
cargo clippy --all-targetscleanSummary by cubic
Bounded the frame write in
Transport::send_framewith a 10-second timeout so a wedged Frama-C server can't freeze the client. Previouslywrite_allhad no timeout; a stalled write blocked forever while holding the client mutex, freezing every later request including the poll loop that enforces timeouts. Becausewrite_allisn't cancellation-safe, a timed-out or failed write now poisons the transport — it returnsFramaCError::Timeout, shuts down the socket, and every later call fails fast with a BrokenPipe error instead of corrupting the length-prefixed protocol.Recovery requires a new
Transport, and the respawn is only partially automatic:ensure_main_spawneddecides in-place vs respawn fromMainFramaCStatealone, so a reload with explicit files respawns only on the second attempt, and sandbox clients have no respawn path at all.Written for commit 0f86023. Summary will update on new commits.