Repository navigation
fix: let the newer of two overlapping prompts win - #88
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`_
Two bugs that verify-session-cancel found: - Overlapping prompts of one session lost the cancel. When an older prompt returned, its cleanup deleted the sessionCancels entry, which by then held the newer prompt's cancel func. registerPrompt now returns a func that deletes the entry only while it is still that prompt's. - A session/cancel could cancel a prompt that the client sent after it. The inbound barrier starts a request while the running notification handler waits on the client, so a later prompt could register before an earlier cancel ran. Each entry now keeps the prompt's watermark, and cancelPrompt skips a prompt whose watermark is at or above the cancel's seq. This also covers an agent Cancel that calls the client. The skill reads both fixes as facts, so a revert fails check.sh. The replays move into agent_session_cancel_test.go as regression tests. _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_
Two bugs that verify-session-cancel found: - Overlapping prompts of one session lost the cancel. When an older prompt returned, its cleanup deleted the sessionCancels entry, which by then held the newer prompt's cancel func. registerPrompt now returns a func that deletes the entry only while it is still that prompt's. - A session/cancel could cancel a prompt that the client sent after it. The inbound barrier starts a request while the running notification handler waits on the client, so a later prompt could register before an earlier cancel ran. Each entry now keeps the prompt's watermark, and cancelPrompt skips a prompt whose watermark is at or above the cancel's seq. This also covers an agent Cancel that calls the client. The skill reads both fixes as facts, so a revert fails check.sh. The replays move into agent_session_cancel_test.go as regression tests. _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_
When the client sent two prompts of one session back to back, the newer prompt's handler often registered first. registerPrompt then let the older prompt cancel it, so the user's latest prompt ended at once and the stale turn kept running (284 of 300 runs). receive now numbers each request from the peer, and registerPrompt keeps a registered prompt that arrived later and cancels the older one at once. verify-session-cancel gets a third promise, NewerPromptSurvives, and a fact RegisterKeepsNewer. It also takes three review follow-ups: check.sh reads a changed peer-wait loop as DRIFT, the statechart labels name a pending cleanup or response, and two tests wait for the cancel handler instead of a timer. Both check.sh scripts give TLC its own temp folder, so parallel runs no longer race on /tmp/Naturals.tla. verify-notification-barrier moves its sync commit forward: receive only gained the counter, which the receive goroutine alone touches, and all 8 configs pass. Its line citations are remapped. _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_
…ix-newer-prompt-wins # Conflicts: # .agents/skills/verify-session-cancel/SKILL.md # .agents/skills/verify-session-cancel/SessionCancel.tla # .agents/skills/verify-session-cancel/cancel-waits-later-prompt.cfg # .agents/skills/verify-session-cancel/chart.cfg # .agents/skills/verify-session-cancel/check.sh # .agents/skills/verify-session-cancel/fingerprint.txt # .agents/skills/verify-session-cancel/one-prompt-at-a-time.cfg # .agents/skills/verify-session-cancel/overlapping-prompts.cfg # .agents/skills/verify-session-cancel/peer-wait-earlier-prompt.cfg # .agents/skills/verify-session-cancel/peer-wait-later-prompt.cfg # .agents/skills/verify-session-cancel/statechart-view.mjs # .agents/skills/verify-session-cancel/two-sessions.cfg # agent.go # agent_session_cancel_test.go
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. |
…late Adds the verifier's path for #88 and fixes the fact count in SKILL.md. _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: aa39304318
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
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".
Codex review of #88: registerPrompt compared only with the prompt that was registered. When the newer prompt registered, returned and cleaned up before a delayed older prompt registered, the older one ran with a live ctx. The agent now keeps the newest arrival per session in sessionNewest, and prunes it like the cancel markers: receive records each in-flight request's arrival, and an entry goes once no older request is in flight. The model gets OlderPromptEnds and the facts KeepNewerBy and NewestDropsWhen. The barrier skill's line citations are remapped from the original text, so ranges no longer run backward (Codex review). _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_
Member
Author
|
@codex review |
|
Codex Review: Didn't find any major issues. Hooray! 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". |
Review of #88: two range ends in the barrier SKILL.md kept their old numbers. The remap now uses git's diff hunks and also moves a number at the end of a sentence. All 129 citations hold the same code text as at the previous sync commit. New tests pin the early return in registerPrompt, the sessionNewest cap and the cleanup of the arrival state. Each one fails when its code is mutated. _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_
# Conflicts: # .agents/skills/verify-session-cancel/SKILL.md # .agents/skills/verify-session-cancel/SessionCancel.tla # .agents/skills/verify-session-cancel/check.sh # .agents/skills/verify-session-cancel/fingerprint.txt # .agents/skills/verify-session-cancel/overlapping-prompts.cfg # .agents/skills/verify-session-cancel/peer-wait-earlier-prompt.cfg # acp_test.go # agent.go # agent_session_cancel_test.go
Member
Author
|
@codex review |
|
Codex Review: Didn't find any major issues. Already looking forward to the next diff. 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. |
Review of #88: a weaker sessionNewest prune guard kept entries longer and no test failed. The new test registers a prompt with no older request in flight and asserts that no entry stays. _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_
Member
Author
|
@codex review |
|
Codex Review: Didn't find any major issues. Hooray! 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
Readiness review of #88: the PlainHandlerReturns row in the barrier SKILL.md cited the wrong lines since #73. Verifier note on #89: the Register row named the steps of registerPrompt out of order. _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 A `session/cancel` must cancel every prompt of its session that the client sent before it, and never one that it sent after it. The protocol defines `session/cancel` as a notification, but a client can send it as a request, with an id. The SDK then had no notification seq for it. It recorded no marker and canceled the registered prompt whenever it arrived. A verifier measured both harms on #88's code: in 300 runs of "prompt, then cancel request", the earlier prompt kept running 278 times. In 300 runs of "cancel request, then prompt", the later prompt was canceled 268 times. ## What - One clock: `receive` gives every request and every queued notification the next arrival number (`c.inboundMessages`). The number goes into the `handlingRequest` or `handlingNotification` ctx value, and `messageArrival` reads either one. - `cancelPrompt` and `registerPrompt` compare arrivals for both cancel forms. The cancel marker keeps the latest cancel: two cancel requests run on their own goroutines, and an older one that runs last must not lower it. - The clock replaces the watermark bookkeeping that only the cancel markers used. `inflightWatermarks`, `oldestInflightWatermark`, `requestWatermark` and the watermark in `promptCancel` are gone. The barrier still uses its watermark, which `receive` keeps as before. - `verify-session-cancel` models cancel requests (`cancel-requests.cfg`: prompts, two cancel requests and one cancel notification, 134,169 states) and reads a new fact, `MarkerKeepsLatest`. The model caught the marker overwrite before any test did. - `verify-notification-barrier` gets the new queue line and handler ctx line in `check.sh`, remapped citations and a new sync commit. Its model is unchanged, and all 8 configs pass. - The `PlainHandlerReturns` row in the barrier `SKILL.md` cited the wrong lines since #73. It now cites the `handlerCtx` and `handleInbound` lines. No protocol or schema change. `agent_gen.go` is unchanged. ## Tests - `TestAgentSideConnection_SessionCancelRequestIsOrdered` (both orders, 20 rounds each) fails on #88's code at round 0 and passes here at `-cpu 1,2,8`. - `TestAgentSideConnection_OlderCancelRequestKeepsLaterMarker` drives the two cancel requests in the bad order directly. It fails when the marker guard is a plain `if hasArrival {`. - `verify-session-cancel/check.sh`: 7 configs as expected, exit 0. With `MarkerKeepsLatest = FALSE`, `cancel-requests` breaks `CancelReachesEarlierPrompts`. `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 #88 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
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.
registerPromptthen 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-cancellisted the case as uncovered, and checking that gap found it.What
receivenumbers each request from the peer (c.inboundRequests, which only thereceivegoroutine touches) and puts the number in thehandlingRequestctx value.requestArrivalreads it.receivealso records each in-flight request's arrival (c.inflightArrivals), andoldestInflightArrivalreturns the smallest.sessionNewest).registerPromptcancels 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.pruneCancelMarkersdrops an entry once no older request is in flight, as it does for the cancel markers, with the same 1024 cap.verify-session-cancelgets two promises,NewerPromptSurvivesandOlderPromptEnds, and two facts,KeepNewerByandNewestDropsWhen. Removing the newest check makescheck.shexit 1. A changed prune guard gives DRIFT (exit 2), and the model shows that dropping entries too early breaksNewerPromptSurvives.check.shreads a changed peer-wait loop as DRIFT, not as a removed release.check.shscripts pass-Djava.io.tmpdirper run. Parallel TLC runs raced on/tmp/Naturals.tla, and one run failed with a parse error.verify-notification-barriermoves its sync commit forward.receiveonly gained the counter, so the barrier model is unchanged. All 8 configs pass, and theSKILL.mdline citations are remapped to the new lines.No protocol or schema change.
agent_gen.gois unchanged.Tests
TestAgentSideConnection_NewerPromptWinsWhicheverRegistersFirstandTestAgentSideConnection_PromptAfterCancelSurvivesLateOlderRegister(20 rounds per run) fail on fix: limit session/cancel to the prompts sent before it #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_SessionNewestIsCappedandTestAgentSideConnection_ArrivalStateDrainspin 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_OlderPromptEndsAfterNewerReturneddrivesregisterPromptdirectly for the path where the newer prompt returns before the older one registers. No black-box path can stall a handler that long.check.shexit 1 (KeepNewerBy = "never",overlapping-promptsbreaksNewerPromptSurvives) and fails 3 tests. A prune that never deletes fails the prune assertion. In the model,KeepNewerBy = "prev"(compare only with the registered entry) breaksOlderPromptEnds.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-sdkwire journeys (cancel-session, cancel-request, prompt-allow, prompt-reject, errors): 42 of 42 steps pass.Refs #72
#86 is merged.
Generated with
xum• Model:anthropic:claude-opus-5-5• Thinking:high