Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions .agents/skills/verify-session-lifecycle/SKILL.md
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ Yes, when the diff changes any of these:
- `src/host/programGroup.ts`: the token capture (`captureProgram`, `captureToken`, `readAutogroup`, `parseAutogroup`, `parseProcStat`), the `/proc` reads (`readProcFileIfExists`, `readLiveThreadState`, `readProcStat`, `readShownProcStat`, `isRefusedRead`, `readBootId`), the record (`writeProgramRecord`, `readProgramRecord`, `readProvenProgramGroup`, `readProgramGroup`), the verdict (`judgeProgramGroup`, `readGroupMembers`), and the kill and the probe (`stopProgramGroup`, `isProgramGroupAlive`, `processGroupTarget`, `isProcessGroupAlive` with `groupHasLiveProcess` and `procHidesOtherUsers`, `killProcessGroupBestEffort`, `signalProcessGroup`).
- `src/host/hostMain.ts`: `waitForManifestFromCreate`, `isSessionCommandable`, and in `runHost` the start-up statements (the manifest wait, the `hostPid === process.pid` check, the `host.json` write with `captureHost` and `writeHostRecord`, `createSerialManifestWriter`, `EventLog.open`, `createPty`, `setChildPid`, `captureProgram`), `hangUpProgram` with its kill timer and the `SHUTDOWN_KILL_GRACE_MS` constant, `startIdlePolling` (the idle time-out), `initiateShutdown`, `startShutdown`, `handlePtyExit` with its wait for the program's group, `pty.onExit`, the `SIGTERM` handler, the `resize` and `destroy` handlers, and the last `try` block (the `program.json` write, the start-up manifest write and `rpcServer.listen`).
- `src/host/manifestWriter.ts` `createSerialManifestWriter`.
- `src/cli/commands/gc.ts` `gcSessions`, `src/cli/commands/create.ts` `runCreateCommand`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`.
- `src/cli/commands/gc.ts` `gcSessions`, `src/cli/commands/create.ts` `runCreateCommand` with `waitForReadyHost`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`.
- `src/host/sessionState.ts` `setDimensions`, `requestDestroy`, `recordDestroyed` and `recordExit`, `src/host/eventLog.ts` `EventLog.open`, `src/host/rpcServer.ts` `listen` and `close`, `src/host/rpcClient.ts` `toTransportCliError` (which socket errors read as `HOST_UNREACHABLE`).
- `src/host/hostRecord.ts`: `captureHost`, `writeHostRecord`, `readHostRecord`, `pidExists`, `judgeHost`, `inPidNamespace`, `readTimeNamespace`, `inTimeNamespace`, `readMachineId`, `inHostPidSpace` and `sharesHostPids`.
- `src/storage/manifests.ts` `readValidatedJsonFile`, `replaceFileAtomic`, `replaceFileAtomicSync`, `writeValidatedJsonFileSync`, `writeManifest`, `writeDestroyMarker`.
Expand Down Expand Up @@ -371,7 +371,7 @@ ps -eo pgid=,args= | awk -v g="$pgid" '$1 == g' # prints nothing: the l

