Repository navigation
verify-session-cancel: add a TLA+ check of session/cancel handling - #85
Merged
Merged
Conversation
A session/cancel must cancel every prompt of its session that the client sent before it, whichever handler runs first, and must not cancel a prompt that the client sent after it. The new skill model-checks both promises for cancelPrompt, registerPrompt and pruneCancelMarkers, the generated session/prompt and session/cancel cases, and the parts of receive and the inbound barrier that they rely on. check.sh reads four facts from the code, refuses to run when a shape that the model assumes changes, and fingerprints the covered code. replay.sh replays each counterexample against the real code. The current code breaks both promises. check.sh expects these results: - Overlapping prompts lose the cancel (#83, #72 item 4). - The peer-wait release lets a cancel hit a later prompt (#72 item 1), also when the agent's Cancel calls the client. The barrier and wire-level skills now point at the new skill. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_
Member
Author
|
@codex review |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
Codex Review: Didn't find any major issues. 👍 Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
Member
Author
|
@codex security review |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
ThomasK33
added a commit
that referenced
this pull request
Nov 5, 2026
## Why A `session/cancel` must cancel every prompt of its session that the client sent before it, and must leave alone a prompt that the client sent after it. `verify-session-cancel` (#85) found that the SDK breaks both promises. Agent authors see it this way: - The user stops a turn while a second prompt of the session is in flight, and the agent keeps working. - A notification handler (or the agent's own `Cancel`) calls the client, and the next prompt the user sends ends at once as canceled. ## What - `registerPrompt` stores a `promptCancel` per session: the cancel func plus the prompt's request watermark. It returns a func that the `session/prompt` case calls when `Prompt` returns. That func deletes the entry only while it is still this prompt's, so a newer prompt stays cancellable. - `cancelPrompt` skips a registered prompt whose watermark is at or above the cancel's seq. The client sent that prompt after the cancel. The barrier starts such a prompt early while the running notification handler waits on the client. - The emitter (`WriteDispatchJen`) writes the new `donePrompt` call, and `agent_gen.go` is regenerated. Only the `session/prompt` case changes. - `verify-session-cancel` reads both fixes as facts (`CleanupChecksOwner`, `CancelSkipsLaterPrompt`), so a revert makes `check.sh` fail. All six configs now expect a pass. The overlapping-prompts config is wider: 3 prompts, 2 cancels and a handler that waits on the client. - The three replays move into `agent_session_cancel_test.go` as regression tests. No protocol or schema change. ## Tests - The three new tests fail on main's product code (3 of 3) and pass on this branch (10 runs, and 3 more runs of the package with `-race`). - Mutation checks: reverting the watermark guard makes `check.sh` exit 1 and fails both `...SparesPromptReleasedBy...` tests. Reverting the owner check makes `check.sh` exit 1 and fails `TestAgentSideConnection_OverlappingPromptsKeepCancel`. - `check.sh`: 6 configs as expected, covered code matches `fingerprint.txt`, exit 0. - `verify-acp-go-sdk` wire journeys on binaries built from this branch: cancel-session, cancel-request, prompt-allow and errors, 36 of 36 steps pass. - `make test`, gofmt, shellcheck, and treefmt without mdsh: pass. Fixes #83 Refs #72 (items 1 and 4) Merge after #85. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_
ThomasK33
added a commit
that referenced
this pull request
Nov 5, 2026
## Why When a client sends two prompts of one session back to back, the newer prompt must replace the older one. The SDK did the opposite most of the time. Each prompt runs on its own goroutine, and the newer one usually registered first. `registerPrompt` then let the older prompt cancel it. The user's latest prompt ended at once as canceled, and the stale turn kept working. A probe on #86's code hit this in 284 of 300 runs. Main has the same bug. `verify-session-cancel` listed the case as uncovered, and checking that gap found it. ## What - `receive` numbers each request from the peer (`c.inboundRequests`, which only the `receive` goroutine touches) and puts the number in the `handlingRequest` ctx value. `requestArrival` reads it. `receive` also records each in-flight request's arrival (`c.inflightArrivals`), and `oldestInflightArrival` returns the smallest. - The agent keeps the newest registered arrival per session (`sessionNewest`). `registerPrompt` cancels a prompt at once when a later prompt of the session has registered, even one that has already returned. Otherwise it replaces the registered prompt, as before. `pruneCancelMarkers` drops an entry once no older request is in flight, as it does for the cancel markers, with the same 1024 cap. - `verify-session-cancel` gets two promises, `NewerPromptSurvives` and `OlderPromptEnds`, and two facts, `KeepNewerBy` and `NewestDropsWhen`. Removing the newest check makes `check.sh` exit 1. A changed prune guard gives DRIFT (exit 2), and the model shows that dropping entries too early breaks `NewerPromptSurvives`. - Follow-ups from the #85 readiness review: - `check.sh` reads a changed peer-wait loop as DRIFT, not as a removed release. - The statechart labels name a pending cleanup or response. - Two tests wait until the cancel handler returns, instead of a 1-second timer. - Both `check.sh` scripts pass `-Djava.io.tmpdir` per run. Parallel TLC runs raced on `/tmp/Naturals.tla`, and one run failed with a parse error. - `verify-notification-barrier` moves its sync commit forward. `receive` only gained the counter, so the barrier model is unchanged. All 8 configs pass, and the `SKILL.md` line citations are remapped to the new lines. No protocol or schema change. `agent_gen.go` is unchanged. ## Tests - `TestAgentSideConnection_NewerPromptWinsWhicheverRegistersFirst` and `TestAgentSideConnection_PromptAfterCancelSurvivesLateOlderRegister` (20 rounds per run) fail on #86's code within the 20 rounds, mostly at round 0, and pass on this branch, 5 runs each at `-cpu 1,2,8`. - `TestAgentSideConnection_LateOlderPromptKeepsNewerCancellable`, `TestAgentSideConnection_SessionNewestIsCapped` and `TestAgentSideConnection_ArrivalStateDrains` pin the early return, the 1024-entry cap and the cleanup of the arrival state. Each one fails when its part of the code is mutated. - `TestAgentSideConnection_OlderPromptEndsAfterNewerReturned` drives `registerPrompt` directly for the path where the newer prompt returns before the older one registers. No black-box path can stall a handler that long. - Mutation checks: removing the newest check makes `check.sh` exit 1 (`KeepNewerBy = "never"`, `overlapping-prompts` breaks `NewerPromptSurvives`) and fails 3 tests. A prune that never deletes fails the prune assertion. In the model, `KeepNewerBy = "prev"` (compare only with the registered entry) breaks `OlderPromptEnds`. - The two rewritten tests still fail on main's code. - `verify-session-cancel/check.sh`: 6 configs as expected, exit 0. `replay.sh`: 0 replays, exit 0. `verify-notification-barrier/check.sh`: 8 configs pass. - `make test`, `go test -race -count=3 .`, the generator (no change), gofmt, shellcheck, and treefmt without mdsh: pass. - `verify-acp-go-sdk` wire journeys (cancel-session, cancel-request, prompt-allow, prompt-reject, errors): 42 of 42 steps pass. Refs #72 #86 is merged. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Why
A
session/cancelmust cancel every prompt of its session that the client sent before it, whichever handler runs first. It must also leave alone a prompt that the client sent after it. Unit tests reach only a few of the orders in which the cancel handler and the prompt handlers can run. This PR adds a project-local skill that model-checks both promises with TLA+ (TLC), so the next change to this code can be checked against them.What
New skill
.agents/skills/verify-session-cancel:SessionCancel.tla: a model ofcancelPrompt,registerPrompt,pruneCancelMarkers, the generatedsession/promptandsession/cancelcases, and the parts ofreceiveand the inbound barrier that they rely on.check.sh: reads four facts from the code, refuses to run (DRIFT) when a code shape that the model assumes changes, and fingerprints 19 covered code blocks (STALE on any other change). It runs six configs in about 10 seconds.replay.shandreplay_test.go: replay each counterexample against the real code.statechart-view.mjsandchart.cfg: labels for reading results with/statechart.verify-notification-barrierandverify-acp-go-sdknow point at the new skill.No product code changes. The skill records three findings as expected results, so
check.shexits 0 on main today:Cancelcalls the client.Each replay fails 10 of 10 runs on main and passes on a scratch fix. Follow-up PRs fix them and flip the expected results to pass.
Tests
check.sh: 6 configs as expected, covered code matchesfingerprint.txt, exit 0.SKILL.mddescribes.make test, gofmt, shellcheck, and treefmt without mdsh (mdsh is not installed on my host): pass.Refs #72
Refs #83
Generated with
xum• Model:anthropic:claude-opus-5-5• Thinking:high