Terminal Session Correctness

Design & test report · branch nwparker/sta-3077-reattach-pane-cardinality · PRs #13110, #13111

1 · What sits behind one terminal

Five separate things line up behind the rectangle you see.

Anatomy of a terminal⤢ zoom

The PTY is the real shell doing the work. The binding is the note connecting it to your pane. On a remote machine a lease is a second note saying “we still own that shell.” Every failure below is one of those notes pointing at the wrong thing.

2 · The reported failure

Reconnect growth — a real customer report⤢ zoom

The remote machine also fills with unused shells until it refuses to start more. A second, worse variant: an AI coding agent resumed twice — two claude processes writing to one conversation file. One report reached five.

3 · Three root causes

Cause 1 — the lease forgot its pane

A lease identified a shell but never checked which pane it belonged to. Every reconnect added a note; nothing removed one.

Lease accumulation⤢ zoom

FIXED A lease is identified by its pane. One pane, one live lease. Superseded leases are marked expired, not killed — the remote shell keeps running, because losing a note is not proof the shell died.

Cause 2 — reconnecting could create panes

Reattach decision⤢ zoom

FIXED Reattach binds only. Opening a new terminal still creates, exactly as before.

Cause 3 — a living shell reported as dead

Real meaning	Reported as	Consequence
This shell is gone	SESSION_EXPIRED	correct
Shell is fine — output pipe needs re-establishing	SESSION_EXPIRED	respawn → agent resumed twice

FIXED The second case has its own message, and respawn now requires positive proof. Anything unrecognised is “unknown”, which never justifies a replacement.

4 · The rule underneath all of it

Unknown is not dead⤢ zoom

The liveness check also became three-valued. It previously returned yes/no, so a provider whose socket was down could only answer “no” — meaning dead — when the honest answer was “I can’t see”.

5 · What changed

#	Change	Prevents
1	Reattach binds, never creates	Ghost panes
2	Leases identified by pane	2 → 19 → 20 growth
3	Heal already-corrupted lease data	Existing installs stuck at 20
4	“Needs re-establishing” ≠ “expired”	Duplicate agent resume
5	Liveness can answer “unknown”	Live shells declared dead
6	One PTY’s failure can’t drop the shared channel	One bad pane killing every session on a host

Change 6 — blast radius⤢ zoom

6 · How we decide a test is worth trusting

The four-step proof⤢ zoom

Delete a real guard, not the test. Prefer one clause at a time — a mutation reddening exactly one claim proves the claims independently. Watch it fail yourself: six of twelve oracles were personally re-verified, and two of those re-checks overturned the original claim.

7 · Why “same id” is not good enough

The most valuable lesson here. Break the quit path so it destroys shells instead of detaching, then restart:

tab id    same ✓
pane id   same ✓
pty id    same ✓
OS pid    13756 → 8852   ✗
start     02:01:29.337 → 02:01:34.728   ✗

Every id-only restart test stays green here.
Your shell is gone.

Proving the process really survived⤢ zoom

8 · Journey status

#	Journey	State	Why
1	Local restart — macOS · Linux · Windows	PROVEN	Clause-selective on all three platforms
2	Daemon & physical WSL	PROVEN	Clause-selective on macOS, Linux, WSL2
4	Concurrent multi-host	BY CONSTRUCTION	A mux is per-host — dispose cannot cross hosts, so there is nothing to break
3	Lazy discovery	NO SELECTIVE MUTATION	Removing the real guard breaks setup before the clause is reached
6	Docker MaxSessions=1	PARTIAL	2 clauses redden; a third survived four guard removals
12	Mixed versions	WITHDRAWN	The token never crosses a version boundary in production
13	Performance & scale	IN PROGRESS	1 of 10 dimensions measured; rest running
5, 10, 11	Device proof · identity reset · namespace admission	NO SUBJECT	The code does not exist. No oracle is writable at any effort.

Why a property may resist proof⤢ zoom

9 · Traps that can fake a result

Trap	Effect	Mitigation
Shared temp directory — the harness writes a pointer to a machine-wide path	Concurrent runs can fake a red and hide a real one	Isolated TMPDIR per run
Stale build — e2e runs a built app	You tested the old code	Check build timestamp against source edit
Mutation silently didn’t apply	Test stays green, looks like “no teeth” — wrong conclusion	Verify the mutation landed before believing the result
Serial mode reports “did not run”	A skip mistaken for a pass	Re-run the others alone under the same mutation

Two of our own tests were broken in ways only real hardware revealed: one failed on every Linux run (a single unpolled read where its sibling polls for 15s), and one could not execute at all on Windows (echo $$ and ps don’t exist there).

10 · Open decisions

ID	Decision	Blocks
D2	Re-scope G4? It demands an architecture where 0 of 394 files exist, measured at +62k LOC — the approach that already failed at 0/13.	G4, G1, G3
D3	Strike or defer J5 / J10 / J11? They have no production subject.	3 journeys
D4	Architectural gates need a “reviewed diff + file list” receipt; the doc’s red-SHA template makes them structurally unpromotable.	G0, G1, G4
D5	The input quarantine is load-bearing, not superseded. Deleting it re-opens a verified rm -rf hazard. Amend the clause, or accept something weaker on remote hosts?	G6

11 · Corrections made along the way

Included because a report without them is not trustworthy.

Claim	Outcome
“The reconnect e2e proves the fix”	Retracted — passed with the fix removed, twice, isolated
“Cross-version tests confirm old clients are safe”	Withdrawn — they exercise a route production never takes
“mayCreate fixes reattach”	Was inert — no production caller for several commits
“A branded binding type is the fix”	Rejected — three claims false; would have added a second identity system
“Fixtures compile as production”	Corrected — none ship; the sweep was stopped
“bash 5.3.9 causes the WSL failure”	Corrected — macOS runs the same version and passes