Without the guard, `runCreateCommand` gave up after 50 failed `inspect` calls, about 6 seconds, and reported `HOST_UNREACHABLE` (exit 6) without stopping anything. A host that started slowly, on a loaded machine or after a pause, then listened later, and the session ran although `create` had failed (coder/agent-tty#209). The `reconcileSession` call and the `HOST_TIMEOUT` error after the loop never ran, because the last attempt rethrew its error, and the reconcile would have skipped a live host anyway.

Now the last failed attempt calls `host.stop()`, which sends the host SIGTERM through the `ChildProcess` handle that `launchHost` returns, and then rethrows the same error, so the error code does not change. The handle sends nothing once the host has exited, so a reused pid never gets the signal. The host stops its program and records `destroyed` once the group is gone, as for any SIGTERM. `create` writes nothing itself: before the host's start-up write names the program, and without a token, no file names a group that a CLI could prove, so a forced destroy from `create` would record `destroyed` while the program runs. `runHost` registers its SIGTERM handler before it waits for the manifest. A SIGTERM before the spawn makes it return without spawning, and one after the spawn waits for the synchronous start-up block, so the default action can no longer end the host between the spawn and `program.json`. In the model, the give-up sends that SIGTERM, which `HostGetsSigterm` takes. The replay holds the host's start-up write past the readiness loop.
Now every error of the readiness wait (`waitForReadyHost`), the last failed attempt included, makes `runCreateCommand` call `host.stop()`, which sends the host SIGTERM through the `ChildProcess` handle that `launchHost` returns. It then rethrows the error with `details.sessionId` added, so the error code does not change. The handle sends nothing once the host has exited, so a reused pid never gets the signal. The host stops its program and records `destroyed` once the group is gone, as for any SIGTERM. `create` writes nothing itself: before the host's start-up write names the program, and without a token, no file names a group that a CLI could prove, so a forced destroy from `create` would record `destroyed` while the program runs. `runHost` registers its SIGTERM handler before it waits for the manifest, and `facts.mjs` checks that order. A SIGTERM before the spawn makes it return without spawning, and one after the spawn waits for the synchronous start-up block, so the default action can no longer end the host between the spawn and `program.json`. In the model, the give-up sends that SIGTERM, which `HostGetsSigterm` takes. The replay holds the host's start-up write past the readiness loop.

```sh
LOG=$(mktemp)
Expand Down Expand Up @@ -525,6 +525,7 @@ It assumes:
- A destroy that lands between reconcile's last read and its write is still overwritten with failed, for the time until that reconcile finds the destroy marker and writes destroyed again (`ReconcileRepairsDestroyed`). A `list` or `gc` that reads in that time sees `failed`, a terminal status, so gc can remove the folder as it would remove a destroyed one. A reconcile whose process dies in that time leaves `failed` until the next reconcile reads it: that read finds the marker and writes destroyed (`ReconcileRepairsMarked`). `home list` and the dashboard count a session with the marker as destroyed, also in that time. The model has no crash of a reconciling process, so it checks that the repair at the read breaks no rule, not that it heals the crash.
- The idle time-out calls the same `hangUpProgram` as `initiateShutdown`: SIGHUP, then the group kill after `SHUTDOWN_KILL_GRACE_MS`. When the program exits on that SIGHUP, `handlePtyExit` kills the group too, so a process that ignores SIGHUP does not outlive the idle time-out. An idle time-out still ends exited. When the check cannot run (`unknown`), the idle kill sends nothing, and the session ends exited with that process running, as after a program that exits on its own and leaves a process (coder/agent-tty#222). The model leaves both group kills out: they go through `stopProgramGroup` like every kill, and a process that outlives them is one that the program left, which the model keeps after a normal exit anyway.
- Windows has no process groups, so there `processGroupTarget` gives the program's pid, and every kill reaches only that process. `destroy` never re-runs on Windows. There SIGTERM ends the host at once, so a `create` that gives up stops its host only once the manifest names the program, and the next reconcile records `failed` and ends the program. Before that write, `create` leaves the host alone. `CreateStopsOnGiveUp` checks the stop for Linux and macOS.
- A host stopped with SIGSTOP, or with a blocked event loop, takes the SIGTERM of a `create` that gave up only when it runs again. Until then its program runs and the session reads `running`, which R17 allows because the SIGTERM is still on its way. A plain `destroy` fails because the host does not answer, and only `destroy --force` ends such a session sooner.
- A destroy that the program runs, or that someone types into the program's interactive shell, runs inside the program's session, and `rerunInNewSession` runs it again in a new session. The model lets such a destroy start while the program's leader runs, and assumes that it kept `AGENT_TTY_SESSION_ID`, which every process of the program inherits at spawn. A destroy whose environment lost the variable, or whose `create --env` overrode it, is seen through the id comparison only. On Linux that compares the CLI's session id with `childPid`, so it misses such a destroy only before the host's start-up write. Other POSIX systems compare the process group and the controlling terminal, through `/bin/ps`. A terminal is the controlling terminal of one session and of every process in it, so that also finds a job of an interactive shell, which runs in a group of its own. A process without a controlling terminal is seen only through the group.
- The program's processes stay in its process group. A process that leaves the group (`setsid`, or the job control of an interactive shell) is out of reach of the group kill, and it is no witness for the token either. That is case 4 of coder/agent-tty#203, a documented limit with no code change.
- A process that the program left when it exited on its own stays in the program's group and session, so it carries the token. `destroy` of the terminal session kills it through `program.json` (case 1 of coder/agent-tty#203, coder/agent-tty#204). Nothing else stops it: the host does not kill at a normal exit, and gc removes `program.json` with the folder, so a process that a session removed by gc left stays unproven. The model drops a process of another user at a normal exit.
Expand Down
6 changes: 4 additions & 2 deletions .agents/skills/verify-session-lifecycle/coverage.json
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
{
"fingerprints": {
"src/cli/commands/create.ts#runCreateCommand": "5135dd8d24063c90",
"src/cli/commands/create.ts#runCreateCommand": "635715a49fa0273e",
"src/cli/commands/create.ts#waitForReadyHost": "a7fd2ba345b6bfd6",
"src/cli/commands/destroy.ts#runDestroyCommand": "ecaa8b1d572da7c6",
"src/cli/commands/destroy.ts#rerunInNewSession": "cf32d7d082758522",
"src/cli/commands/gc.ts#gcSessions": "667e4ebc3ca3029c",
Expand Down Expand Up @@ -90,7 +91,7 @@
"src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542",
"src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac",
"skill:model/SessionLifecycle.tla": "f7270faba013acff",
"skill:scripts/facts.mjs": "6ae4fd3279517f42",
"skill:scripts/facts.mjs": "b336aed63c9e6cc3",
"skill:scripts/check.sh": "3a47553300cb217a"
},
"callSites": {
Expand Down Expand Up @@ -126,6 +127,7 @@
"src/cli/commandTarget.ts#resolveCommandTarget",
"src/cli/commands/create.ts#readCreateResult",
"src/cli/commands/create.ts#runCreateCommand",
"src/cli/commands/create.ts#waitForReadyHost",
"src/cli/commands/gc.ts#gcSessions",
"src/cli/commands/inspect.ts#runInspectCommand",
"src/cli/commands/record-diff.ts#resolveSessionDirectory",
Expand Down
61 changes: 29 additions & 32 deletions .agents/skills/verify-session-lifecycle/scripts/facts.mjs
Original file line number Diff line number Diff line change
Expand Up @@ -249,45 +249,40 @@ function createFacts() {
};
}

// In runCreateCommand's readiness loop, the catch of an unreachable host
// ends with host.stop() right after its last retry and before it rethrows
// the error. Only a win32 create skips the stop while the manifest names
// no program, so on Linux and macOS, which the model covers, it always stops. launchHost's stop sends SIGTERM through the ChildProcess
// handle, and runHost registers its SIGTERM handler before it spawns the
// program and skips the spawn when a SIGTERM came first.
// In runCreateCommand, the readiness wait is the only statement of a try
// whose catch calls host.stop() and then rethrows, so every error of the
// readiness wait stops the host. Only a win32 create skips the stop while the
// manifest names no program, so on Linux and macOS, which the model covers,
// it always stops. launchHost's stop sends SIGTERM through the ChildProcess
// handle, and runHost registers its SIGTERM handler before it waits for the
// manifest, notes a SIGTERM until the spawn, and skips the spawn when a
// SIGTERM came first.
function stopsOnGiveUp(body) {
let stops = false;
walk(body, (node) => {
if (!ts.isCatchClause(node)) {
return;
}
const last = node.block.statements.at(-1);
if (last === undefined || normalize(last.getText()) !== 'throw error;') {
return;
const stops = body.statements.some((s) => {
if (!ts.isTryStatement(s) || s.catchClause === undefined) {
return false;
}
walk(node.block, (inner) => {
if (!ts.isIfStatement(inner) || !ts.isBlock(inner.thenStatement)) {
return;
}
const st = inner.thenStatement.statements.map((s) =>
normalize(s.getText()),
);
const retry = st.findIndex((s) =>
s.startsWith('if (attempt + 1 < READINESS_MAX_ATTEMPTS) {'),
);
stops ||=
retry >= 0 &&
retry === st.length - 3 &&
st[retry + 1].startsWith('invariant(host !== undefined,') &&
st[retry + 2] ===
"if (process.platform !== 'win32' || manifest?.childPid != null) { host.stop(); }";
});
const tried = s.tryBlock.statements.map((t) => normalize(t.getText()));
const st = s.catchClause.block.statements.map((t) =>
normalize(t.getText()),
);
return (
tried.length === 1 &&
tried[0] ===
'result = await waitForReadyHost(socketFile, sessionDirectory, sessionId);' &&
st.length === 4 &&
st[0].startsWith('invariant(host !== undefined,') &&
st[2] ===
"if (process.platform !== 'win32' || manifest?.childPid != null) { host.stop(); }" &&
st[3] === 'throw withSessionId(error, sessionId);'
);
});
const launch = normalize(
requireDeclaration('src/host/lifecycle.ts', 'launchHost').getText(),
);
const run = requireDeclaration('src/host/hostMain.ts', 'runHost').body;
const handler = indexOfStatement(run, /^process\.on\('SIGTERM'/);
const wait = indexOfStatement(run, /= await waitForManifestFromCreate\(/);
const skip = indexOfStatement(
run,
/^if \(sigterm\.received\) \{\s*await eventLog\.close\(\);\s*return;\s*\}$/,
Expand All @@ -297,7 +292,8 @@ function stopsOnGiveUp(body) {
stops &&
/stop: \(\) => \{ child\.kill\('SIGTERM'\); \}/.test(launch) &&
handler >= 0 &&
handler < skip &&
handler < wait &&
wait < skip &&
skip === spawn - 1
);
}
Expand Down Expand Up @@ -1307,6 +1303,7 @@ function policyFacts() {

const COVERED = [
['src/cli/commands/create.ts', 'runCreateCommand'],
['src/cli/commands/create.ts', 'waitForReadyHost'],
['src/cli/commands/destroy.ts', 'runDestroyCommand'],
['src/cli/commands/destroy.ts', 'rerunInNewSession'],
['src/cli/commands/gc.ts', 'gcSessions'],
Expand Down
8 changes: 7 additions & 1 deletion docs/USAGE.md
Original file line number Diff line number Diff line change
Expand Up @@ -323,10 +323,16 @@ A reconcile that writes over the record at the same moment finds the file right
A `list`, `inspect` or `gc` that reads the session between those two writes sees `failed`, and `home list` and the dashboard count a session that has ended and has that file as destroyed. If the reconciling process is killed between them, the next reconcile finds the file and records the session as `destroyed`. When that repair fails, for example on a full disk, `list` and `inspect` show the session as it reads.
If `destroy` fails after it wrote the file, for example because its manifest write fails, the file stays, and the next reconcile records the session as `destroyed`, also when the session had already ended. Nothing deletes the file before `gc` removes the session folder, because a reconcile that read before the destroy can still write after it.
A host that died after it recorded the session as ended leaves its socket. `gc`, and a `destroy` of a `destroyed` session, remove that socket when the manifest names no host pid or the host check below reads the host as ended.
When `create` cannot reach its new host within about 6 s, it fails with `HOST_UNREACHABLE` or `HOST_TIMEOUT` and tells the host to stop.
When `create` cannot reach its new host, it fails and tells the host to stop. It fails with `HOST_UNREACHABLE` (exit 6) after about 6 s when nothing listens on the socket, and with `HOST_TIMEOUT` (exit 5) after about 10 s when the host accepts the connection but does not answer.
`create` also tells the host to stop when it fails for another reason after it wrote the session's first manifest, for example when it cannot read that manifest again. Each such error names the session in `details.sessionId`.
When that first manifest write fails, `create` removes the session folder. The host waits for the manifest only while `create` runs, so it then exits without starting the program.
On Linux and macOS it sends the host SIGTERM, and the host stops the program the way `destroy` does and records the session as `destroyed` once the program's group has ended, also while its start-up is still slow.
`create` exits before the host has ended the session, so a caller that checks at once can still read `running` or `destroying`.
The host records `destroyed` right after the program exits on the SIGHUP, or about 2 s later, after the shutdown grace, when the program ignores SIGHUP. A host whose start-up write is still slow records it only after that write.
Once the session reads `destroyed`, a `destroy` of it exits 4 with `SESSION_ALREADY_DESTROYED`.
A host that has already died, or that gets the SIGTERM before it spawns the program, leaves the session to the reconcile above: the session reads `running` until the next reconcile records it `failed`, and no program runs.
When the host cannot end the program's group, for example a process of another user, the session stays `destroying` with the host alive. That host never listened, so a plain `destroy` then fails with `HOST_UNREACHABLE` (exit 6), and only `destroy --force` can end the session.
A host stopped with SIGSTOP, or with a blocked event loop, handles the SIGTERM only when it runs again. Until then the program runs and the session reads `running`. A plain `destroy` fails because the host does not answer, and only `destroy --force` ends the session sooner.
On Windows, SIGTERM ends the host at once, so the host cannot stop the program itself. There `create` sends it only once the manifest names the program: the session then reads `running` with a dead host until the next reconcile records it `failed` and ends the program. Before the host's first manifest write, `create` leaves the host alone, as before this change, so a host that starts late can still serve the session.

On Linux, `destroy` and reconcile never kill a process group that they cannot prove is the session's.
Expand Down
Loading
Loading