Repository navigation
fix(server): do not drop a live Claude on a late keepalive tick - #479
Merged
Merged
Conversation
libuv runs timers before it reads sockets. A ping timer tick that Neovim runs late after a block of 1.0 to 1.5 intervals is not a wake (the wake reset needs more than 1.5 intervals), and it finds the pong of the last ping still unread: now - last_pong is about 2.3 intervals, above the timeout, so the client was dropped with 1011 although it answers every ping. The first tick that finds no pong for two intervals now pings again and sets client.pong_overdue. The next tick finds the pong that was read in between, or drops the client. A pong clears pong_overdue at the next tick. A client that never answers is dropped one tick later than before.
Member
Author
|
@codex review |
Member
Author
|
@codex security review |
Codex Review Summary: ✅ CompletedThis 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. Swish! 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". |
🛡️ 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 10, 2026
#479 said that libuv runs timers before it reads sockets, which is too general. A tick that Neovim runs late can run before the socket read after any block on Neovim 0.8. On newer Neovim it does so only after a block inside a libuv callback that runs after the poll phase (a check callback), and not after a block in vim.schedule, which reads the socket first (checked on 0.12.3 and 0.8.3). Fix the sentence in the pong_overdue comment, the server README and the unit test, and wrap two lines to 120 columns.
ThomasK33
added a commit
that referenced
this pull request
Nov 10, 2026
#479 changed the ping timer: the first tick that finds no pong for two intervals pings again and sets client.pong_overdue, and only the second drops the client. The model now has the step the first version could not see. - TimerTicksLate (LateTickAfterPing): a tick delayed by 1.0 to 1.5 intervals, below the wake threshold, with Claude's pong still unread. TickOne takes a mode ("normal", "late" or "wake"). A block does not count as awake time. - The variable overdue is client.pong_overdue. The facts DropsOnSecondOverdueTick and AliveTickClearsOverdue are caught by NoFalseTimeout, which needs two delayed ticks (MaxSleeps = 2). - SKILL.md: the NoFalseTimeout sentence says "second tick in a row", the bug list has a fourth entry (fixed in #479), and the stale "baseline" sentence of --mutants is gone. - New replay short-block-after-ping.lua: a 1.3-interval block in a check callback, right after a ping. BROKEN on b65d266, KEPT on main.
ThomasK33
added a commit
that referenced
this pull request
Nov 10, 2026
…ection covered.lock files The diff-lifecycle record changes only for client.lua and tcp.lua, whose edits are comments. The ws record also covers the new fail-safe branch of the ping timer that #479 added, which the model now describes.
ThomasK33
added a commit
that referenced
this pull request
Nov 10, 2026
… the #479 merge Only the file hashes of init.lua and server/client.lua changed. The queue code calls no diff function, and the client.lua change is outside create_client. check.sh passes.
This was referenced Nov 10, 2026
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 12, 2026
) ## Why Goal: a Claude that answers every ping but never reads must not pin Neovim's memory. Today it does. The ping timer drops a client only when no pong arrived for `interval * 2`. Replies and pings that this client never reads wait in libuv's write queue, which is Neovim's memory, and nothing bounds that queue. A probe on current main grew the queue to 118,225,574 bytes in 30 s (Neovim RSS about 222 MB), and the client was never closed. A local client needs the lock-file auth token to do this, but a Claude whose reader stalls while its pong path still runs does the same. ## The rule **A client that answers its pings is closed, and its queue goes with it, when its libuv write queue shows no progress at two ping ticks in a row and still shows none right after libuv's next poll.** Three terms: - A *tick* is one run of the ping timer (every 30 s by default). - *Progress* means libuv wrote at least one more byte of the client's queue since the last progress, or the queue is empty. - A *poll* is the step of the libuv loop where libuv asks the operating system which sockets are ready. Two places use the idea of "no write progress": 1. The ping timer applies the rule above to every connected client. 2. A deadline applies a simpler rule to a Close frame that waits in the queue. A client that broke the protocol, or that `stop_server` closed, has left `server.clients`, so the ping timer cannot see it. Without the deadline a Claude that never reads kept that socket and its queue until Neovim exited. That was the limit that coder#455 wrote into the server README. `client.close_timer` is a repeating timer, one `keepalive_timeout` long, that runs while `client.close_pending` is set. A socket that wrote no byte of its queue in that window is closed, and the queue with it. The bound is time without write progress, never queue size. A cap on size drops a live Claude that receives one large openDiff payload. The window is two ticks, so no new constant exists. The default is 60 s to 90 s after the last actual write progress. The next tick records that progress. The following two ticks find no further progress, and the second confirms the stall after the next poll. That holds for ticks that come late by less than 1.5 intervals, plus their delay. The wake rule below covers later ticks. The ping timer closes with Close 1011 and disconnect 1006 through the existing disconnect path (`_disconnect_client`, then `on_disconnect`), so pending diffs of that client are rejected as for any disconnect. The Close-frame deadline closes only the socket. The frame keeps its original status, which is the protocol error's status or 1001 from `stop_server`. The pending diffs of that client were already rejected by then. In both cases the Close frame cannot reach the peer, because it waits behind the queue. Closing the socket drops it. ## Why the drop waits for a look after the next poll The pushed head (`8fe3c19`) closed a client when its queue showed no progress for `interval * 2`. That can close a Claude that reads. libuv learns that a socket can take more bytes only in its poll step. Neovim can run the ping tick right after its main loop was blocked inside an I/O callback, and that tick runs before the poll that reports what Claude read during the block. A Claude that resumed reading then shows no progress, although it reads. In a real-socket probe the pushed head closed such a reader after 4.00 MB read (first table below). coder#479, merged to main, fixed the same kind of false drop for the pong rule by giving a late tick a second chance. Two earlier attempts at the same defect failed in verification. Both stayed on local heads and were never pushed. The later one is the "5% head" (`9a0d8d4`) in the tables below. They excused a late tick, meaning a tick more than 1.05 intervals after the one before it. Two independent verifiers found two holes: 1. A tick that comes within 5% after its due time is not late by that rule, and it can still run before the poll. A real-socket probe let a reader resume during a 500 ms block inside an I/O callback. The reader read 1.61 MB from the socket, and that head still closed it ("Write queue stalled"). That happened on Neovim 0.12.3 and on 0.8.0, at a 5 s interval and at the default 30 s. 2. A tick that is late every time never counts, so a stalled client stayed past the bound. One verifier kept a stalled client for 126 s with callbacks of about 2 s. This head has no lateness rule. When the second tick in a row finds no progress, the tick sends its ping as usual and calls `after_next_poll` (`tcp.lua`). That function starts two libuv handles: - a *check* handle, which libuv runs right after every poll step, in every libuv version, and - an *idle* handle, which keeps that poll from waiting for a timer or a socket. The check callback closes both handles, takes them off `server.pending_polls`, samples the queue once more, and closes the client only if there is still no progress. A client that left or started to leave in the meantime, because the poll read its EOF, a read error, its Close frame or a protocol error, is skipped without a log line. A reader that resumed during a block before that poll makes progress by then, and the count clears. The first tick that finds no progress only sets `client.write_stalled`. A false first count is harmless, because the drop needs a second tick and the look after the poll. If libuv cannot create a handle, the tick leaves the client for the next tick. `stop_server` closes the handles of a look that did not run yet (`server.pending_polls` lists them). **The look is a sample, and it has one known race.** libuv takes its snapshot of the ready sockets when a poll starts. A callback that blocks inside that poll, after the snapshot, hides what Claude reads during the block from the check callback that follows. A client that was stalled for the whole window (two ticks) and resumes during such a block is dropped. That is a deadline race, as with any timeout: the client was stalled when the window ended, and what it read afterwards is not reported yet. Two verifiers closed a reader that way in real-socket probes: a 0.5 s block (3.86 to 3.99 MB read, Neovim 0.12.3 and 0.8.0, 3 s and 30 s intervals) and a 1.5 s block (3.93 MB read, 5 s and 30 s). A block after the tick and before that poll keeps the reader, and so does a block in a scheduled callback. A detector for blocks inside the poll is possible: a prepare handle that times each poll, and a look that repeats until a poll was short. A prototype kept the reader in the two poll-block probes of the verifier on Neovim 0.12.3. I did not run it on 0.8 or on the full probe set. It adds a third handle, a threshold and a give-up count, and it still leaves a window as wide as the threshold, so this PR does not include it. A tick gap above `interval * 1.5` counts as a wake from sleep. A wake tick starts a fresh stall window: it resets `last_pong` of each connected client (as on main), resets `last_drain`, clears the count, and judges nothing, because Claude had no chance to read after the sleep. That delays the drop by one tick when the count was clear, and by two ticks when the wake tick takes the place of the confirming tick. The next two ticks always count, wake ticks or not, and a wake tick within them only resets `last_pong`. Wake ticks that come again and again are a loop that stays blocked, not sleeps. So whatever the pattern of late ticks, a stalled client is closed at the second tick after a fresh window started. A wake tick three or more ticks after the last fresh start starts a new window. Before this rule every wake tick cleared the count, and a verifier kept a client with 12.8 MB queued for 20 intervals while every tick was a wake tick. Ticks that come late by less than 1.5 intervals move the drop by their own delay and no more. ## What changed - `client.lua`: `write()` counts the bytes it passes to the socket in `client.queued_bytes`, and every socket write goes through it (frames, pings, pongs, Close frames). A frame of more than 1 MiB is queued in pieces of 1 MiB, and the callback of the last piece reports the frame. New `M.sample_write_progress`, `M.is_client_reading(client)` and `M.abandon_close_frame`. `close_client` starts the Close-frame deadline. `create_client(tcp_handle, keepalive_timeout)` takes the window. - `tcp.lua`: the ping tick samples every connected client and, for a client that answered, calls `confirm_stall` at the second tick without progress. New local functions `after_next_poll`, `close_pending_polls`, `confirm_stall` and `drop_client` (the close sequence the keepalive drop and the stall drop share: Close 1011, then `abandon_close_frame`, then `_disconnect_client` with 1006). The drop logs one info line: `Closed client_<n>: not reading for <s>s, <n> KB queued`. `start_ping_timer` sets `server.keepalive_timeout` to `interval * 2`. `stop_server` closes pending handles. - A pong rule runs first on each tick: a client without a pong gets a second chance (`pong_overdue`) and then the keepalive drop, whatever its queue shows. Only a client that answered is judged for a stall. - `lua/claudecode/server/README.md`: the "never reads keeps its socket" limit is replaced by the rule above. The API list, the ping-timer item and the side-effects list name the new functions and handles. - `tests/mocks/vim.lua`: `new_check` and `new_idle` mocks. Fake clients in the server specs carry `queued_bytes` and `get_write_queue_size`. - `tests/unit/server/connection_lifecycle_spec.lua`: 61 tests, 28 before this round. The spec stubs `valid_utf8`, so the 1 MiB-and-larger frames do not run the real validator under luacov (see Verification). - `covered.lock` re-recorded. ### Since the last push (`8fe3c19`) 1. The stall rule changed from "no progress for `interval * 2`" to "no progress at two ticks in a row, and still none right after the next poll". `is_client_reading` lost its `timeout` argument and counts through `client.write_stalled`. 2. The stall rule now sits behind the pong rule of coder#479: a client without a pong gets the second chance and the keepalive drop, whatever its queue shows. Only a client that answered is judged for a stall. 3. A wake tick makes no judgement and clears the count, unless a fresh window started in the last two ticks. Then it counts like any tick. 4. The ping and pong byte count, and the error of the last piece of a split frame, had no test. They have tests now (the code did not change). 5. The lifecycle spec grew from 28 to 61 tests. The spec stubs `valid_utf8`, and builds its pong frame in `before_each`. 6. The server README, `covered.lock` and the `vim` mock (`new_check`, `new_idle`) follow. ## Tradeoffs - **Slow readers.** libuv writes more only after the kernel reports the socket writable again. On a Linux loopback socket with the default 4 MiB `tcp_wmem` maximum, the reader had to read 1.16 to 1.54 MB (median 1.35 MB over 8 cycles) before that happened. So a Claude must read about 1.4 MB per window while a backlog exists. At the default 60 s window that is about 23 KB/s. I measured this on Linux only. A real Claude reads far faster. A reader at 100 KB/s stayed connected for 200 s (see the live probes). - **A reader that keeps up just enough.** Size is not capped, so a Claude that reads a little more than that floor, while Neovim queues more than it reads, still lets the queue grow. I chose this over a size cap because any cap drops a live Claude that gets a large message. - **One large message.** A 64 MB message that a reader takes at 1 MB/s stays connected for as long as libuv writes any of it. - **Close-frame deadline.** A protocol-error client that reads slowly keeps its socket while it reads. A client that stops reading is cut after one to two windows, and its Close frame is dropped. One window without progress is enough here: the client is leaving anyway, so a close that comes too early after a blocked loop costs only its Close frame. - **Windows.** libuv on Windows adds a whole write request to the queue size when it is queued and subtracts it when the request completes (`src/win/tcp.c`), while on Linux and macOS it lowers the size as bytes are written (`src/unix/stream.c`). So a frame of more than 1 MiB is queued in pieces of 1 MiB, and a Claude must finish one piece per window there. I have no Windows host here, so I did not run it. This rests on the libuv source and on a test that models a reader finishing whole requests. - **Piece size.** The 1 MiB piece is one fixed constant. It costs one extra copy of a large frame while it is queued. A frame of 1 MiB or less is one write, as before. - **Two handles per look.** A look exists only for a client that answered and showed no progress at two ticks in a row. The check callback closes the pair in the loop pass where it runs. A server whose clients all read normally never creates one. - **One more ping.** The tick that asks for the look still pings, because the drop comes after the poll. That ping is a few bytes in a queue that is dropped a moment later. - **A race in the look.** A client that was stalled for the whole window and resumes during a block inside the confirming poll is dropped. See "The look is a sample" above. The cost is one reconnect of Claude, with the pending diffs of that client rejected as for any disconnect. - **Wake from sleep.** The Close-frame deadline has no wake reset. It only closes a client that already broke the protocol or that the server stopped. ## Scope and blast radius Server transport only: `client.lua`, `tcp.lua` and their README. The change adds one disconnect reason and one socket close for a Close frame that nobody drains. Both use the existing `_disconnect_client` and `on_disconnect` path. The stall drop now runs one libuv poll after the tick, from a check callback instead of the timer callback. It changes no diff state and no openDiff answer beyond that path. `verify-diff-lifecycle` `check.sh` passes after the re-record. Only the `client.lua` and `tcp.lua` file hashes and the `create_client` block hash changed. No code fact reads FALSE. No credential handling changes. The auth token is neither read nor written by this diff. The blast radius is all WebSocket clients. A client that reads normally has an empty queue at each tick, which counts as progress. The risk is a false drop of a very slow reader (see Tradeoffs). `create_client` has a second, optional parameter. Fake clients in tests must carry `queued_bytes`. ## Verification ### Tests - `mise run all` with `CLAUDE_CONFIG_DIR` unset, on the merged head: 1393 successes, 0 failures, 0 errors, 16 pending (specs that need a real Neovim). luacheck: 0 warnings in 163 files. `mise run format-check` (`treefmt --ci`): 329 files, 0 changed. - Server specs (`tests/unit/server`, `tests/unit/server_spec.lua`): 191 ok, 0 not ok. - `scripts/run_integration_tests_individually.sh`: reports 272 successes, 0 failed, 0 errors. The script counts the lines "Success" and "Success: N" in each spec's output, so the true number is 254 (the other 18 are summary lines). That counting is older than this PR, and I did not change it. - `.agents/skills/verify-diff-lifecycle/check.sh`: PASS (main 89,205 states, live 5,269 states) after the re-record. `--hash-only`: matches. No code fact reads FALSE. - Shuffled orders: the lifecycle spec and `send_utf8_spec` pass with `busted --shuffle --seed=N` for N in 467, 11, 12, 99, 2026 and the eight seeds below (64 ok each). `mise run all` shuffles too and prints its seed. The pong frame of the spec is now built in `before_each`. Building it while the file loads fails with "attempt to index upvalue 'frame'" under `--shuffle --seed=N` for N in 17, 18, 24, 25, 50, 51, 66 and 75 (a scan of 1 to 80, one failing test each) and passes at the other 72 seeds. Seed 467 no longer exposes it. - CI time: an earlier head of this PR made CI take about 14 minutes, because the 1 MiB-and-larger frames in the lifecycle spec ran the real UTF-8 validator under luacov. That one spec took 753 s under luacov. The spec now stubs `valid_utf8` and takes 45 s (54 s on this head, on a busy machine). - The fake timer of the lifecycle spec rejects a second `close()`, as libuv does and as the spec's fake check, idle and socket handles already did. Before, it accepted one, and removing `client.close_timer = nil` from `stop_close_timer` passed every test. On real sockets every drop then raised "handle is already closing" from the Close frame's write callback. With the assertion, that mutant fails 3 tests. - No test passed only on retry. ### Red to green and mutants I ran the lifecycle spec of the previous head (54 tests) against older code: 22 of its tests failed against the code of the pushed head (`8fe3c19`), and 12 against the local 5% head (`9a0d8d4`, never pushed). The spec of this head has 61 tests. Each mutant below changes one guard of this head. Every one makes at least one test fail: | Mutant | Tests that fail | |---|---| | The tick closes the client itself, with no look after the poll | 14 | | The check callback closes without sampling the queue again | 2 | | No idle handle next to the check handle | 1 | | The handles stay open after the callback ran | 4 | | The finished look stays in `server.pending_polls` | 1 | | `stop_server` leaves the handles of a pending look open | 1 | | The look skips no client that left in the poll (no guard) | 3 | | The look skips only a client that left `server.clients`, not one that is no longer connected (a peer Close) | 1 | | The look skips only a client that is no longer connected, not one that left `server.clients` | 1 | | Every tick asks for a look, not only the second | 35 | | A wake tick that starts a fresh window samples the queue | 6 | | A wake tick that starts a fresh window does not reset `last_drain` | 2 | | Every wake tick starts a fresh window, as before the counter | 2 | | A fresh window protects one tick, or three, instead of two | 2 and 1 | | A fresh window never ends | 1 | | A wake tick inside a fresh window does not reset `last_pong` | 2 | | Pings are written without the byte count | 3 | | Pongs are written without the byte count | 1 | | The write error of the last piece of a frame is dropped | 5 | | A frame of more than 1 MiB is not split | 4 | | The deadline of a Close frame closes without sampling | 1 | | `drop_client` does not end the deadline | 1 | | `stop_close_timer` does not clear `client.close_timer` before it closes the timer | 3 | The survivors of other mutations are listed at the end. <details> <summary>Real sockets, Neovim 0.12.3 (libuv 1.52.1) and 0.8.0 (libuv 1.44.2)</summary> I ran a headless Neovim with its own XDG directories and `CLAUDE_CONFIG_DIR` against raw WebSocket clients that play Claude. The rows for the block and memory probes ran on the server code of `964b744`. The commits after it change the wake rule, remove a dead store, and add comments and tests, so I ran the probes that touch ticks, wakes and the plain stall again on the head of the wake counter (`5c910f7`): the `fresh.py` rows, the 1.35 and 1.6 rows and the 3 s stall. `client.lua` and `tcp.lua` are the same on the final head. The auth token appears in no output file (match count 0). The probes that block the loop use one block of 0.5 s to 5.5 s, either inside an I/O callback (a libuv accept callback) or inside a scheduled callback. Every client except the "parsing reader" rows sends pongs without being pinged. The parsing reader reads and parses frames and answers each ping it reads. **A reader resumes during a block, and the tick comes just after.** Interval 5 s. The reader stalled, and starts reading while the loop is blocked. "Closed" and "kept" describe the client at the end of the run. | Case | `8fe3c19` (on GitHub) | 5% head (`9a0d8d4`, local) | This head | |---|---|---|---| | Block inside an I/O callback, tick 1.02 intervals after the last: 0.12.3 | closed, 4.00 MB read | closed, 3.93 MB read | kept, 33.55 MB read | | Same: 0.8.0 | closed, 3.93 MB read | closed, 3.93 MB read | kept, 33.55 MB read | | Same, tick 1.00 intervals after the last: 0.12.3 and 0.8.0 | not run | not run | kept, 33.55 MB read | | Same, parsing reader: 0.12.3 and 0.8.0 | not run | closed, 3.95 MB read | kept, 33.55 MB read | | Block inside a scheduled callback, tick 1.02 late: 0.12.3 | kept | kept | kept | | Same: 0.8.0 | closed, 3.93 MB read | closed, 3.93 MB read | kept | | Block of 1.35 intervals: 0.12.3 and 0.8.0 | closed, 3.93 MB read | kept | kept | In the I/O callback rows, the tick after the block saw no progress yet (the probe records it). This head kept the client because the look after the next poll saw progress. A second probe, `fresh.py` (not run on `8fe3c19`): a reader that stalled for one tick resumes 50 ms into a 500 ms block inside an I/O callback, and the next tick runs right after the block. | Interval, Neovim | 5% head (`9a0d8d4`, local) | This head (`5c910f7` and `964b744` gave the same numbers) | |---|---|---| | 5 s, 0.12.3 | closed, 1.61 MB read | kept, 15.97 MB read | | 5 s, 0.8.0 | closed, 1.61 MB read | kept, 16.14 MB read | | 30 s (default), 0.12.3 | closed, 1.61 MB read | kept, 15.97 MB read | | 30 s (default), 0.8.0 | closed, 1.61 MB read | kept, 16.14 MB read | **A stalled reader that answers each ping, with ticks that come late.** Interval 5 s. A block in a timer callback after each tick makes the next tick late. The loop reads and answers nothing else. | Pattern | 5% head (`9a0d8d4`, local) | `8fe3c19` (on GitHub) | `964b744` | `5c910f7` (same server code as this head) | |---|---|---|---|---| | Every tick 1.35 intervals late (below the wake threshold of 1.5), 0.12.3 | kept for the whole 120 s (17 late ticks) | closed after 18.4 s | closed after 19.3 s | closed after 19.3 s | | Same, 0.8.0 | kept for the whole 120 s | not run | closed after 18.5 s | closed after 19.2 s | | Every tick 1.6 intervals late, so every tick is a wake tick, 0.12.3 | not run | not run | kept for the whole 100 s | closed after 29.3 s | | Same, 0.8.0 | not run | not run | kept for the whole 100 s | closed after 29.2 s | | 1.6 intervals late after the stall sample only, so wake ticks alternate with ticks in time, 0.12.3 | not run | not run | kept for the whole 100 s | closed after 26.3 s | | Same, 0.8.0 | not run | not run | kept for the whole 100 s | closed after 26.2 s | The last four rows are the case that a verifier found on `964b744` (every wake tick cleared the count) and the case that my first rule for it did not cover (wake ticks that alternate with ticks in time). The counter rule above closes both. **A block inside the confirming poll** (not run by me, from two verifiers). A client that was stalled for two ticks, whose reader resumed 0.05 s to 0.1 s into a 0.5 s or 1.5 s block inside the poll that the look waits for, was closed after 3.86 to 3.99 MB read. That is the deadline race described above. A 500 ms block before that poll or inside a scheduled callback kept the reader. **Plain stall, and the pong rule** (interval 3 s). The reader never reads, one case answers each ping, one never answers, one answers only from 10 s, one with a 6 s block of the loop at 7.5 s (a machine that slept): | Case | Closed after | Reason | |---|---|---| | Never reads, answers pings | 8.9 s (0.12.3), 8.9 s (0.8.0), also on `5c910f7` | Write queue stalled | | Never reads, never answers | 12.0 s | Connection timeout, after the second chance | | Never reads, first pong at 10 s | 12.0 s | Write queue stalled | | Never reads, loop blocked 6 s at 7.5 s | 19.5 s, 6 s after the wake tick | Write queue stalled | The times are the same on the 5% head. On `8fe3c19` the plain stall closes after 8.9 s too (not run for the other three). **Memory and controls** (0.12.3). A raw client, no block of the loop: | Case | Result on this head | |---|---| | Never reads, one pong per second, 1000 requests per second (3 s ping, 6 s window) | Closed 8.9 s after the accept. The queue was 34,331,532 bytes and is then 0. Lua heap falls from 46,526 KB to 1,720 KB after a GC. RSS fell from 71,392 to 56,580 kB in this run. | | Same at the default 30 s ping, 250 requests per second | Closed 89.9 s after the accept. The queue was 87,263,130 bytes and is then 0. Lua heap falls from 149,421 KB to 1,953 KB. | | Breaks the protocol (BINARY frame) while the queue is 10 MB and never reads | Socket closed 7.0 s later. The queue was 10,367,540 bytes and is then 0. Lua heap 1,524 KB after a GC. | | Control: reads 1 MB/s, 300 requests per second (3 s ping, 60 s) | 0 disconnects. 62.65 MB read. | | Control: reads 100 KB/s, 300 requests per second (default ping, 200 s) | 0 disconnects. The queue reached 216,165,112 bytes. | | Control: one 64 MB message, reader at 1 MB/s for 55 s (default ping) | Connected. 56.6 MB read. After the reader stopped, closed 63.7 s later. | The row for 100 KB/s shows the second tradeoff above: a reader above the floor keeps its connection while the queue grows. </details> ### What the tests and probes do not cover - No unit test runs libuv. The fake `check` and `idle` handles run their callback when the spec says that a poll happened. Only the real-socket probes show libuv's order of phases, on Linux with 0.12.3 and 0.8.0. I ran no Windows and no macOS. - A block inside the confirming poll is the race above. The probes of two verifiers show it, and no test pins it, because the fake loop has no snapshot to miss. - Neovim 0.8's `uv.walk` crashes on handles that luv did not create, so the probes count the check and idle handles only on 0.12.3 (0 left open at the end of every run). - The slow-reader probes send a pong every second without being pinged. A real Claude answers each ping, so the pong path here is easier than in real life. - Mutations that survive the server specs and the full suite. The list below is one non-exhaustive set: the seven survivors of one verifier's mutation set. A second verifier's independent set of 88 mutants found the same seven, one test gap (the `close_timer` line above, now covered), and eight more that change no behavior. A third verifier's set of 55 mutants found two survivors that do change behavior and have no test: the first delay of the Close-frame deadline (`timer:start(timeout, timeout, ...)` in `start_close_timer`). Started at once, the deadline cuts off a client that reads, before it reads its Close frame. Started after three windows, it keeps the socket of a client that never reads for three windows instead of one. Both change behavior only for a client that is already being disconnected, and no test reads the delay. I will cover them in a follow-up PR. Other survivors can exist. I know of no defect in the code behind any listed survivor. 1. An empty queue counting as progress in `sample_write_progress`. It is equivalent: every tick writes a ping, so a queue that is empty at a tick always follows progress. 2. Writing the Close frame that answers a peer's Close with `tcp_handle:write`, which skips the byte count of `write()`. That reply starts no deadline, and the client is `closing`, so the tick and the look skip it. 3. Writing the Close frame of `close_client` the same way. It is equivalent for the progress decisions after the socket is closing, because the deadline compares two samples of `queued_bytes` less the queue size, and a frame that is queued before the first sample cancels out. 4. The identity check of the Close-frame timer (`client.close_timer ~= timer`). 5. The check of `close_pending` in the timer callback, its early exit when the write already finished. 6. The check of `handle:is_closing()` in the timer callback. 7. The `if not timer then return end` guard in `start_close_timer`, for a `vim.loop.new_timer()` that fails. For 4 and 5 every path that clears `close_pending` also stops the timer in the same step, and libuv runs one callback at a time, so I know of no order that reaches them. I did not look for an order that reaches 6 and 7. A verifier's advisory pass found no failing order for 4 to 7. The eight that change no behavior, from the second verifier: - `<=` to `<` for a frame of exactly 1 MiB in `write()`: the piece loop makes the same single write. - The `stop_close_timer` call inside `start_close_timer`: dead code, because `close_client` returns early for a closing client, so the deadline starts once per client. - The `last_drain` store in `start_close_timer`: a closing client is never logged. - `close_pending = nil` when the deadline closes the socket: the cancelled write callback clears it in the same loop pass. - The initial `last_drain` in `create_client`: the first sample always sees the drained 101 reply. - Running `fn` before the handles close in the look. - The `is_closing` check in `close_pending_polls`: pending handles are never closing. - `handle:stop()` before `handle:close()` in the look: `uv_close` stops the handle. Tests do observe the 1011 Close frame of a ping drop: leaving it out turns 8 tests red. - The state half of the look's guard (`client.state ~= "connected"`) is reachable and has a test. A peer Close sets the client to `closing` before its scheduled removal, so a look that runs in between finds a client that is listed and no longer connected. Without the guard the look reports 1006 "Write queue stalled" instead of the peer's 1000. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 12, 2026
…er#488) ## Result Neovim 0.8 no longer drops a Claude that answers every ping. A block of the main loop, of any length and in any callback, does not close a Claude that writes something within 75 s (`interval * 2.5`) of each ping. A Claude that sends nothing is still closed 3 intervals (90 s by default) after its first unanswered ping, when no block longer than 1.5 intervals gets in the way. **This push also merges main with coder#467** (a client that answers pings but never reads), which rewrote the same ping tick. Its stall rule stays, and both rules hold (see "With coder#467"). ## Problem coder#479 made the ping timer drop a client only at the second tick that finds no pong. On Neovim 0.8 (libuv 1.44.2) that is still a race. `uv_run(UV_RUN_ONCE)` runs timers at the start of a pass and again at the end, after the check handles. Neovim runs `vim.schedule` callbacks between two `uv_run` calls. So a tick at the end of a pass, a block in `vim.schedule`, and a tick at the start of the next pass run with no socket read between them. Claude's pong waits in the socket for both ticks. Trace on main, Neovim 0.8.3, a separate-process Claude that answers every ping at once (interval 200 ms): ``` TICK since_pong=191 overdue=nil ping sent B1: 260 ms block in a check callback TICK since_pong=453 overdue=true timers run again at the end of the pass, pong still unread B2: 260 ms block in vim.schedule on_disconnect(client_1, 1006, "Connection timeout") dropped at the next tick ``` A counter cannot fix this. Any number of ticks can run before a read, so the tick must not judge at all. ## Change - A tick pings each connected client and never drops one. It stamps `client.ping_unanswered_since` with the oldest ping sent since bytes were last read from the client. It calls `vim.loop.update_time()` before it reads the clock for the wake test, the stamp and the gap: libuv caches the loop time when a pass starts and runs the timers of the pass with it, and a timer callback that ran before the tick in the pass can have blocked since, or the machine can have slept in it. A stale time hid a wake in the earlier pushes of this PR (Codex round 3). - Each tick that pinged a client starts a one-shot libuv check handle. libuv runs it after the poll phase that reads the sockets, so every byte that reached a socket before the loop time of the check was read. The check drops a client whose oldest ping is `interval * 2.5` old. - **Any bytes clear the stamp.** The read callback clears it, not only a PONG. A pong can wait behind more unread data than the socket holds (Claude writes while Neovim is blocked, and one poll reads only the first part), so the poll after a block does not always reach the pong. Claude shows it is alive by writing anything. - **The check judges only if its loop time is at most `interval * 1.5` after its tick.** A machine that sleeps between a tick and its poll stops Neovim and Claude together: no bytes arrive, and the ping looks as old as the sleep. A tick treats a gap above 1.5 intervals as a wake. The check now does too, and the next tick starts the count over. A block longer than 1.5 intervals therefore restarts the count. - A wake from sleep (a tick gap above `interval * 1.5`) clears the stamps. - Removed: `client.pong_overdue`, `client.is_client_alive` (its only caller was the old tick), and the reset of `last_pong` in the 101 write callback (a client that no tick pinged has no stamp, so the main loop cannot time it out). - `vim.schedule` is not a safe place to judge: Neovim can run it before the read. The check handle is. ## With coder#467 coder#467 landed on main while this PR was in review. It rewrote the ping tick (a pong rule with a second chance, `pong_overdue`, `is_client_alive`) and added a write-queue stall rule with its own check and idle handles. This branch keeps that rule and puts the keepalive of this PR next to it: - The stall rule is unchanged: a client that answered and whose write queue made no progress at two ticks in a row is closed after the next poll ("Write queue stalled", Close 1011 "Not reading"). The 61 tests of main's lifecycle spec: 56 pass under their names, and 5 were rewritten for the stamp and renamed (the `pong_overdue` second chance, the late-tick tests, and the wake and drain tests that spoke of flags). - "Answered" now means that no ping of the client waited for `interval * 2` (it was "a pong within `interval * 2`"). Only an answered client is judged for a stall. A silent client is closed by the keepalive judgement ("Connection timeout", Close 1011 "Keepalive timeout") at the same tick as before, whatever its write queue shows. - A tick that pinged a client arms **one** check and idle pair (`after_next_poll`, from coder#467) that runs both judgements after the poll. It was one pair for each stalled client. `stop_server` closes it as before. - `pong_overdue` and `is_client_alive` are gone, because the stamp replaces them. The tests that named them are rewritten for the stamp (a silent client with a stalled queue is closed by the keepalive, a late pong does not save a stalled queue, a wake restarts both windows). Three confirmation tests no longer expect "no handle" at a tick without a stall, because a tick that pinged always arms the pair. The wake-threshold test from coder#495 ("a tick 1 ms above the wake threshold") expected no handle after a wake tick for the same reason: it now runs the poll after the tick and checks that the client is kept and `on_disconnect` did not run. Two helper counts changed (`forget_handles`). - A real-socket probe of the stall rule (Claude sends unprompted pongs and never reads, 8 MB queued, interval 300 ms): main and this branch both close it with "Write queue stalled" 2.6 intervals after the message, on Neovim 0.8.3 and 0.12.3. - A client that writes data and reads what the plugin writes, but never answers a ping, is kept. Main closes it 3 intervals after its first ping. ## Behavior - A block of the main loop, of any length and in any callback, does not close a Claude that writes something within `interval * 2.5` of each ping. A tick never closes a client, a check judges only after a poll within `interval * 1.5` of its tick, and any bytes clear the stamp. - **A client that writes data and reads what the plugin writes, but never answers a ping, is no longer closed by the keepalive.** It is alive, and the plugin does not judge what it writes. Main closes it 3 intervals after its first ping. The stall rule of coder#467 still closes it if it stops reading, but only once the kernel's socket buffers are full and libuv's write queue backs up: until then every write completes, and an empty queue counts as progress. So a client that stops reading and keeps sending is closed later than main closed it when it also never answered a ping. The README says so. - A Claude that sends nothing is closed at the first read of its socket after the third tick that follows its first unanswered ping (90 s by default). Main closes it at 2 to 3 intervals after its first ping in the verifier's runs and at 3.0 in mine. - A block delays the close of a silent Claude to the first read after the block ends. A block longer than 1.5 intervals also restarts the count, so a run of such blocks can postpone the close. - The info line `Closed client_<n>: no reply for <s>s` counts from the oldest ping sent since bytes were last read. ## Tests `tests/unit/server/connection_lifecycle_spec.lua` models the loop as libuv runs it: a loop time cached at the start of a pass, a poll that reads the sockets, and check handles that run after it. These fail on the code of coder#479 (main): two late ticks with no read between them (the trace above), 20 late ticks in a row, a silent Claude is dropped only at the first read after its tick, the time counts from the first unanswered ping, and a client that hung up or is closing is not judged. These three fail on the first push of this PR (f3576ea) and pass now: a block of 3 intervals between a tick and its poll judges nothing, a Claude that sends a large message before its pong is not dropped (the poll reads only the first 64 KB, the ping is 2.8 intervals old, and the poll is within the gap), and a client that writes data but never answers a ping is kept. The last two also fail on the gap skip alone. The other new tests guard: a client that writes data and never answers a ping is kept, a pong that waits in the socket when its ping is 3 intervals old, a late tick that finds a silent Claude's ping 2.5 intervals old, a poll 1.4 intervals after its tick that still judges, the stamp aged from the time the ping was sent, a block that restarts the count, a stale cached loop time, and a wake from sleep. `tcp_spec.lua` and `log_lines_spec.lua` follow the new tick/check split. Added after the verifier's mutation run on `68b0b13`: the check judges with the loop time of the poll and not with a time read after a younger callback blocked (a Claude whose pong arrives during that block is kept), a tick takes a wake for a wake although the cached loop time is old (a timer callback before it in the pass blocked for 2 intervals, so the clock shows 3 since the last tick and the cache shows 1), the gap skip at exactly 1.5 intervals (judges) and at 1 ms above it (does not), a drop at exactly 2.5 intervals, the stall judgement does not sit under the gap skip (a stalled client is dropped although every poll comes 1.6 intervals after its tick), and a client whose ping is still inside the window is judged for a stall. **Mutants.** My 16 are each caught by at least one test: no `update_time`; bytes do not clear the stamp; a wake does not clear it; no listed-client guard; no connected guard; limit x2 and /2; stamp overwritten each tick; pinged list empty; the check reads the real time; no gap skip; gap x3 and /3; the stall rule judges a silent client; the stall rule never runs; the dropped client keeps its Close-frame deadline. Of the verifier's 33 mutants of `68b0b13`, nine survived. Six are now killed: `update_time` inside `judge_silence`, the stall judgement under the gap skip, the gap skip at 2.0 intervals, the gap skip with `<` for `<=`, the limit with `>` for `>=`, and `answered` true only for a client with no stamp. Each has a test that fails on it. The seventh, a `tick_time` taken from the cached loop time, is equivalent since the round-3 fix (the tick time is the fresh time of the tick), and I dropped it. Two new mutants of the tick clock are killed: no `update_time`, and `update_time` after the wake test. The two that still survive are the stall judgement running before the keepalive one in the check, and the any-bytes clear after `process_data` instead of before it. The verifier classed both as equivalent. As far as I can tell, the first changes only which reason (`Not reading` or `Connection timeout`) a client gets when both rules apply to it in one poll, and the second matters only if `process_data` raises. **Random order.** The full suite passes with `--shuffle` for seeds 1 to 60 (1439 successes, 16 pending, 0 failures in each of the 60 runs). Before the fix, seeds 9, 15, 40, 57 and 59 failed (the verifier found them on `68b0b13`): the pong of the late-tick tests was built when the file loaded, from a `frame` module that only the outer `before_each` sets (`attempt to index upvalue 'frame'`). It is built in a `before_each` now. ## Replays on real Neovim A separate-process Claude (Python) answers every ping at once. Interval 300 ms. **Block matrix.** Blocks of 0.9, 1.3, 1.45 and 2.2 intervals run one after the other: the first right after a ping, in each of four contexts (a check callback, `vim.schedule`, a timer callback, an I/O read callback on a UDP socket), then the second in each of the four. 64 cases. 12 more cases run 6 blocks that cycle through all four contexts. | | Neovim 0.8.3 (libuv 1.44.2) | Neovim 0.12.3 (libuv 1.52.1) | |---|---|---| | main, 76 block cases | **6 dropped**, 70 kept | 0 dropped, 76 kept | | this PR, 76 block cases | 0 dropped, 76 kept | 0 dropped, 76 kept | | main, random blocks, 16 seeds of 20 s | **2 dropped** (seeds 10, 11) | not run | | this PR, random blocks, 24 seeds of 20 s | 0 dropped | 0 dropped | **The three paths of the verifier's finding, each with the mechanism that covers it.** 4 runs each (idle and prepare callbacks, 2 each), dropped / total: | Probe | first push (f3576ea) | gap skip only | any bytes only | both (this PR) | |---|---|---|---|---| | A block of 2.7 intervals before the poll, Claude writes 300 KB and then its pong during it | 4/4 on 0.8.3 and 0.12.3 | 0/4 | 0/4 | 0/4 | | Claude sleeps with Neovim: it answers the ping 2.7 intervals late | 3/4 | 0/4 | **4/4** | 0/4 | | Two blocks of 1.4 intervals (under the gap) with an older stamp, Claude writes 300 KB and then its pong | 4/4 | **4/4** | 0/4 | 0/4 | Each mechanism is needed: the gap skip alone drops the third row, and any bytes alone drops the second. **A client that writes every 100 ms and never answers a ping:** main drops it 3.0 intervals after its first ping. This PR keeps it (2 of 2 versions), and the stall rule of coder#467 still closes a client that never reads. **A Claude that reads pings and never answers:** dropped 3.0 intervals after its first ping on main and on this PR, on both versions. With 2 blocks of 2 intervals in the way: 8.0 intervals on both. **Re-run after the tick reads a fresh clock (Codex round 3), on the `lua/` code of this push.** Block matrix: 76 kept and 0 dropped on Neovim 0.8.3 and on 0.12.3. Random blocks: 24 seeds of 20 s, 0 dropped on both. The three F1 probes and the residual probe (300 KB and a pong behind a block, a Claude that answers 2.7 intervals late, two blocks of 1.4 intervals): kept on both. A client that writes every 100 ms and never answers: kept on both. A Claude that sends nothing: dropped 3.0 intervals after its first ping on both, and 8.0 with two blocks of 2 intervals. With six blocks of 1.3 intervals through four contexts it is dropped at 11.8 (0.8.3) and 11.9 (0.12.3) intervals, 3 later than before the change: the tick now sees the real gap, takes it for a wake, and restarts the count, as the README says. The scripts are my scratch probes, not repo files. They move into the `verify-ws-connection` replays in coder#474. ## Not in this PR - The TLA+ model in coder#474 follows this change in a separate update. ## Checks `luacheck` (with `--no-unused-args --no-max-line-length`, as CI runs it), `stylua --check`, `prettier --check` on the README, a `luajit` load of every file under `lua/`, the full busted suite (1439 successes, 16 pending, seed 424242 and seeds 1 to 60) on the code of the merge with main at `e5c5ddb` (the newer main commit `b477362` changes only `scripts/`), `verify-diff-lifecycle/check.sh` PASS (full run) and its `covered.lock` re-recorded. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 14, 2026
… connection lifecycle (coder#474) Adds `.agents/skills/verify-ws-connection`: a TLA+ model of one WebSocket connection between Claude and the plugin, checked with TLC against guards that `check.sh` reads from the Lua source. It is the second `verify-*` skill on the shared harness (`scripts/tla/check-lib.sh`, coder#450), after `verify-diff-lifecycle`. It describes the keepalive as coder#488 merged it (d63c9b3, with the fix for the fresh clock at the tick). On the code of coder#479 it reads STALE, and its facts for the new design read FALSE. ## What it checks Six rules, from the TCP accept through the handshake, requests, Close frames, keepalive pings and server stop: | Rule | Plain sentence | | --- | --- | | `NoRequestAfterEnd` | A request from Claude runs only after its 101 reply was written, and never after the plugin started to close the connection or saw it end. | | `DisconnectReportedOnce` | `on_disconnect` runs at most once per client. | | `StatusCloseDelivered` | A Close frame for a protocol error (1002, 1003, 1007, 1009) or a server stop (1001) is written before the plugin closes the socket, as long as Claude keeps reading. A Claude whose queue makes no progress for one keepalive window loses the frame to the deadline of `close_client`, which closes the socket (not modeled). | | `NoFalseTimeout` | A Claude that answers each ping before the next tick is never dropped by the ping timer, whatever blocks Neovim or sleeps the machine. A tick reads a fresh clock, only pings and stamps the oldest unanswered ping. The check that drops a client runs after a poll that read the sockets, judges nothing when its poll comes more than 1.5 intervals after its tick, and any bytes read from the client clear the stamp. A Claude that stopped once is not covered. A pong that comes later than one interval is not covered either: when a callback blocks inside the poll phase and refreshes the loop time, the poll can miss it, and the check closes that client once its ping is 2.5 intervals old (the verifier's probe on Neovim 0.12.3 dropped a peer that answered 2.4, 1.4 and 0.4 intervals late. Main does the same.) A real Claude answers a ping at once. The rule holds for any limit above `interval * 1.5`, the window in which a check still judges: a limit of 1.2 intervals passes the model, and real Neovim drops a Claude that answered within 100 ms when a read callback blocks about 1.3 intervals in the poll after the tick. The code keeps 2.5. | | `DeadClientDropped` | A client whose Claude hung up or stopped answering, or whose connection the plugin started to close, eventually leaves `server.clients` with its `on_disconnect`. | | `DroppedSocketCloses` | Once a client left `server.clients`, or the server stopped, its socket eventually closes, as long as Claude reads again. | `covered.lock` hashes the five files the model describes (`server/client.lua`, `tcp.lua`, `handshake.lua`, `server/init.lua`, `init.lua`) and the blocks inside them, so a change there reads `STALE` until someone confirms the model still fits. The model describes the keepalive judgement only. The stall rule of coder#467 (`judge_stall`) and the deadline of a Close frame are not modeled, and `SKILL.md` says what a user sees for each. ## Bugs this model found Its first run broke three rules on the code as it was. Each one was replayed with real sockets and fixed in coder#455. Reviews of this PR then found four more false timeouts that the first model could not see. coder#479 and coder#488 (three rounds of it) fixed them: - `NoFalseTimeout`: a main loop blocked during the handshake got a Claude that answers every ping dropped with 1011 before any ping reached it. Since coder#488 a client has no stamp until a tick pings it, so no block can time it out. - `DeadClientDropped`: after a protocol error while Claude's window was full, the client stayed in `server.clients` (and `is_claude_connected()` stayed true) until Claude read again. - `DroppedSocketCloses`: a stop between Claude's Close frame and the scheduled `on_close` left the plugin's socket in `CLOSE_WAIT`. - `NoFalseTimeout`, again (coder#479): a tick that Neovim ran late after a block of 1.0 to 1.5 intervals can run before the plugin reads Claude's pong, and found the last pong 2.3 intervals old. libuv runs timers before it reads sockets: with libuv 1.44, which Neovim 0.8 bundles, after a block in any callback, and with newer libuv after a block in a check or I/O callback, not after one in `vim.schedule` or a timer callback. - `NoFalseTimeout`, a third time (coder#488): libuv 1.44 runs the timers at the end of a pass of the main loop and again at the start of the next, with Neovim's `vim.schedule` callbacks between. Two ticks ran with no read between them, and coder#479 dropped a Claude that answered every ping. No counter of ticks fixes that, so a tick now only pings and a libuv check handle, which runs after the poll, does the dropping. - `NoFalseTimeout`, a fourth time (the review of coder#488): the check ran on a poll that did not reach Claude's answer. A pong waits behind more unread data than the socket holds (any bytes from the client now clear the stamp), or the machine sleeps between a tick and its poll (the check judges nothing after a block longer than 1.5 intervals). Each of the two guards alone leaves one path open. The model has both, and a replay for each. - `NoFalseTimeout`, a fifth time (Codex's review of coder#488): the tick read `vim.loop.now()` before it called `update_time()`. libuv runs all timers of a pass with the loop time of the start of the pass, so after a sleep or a block of more than 1.5 intervals in an earlier timer callback of the same pass the tick saw no gap, kept the old stamps, and the check dropped a Claude that had no time to answer. The tick now updates the loop time first. There is no replay for it (a replay cannot make a timer callback run before the ping timer inside one pass), so the unit test of coder#488 and the model pin it: with `ClockFreshAtTick` off, `NoFalseTimeout` breaks. The model in this PR describes the fixed code (18 guards, all read TRUE). ## Round 7 (the one extra review round that the maintainer allowed) This push carries the prepared fixes for the last findings of the two verifiers of `77bb6e2`, and merges of main. The model (`model/`) and the `EXPECT` map are the same as in `77bb6e2`. - The limit that the promise holds for. `NoFalseTimeout` holds for any limit above `interval * 1.5`, not for one interval or more. A limit of 1.2 intervals passes the model, and real Neovim drops a Claude that answered within 100 ms when a read callback blocks about 1.3 intervals in the poll after the tick. `SKILL.md` says so now. The code keeps 2.5. - Which test catches which clock mutation. `SKILL.md` named the wrong test for one of them. Deleting `update_time()`, or moving it after `local elapsed` without reading `now` again, turns red only "ages a ping from when it was sent...". Moving it after the wake test and reading `now` again turns red only "takes a tick for a wake...". I ran both mutations. - The README and the comment of `start_ping_timer` say that the first check that finds the oldest unanswered ping `interval * 2.5` old closes a silent Claude, and that a block inside the poll phase refreshes the loop time. - `check.sh`: the record pattern lists `write(client, ` and `handle:close()`, so a change to one of those lines reads STALE. The `DispatchGuard` fact needs the `end` of its `if` right after `on_message`. The `StopWaitsForCloseWrite` fact rejects `release_socket`, `abandon_close_frame` and `drop_client` in `stop_server`. Five wording fixes in `SKILL.md`, and a note that the `sleep` case of the bytes-only contrast on Neovim 0.8.3 depends on timing. - Merges of main (the last one is coder#577). The server README keeps this PR's keepalive paragraph and takes main's new bullets. After the first two merges three locks read STALE and are recorded again: `verify-diff-lifecycle` and `verify-mention-queue` (the hash of `tcp.lua`, which differs from main only in the comment of `start_ping_timer`), and `verify-ws-connection` (`tcp.lua`, and `M.start` and `M.stop` in `server/init.lua`, where main's coder#539 changed a log line in `on_open` and coder#558 answers in-flight requests before `stop_server`). The second merge made the ws lock stale once more: main's coder#541 changed `M._broadcast_at_mention` in `init.lua`, which the model does not cover, and the covered blocks have the same hashes. The model still fits: those answers are ordinary writes to a connected client, the case the model has. The last two merges (coder#544 and coder#577, terminal and diff files only) needed no new record. ## What changed since the first version of this PR - The model follows coder#488: the facts `DropsOnSecondOverdueTick`, `AliveTickClearsOverdue`, `PongResetsAge`, `WakeResetsPong` and `UpgradeStartsKeepalive` are gone. `JudgesAfterRead`, `ClockFreshAtTick`, `StampKeepsOldestPing`, `BytesClearStamp`, `GapSkip` and `WakeClearsStamp` replace them. The environment steps are `StaleLoopTime`, `PollMissesPong` and `SleepInWindow`. A `stale` tick (an earlier callback of the pass blocked or slept) is a wake that only a tick with a fresh clock sees. - **`NoFalseTimeout` no longer counts awake time.** The first model added one tick of awake time on a late tick, so its own sentence ("a block does not count as awake time") was false, and a drop at a late tick while a pong waited unread passed. The rule now asks whether a Claude that never stopped answering was dropped, and the ticks run at any point between reads. A variant that judges at the tick (`JudgesAfterRead` off) breaks it in 12 states. - The text of `SKILL.md` is fixed: the libuv wording, the timings, the exit codes of `--hash-only`, the numbering of the update steps, the order of the `/statechart` steps (the kept directory is deleted after the view is handed over), the sentence about `--mutants` (`RejectClosesSocket` is caught only together with `UnlistedDisconnectReleases`), and each item that is not modeled now says what a user sees. That includes a client that sends bytes and never reads (coder#467 handles that stall) and a client that writes data but never answers a ping, which coder#488 keeps by design. ## What this PR changes outside the skill - `server/README.md` and the comment of `start_ping_timer` described the silent close and the promise wrongly. A silent Claude is closed by the first check that finds its oldest unanswered ping `interval * 2.5` old: 90 s after the ping when ticks come on time. One late tick delays it, because a late tick moves the ticks after it back. Two late ticks in a row, or a poll that a block delays after a tick, bring it as early as 75 s (2.6 intervals in the probes, never earlier). A tick more than `interval * 1.5` after the tick before it is a wake and restarts the count, so a block of more than half an interval just before a tick is enough, not only one of 1.5 intervals. The promise of no false close is now for a Claude that answers each ping before the next tick, as the model checks it, and the README says what a pong later than one interval costs under a block in the poll phase. - A comment in `connection_lifecycle_spec.lua` still named the pong rule and `pong_overdue`, which coder#488 removed. It names the keepalive and the stall rule now. - The comment-only edits to `client.lua`, `tcp.lua` and the spec that this PR carried for the design of coder#479 are gone, because coder#488 replaced that code. - `DEVELOPMENT.md`: the two paragraphs about `covered.lock` name every `verify-*` lock, not only that of `verify-diff-lifecycle` (unchanged in this push). ## Proof - `check.sh` on this branch (checked on the head before the last merge): all 18 facts TRUE and `RESULT: PASS`. `main` 262,285 states, `live-NoFalseTimeout` 256,264, `live-DeadClientDropped` 11,701, `live-DroppedSocketCloses` 11,701. It took 256 s and 271 s in two runs at a host load average of 14 to 40, and 2 to 6 min in other runs. The `check.sh` of the other four skills (`verify-diff-lifecycle`, `verify-mention-queue`, `verify-selection-tracking`, `verify-terminal-lifecycle`) all pass too, and all five locks match the code (`--hash-only`). - `check.sh --mutants` (one TLC worker): I ran it uninterrupted on the head of this push, before the last three merges of main (they change no covered block of this skill): 18 rows, every guard caught, exit 0, 5,753 s at a load average of 14 to 40. Both verifiers of `77bb6e2` had run it uninterrupted too (Opus: 4761 s, gpt: 4814 s, 18 rows each). `git diff 77bb6e2 HEAD -- .agents/skills/verify-ws-connection/model` is empty and the `EXPECT` map is the same in all three runs. The new and changed guards are caught by `NoFalseTimeout` (`JudgesAfterRead`, `ClockFreshAtTick`, `BytesClearStamp`, `GapSkip`, `WakeClearsStamp`) and `DeadClientDropped` (`KeepaliveReaps`, `StampKeepsOldestPing`). `RejectClosesSocket` alone is caught by no rule, because `_disconnect_client` also closes the socket of a client that left the server, so it is removed together with `UnlistedDisconnectReleases`. - A design check outside `check.sh` for the fresh clock: with the `ClockFreshAtTick` fact forced FALSE, `main` passes (264,485 states) and `live-NoFalseTimeout` breaks. So the fact is needed, and the model shows why. - A design check outside `check.sh`: with a clear of the stamp on a PONG only, in place of the any-bytes clear (the design before the any-bytes rule of coder#488), `NoFalseTimeout` breaks through `PollAndCheckPartial`, the poll that reads only the first frame. So `BytesClearStamp` is needed, and the model shows why. The verifier's run of that variant found 83,746 states. The count depends on how the variant is cut, so I give no count of my own. - Fact fidelity: both verifiers removed each guard in the Lua and every one of the 18 facts flipped to FALSE (26 direct removals in Opus's run). Eight mutants that no fact saw now flip one: five in `tcp.lua` (no `table.insert(pinged, client)`, no ping sent, `judge_silence` called at the tick, `fn` run at once in `after_next_poll`, the `end` of the gap `if` moved above the call), and three guard moves from the last round (the `end` of the `DispatchGuard` if above `on_message`, and `abandon_close_frame` with `release_socket`, or `drop_client`, in the `stop_server` loop). I reran the verifier's 42 mutations on the new `check.sh`: none is blind. - `scripts/tla/test-check-lib.sh`: `COUNT cases=44 failed=0 skipped=0`. - Replays (real Neovim, real sockets), run again on the head before the last three merges of main, on Neovim 0.12.3 and on 0.8.3: `gap-during-handshake` 3 of 3, `short-block-after-ping` 3 of 3, `two-blocks-before-read` 3 of 3, `blocks-before-the-poll` 3 of 3, `protocol-close-window-full` 5 of 5, `stop-before-on-close` 4 of 4. `protocol-close-window-full.lua` changed for the merged code: it uses an interval of 500 ms and checks the open socket after half a keepalive window, because the deadline of `close_client` (merged on main since the replay was written) closes a socket whose Close frame makes no progress for one window, so it no longer stays open for ever while Claude does not read. The first three of the older replays keep `1 of 3`, `3 of 5` and `2 of 4` on main before coder#455 (3d4332c). `short-block-after-ping` keeps `2 of 3` on main before coder#479 (b65d266). `two-blocks-before-read` keeps `1 of 3` on the code of coder#479 on Neovim 0.8.3. `blocks-before-the-poll` keeps `0 of 3` on the first push of coder#488 (f3576ea) and with no clear of the stamp at all. With the gap skip and a clear on a PONG only it keeps `big-message` and `sleep` and breaks `two-blocks`. With the any-bytes clear and no gap skip it keeps `big-message` and `two-blocks` and breaks `sleep`. All on both Neovim versions. Both verifiers reproduced the contrast numbers of the other replays. The `sleep` run of the bytes-only build on Neovim 0.8.3 depends on timing: it kept all three once and two of three in five repeats. The last two replays run Claude in a second Neovim, because an in-process Claude answers only when the blocked loop runs again. - The full busted suite with CI's flags (`--coverage -v --shuffle`) on this branch: seeds 424242 and 9 on the head before the last two merges of main, each 1858 successes, 0 failures, 34 pending. Seed 424242 on `a929777` (merged with main at coder#544) 1887 successes, 0 failures, 34 pending. The last merge (coder#577, `diff.lua` and its spec) I did not run again as a whole suite. `luacheck` (with `--no-unused-args --no-max-line-length`) reports 0 warnings in 196 files. `treefmt` (stylua, prettier, shfmt, shellcheck) reports no change on the 16 files this PR touches. Every `covered.lock` matches the code (`--hash-only`) on the head of this push, and the full `check.sh` of `verify-diff-lifecycle` and `verify-terminal-lifecycle` pass on `a929777`. ## Run it ```bash .agents/skills/verify-ws-connection/check.sh # 2 to 6 min .agents/skills/verify-ws-connection/check.sh --mutants # about 80 min at a load average of 14, after you edit the model or a fact .agents/skills/verify-ws-connection/check.sh --hash-only # no TLC: compares covered.lock with the code NVIM=/path/to/nvim .agents/skills/verify-ws-connection/replays/run.sh blocks-before-the-poll.lua ``` CI's `covered-lock` job already runs every `.agents/skills/verify-*/check.sh`. `SKILL.md` has the rules, how to read a result, how to update the model, and its bounds. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
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.
The bug
A Claude that answers every ping can be dropped with 1011
Keepalive timeout. It happens when Neovim's main loop blocks for 1.0 to 1.5 ping intervals right after a ping was sent (39 s with the default 30 s interval).Whether the tick that follows the block runs before the socket is read depends on the libuv version and on where the block runs. On Neovim 0.8 (libuv 1.44) it runs first after any block. On Neovim 0.9.5 and later it runs first after a block inside a libuv callback that runs after the poll phase, such as a check callback. Then Claude's pong is still unread in the socket. The block is shorter than the wake threshold (
interval * 1.5), solast_pongis not reset. The tick findsnow - last_pongat about 2.3 intervals, above the timeout of 2 intervals, and drops the client.The block has to start within a few milliseconds after a ping, before Claude's pong is read, so this is rare. The promise is still that a Claude that answers pings is never dropped. The WebSocket connection model (
verify-ws-connection, #474) did not catch it: a review of that PR found that the model advances each tick by exactly one interval.The fix
The first tick that finds no pong for two intervals now pings again and sets
client.pong_overdue. The next tick finds the pong that was read in between, or drops the client. A pong clearspong_overdueat the next tick. The wake reset is unchanged.A client that never answers is dropped one tick later than before (one interval, 30 s by default).
server/README.mdsays so.Proof
tests/unit/server/connection_lifecycle_spec.lua): a Claude whose pong is unread at a 1.3-interval late tick is not dropped, and a second late tick does not count against the first once Claude answered. A client that never answers is dropped at the second tick that finds no pong, not the first. I also changedtcp_spec.luaandlog_lines_spec.lua, whose keepalive tests dropped the client at the first tick.origin/main(b65d266) these three spec files give27 successes / 4 failures. With the fix they give31 successes / 0 failures.1256 successes / 0 failures / 12 pendingwith--shuffleseeds 5 and 31337. luacheck: 0 warnings in 153 files. stylua and prettier pass.origin/main, each1 of 2 kept:BROKEN Claude, which answers every ping, is not dropped by one 1.3-interval block: on_disconnect(client_1, 1006, "Connection timeout")at 1040, 1065 and 1054 ms. Three runs with the fix, each2 of 2 kept:no on_disconnect in 3 s.origin/mainand 3.0 to 4.0 with the fix.verify-diff-lifecycle/covered.lockre-recorded andcheck.shgivesRESULT: PASS. Only the file hashes ofserver/client.luaandserver/tcp.luachanged. A dropped client still reacheson_disconnectonce, one tick later.Generated with
xum• Model:anthropic:claude-sonnet-5-5• Thinking:xhigh