diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index a4e900b1..02592af5 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -55,7 +55,7 @@ Yes, when the diff changes any of these: You do not have to judge this by hand. The check prints `STALE` when any of these changed since the sync commit. -CI runs the check in the `lifecycle-model` job. Its first share calls `scripts/check.sh --drift-only`, which compares the guard values and the covered code with `coverage.json` and needs no Java, and fails on `STALE`. The whole check runs only when `coverage.json` differs from the base of the pull request or merge group, in eight jobs with `CHECK_SHARD=/8` and `CHECK_JOBS=12`. Each job runs every eighth run that expects pass and every eighth of the rest, because the runs that expect pass explore the whole model and take most of the time, and it starts all its runs at once. With the model of #324, a share took 11 to 33 min. +CI runs the check in the `lifecycle-model` job. Its first share calls `scripts/check.sh --drift-only`, which compares the guard values and the covered code with `coverage.json` and needs no Java, and fails on `STALE`. The whole check runs only when `coverage.json` differs from the base of the pull request or merge group, in nine jobs with `CHECK_SHARD=/9` and `CHECK_JOBS=12`. Each job runs every ninth run that expects pass and every ninth of the rest, because the runs that expect pass explore the whole model and take most of the time, and it starts all its runs at once. With the model of #324, a share took 11 to 33 min. ## Run it @@ -65,13 +65,13 @@ From the repo root: .agents/skills/verify-session-lifecycle/scripts/check.sh ``` -It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. `CHECK_JOBS` runs run at a time (a new one starts as soon as one ends; the bash 3.2 of macOS waits for each batch). The runs that expect pass share the CPUs as TLC workers, at least 1 each, and the others keep 1 worker, so their traces stay the shortest. Fourteen runs explore more than 20 million distinct states each, so `CHECK_JOBS=92` starts every run at once and takes about as long as the longest run. `JAVA=/path/to/java` picks another Java. `TLA2TOOLS_JAR=/path/to/tla2tools.jar` uses a jar you already have, which must be the same 1.7.4 build. `CHECK_OUT=` keeps the results in that folder (default: a new temp folder, printed at the end). +It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. `CHECK_JOBS` runs run at a time (a new one starts as soon as one ends; the bash 3.2 of macOS waits for each batch). The runs that expect pass share the CPUs as TLC workers, at least 1 each, and the others keep 1 worker, so their traces stay the shortest. Fifteen runs explore more than 20 million distinct states each, so `CHECK_JOBS=94` starts every run at once and takes about as long as the longest run. `JAVA=/path/to/java` picks another Java. `TLA2TOOLS_JAR=/path/to/tla2tools.jar` uses a jar you already have, which must be the same 1.7.4 build. `CHECK_OUT=` keeps the results in that folder (default: a new temp folder, printed at the end). What it does: 1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the forty guards that the rules depend on and the status sets of the policy table, and it hashes each covered function with comments and layout removed. 2. It writes one TLC config per run, with those facts as constants. A guard that is not in the code, in the expected place and order, reads FALSE, and the model then runs without it. -3. It runs TLC 92 times and prints one line per run. +3. It runs TLC 94 times and prints one line per run. 4. It compares the guard values, the status sets, the hashes and the call sites with `coverage.json`. Exit codes: 0 means every run gave the expected result and the covered code matches the sync record. 1 means at least one run gave an unexpected result; the line says `UNEXPECTED`. 3 means every result was as expected, but covered code changed since the sync commit; that is not a pass, so follow "When you change covered code on purpose". 2 means a tool could not run. When both 1 and 3 apply, the exit code is 1. @@ -91,7 +91,9 @@ At the sync commit, the expected results are: | `mutant-ProbeCountsDeniedGroup-no-token`, `mutant-KillsProgramGroup-no-token`, `mutant-HostWaitsForGroup-no-token`, `mutant-ReconcileWaitsForGroup-no-token` | violated | The same without a token. The fallback depends on these guards as the code before `program.json` did. With a token, the token check reads a process of another user in view, so only this path checks `ProbeCountsDeniedGroup`. | | `mutant-UnseenBothGuards-unseen` | violated | With neither the freeze nor the wait's probe, the kill through the token finds no member in view, the wait reads the group gone, and `destroy` records destroyed while the fork chain runs (R11). Either guard alone keeps R11. | | `mutant-GcProbesUnseenGroup-unseen` | violated | Without the probe, gc reads the fork chain ended and removes `program.json` while it runs (R20). | -| `mutant-GcFreezesUnseenGroup-unseen-zombies` | violated | `ZombiesInView`: under a PID 1 that never reaps, the fork chain also leaves zombies in view. Without the freeze, gc reads the group ended and removes `program.json` while the chain runs (R20). With every guard, `ZombiesInView` changes nothing, so `current-unseen` covers the pass run. | +| `current-unseen-zombies`, the code as it is with a fork chain behind zombies of its group, every rule | pass | `ZombiesInView`: under a PID 1 that never reaps, the fork chain also leaves zombies in view. Scans that show only zombies read the group ended whatever the wait's probe finds, so the freeze alone keeps R11 here. | +| `mutant-FreezesUnseenGroup-unseen-zombies` | violated | R11: without the freeze, the kill through the token finds no member in view, the wait reads the chain behind its zombies ended, and `destroy` records destroyed while it runs. | +| `mutant-GcFreezesUnseenGroup-unseen-zombies` | violated | Without the freeze, gc reads the group ended and removes `program.json` while the chain runs (R20). | | `current-unseen-misses`, the code as it is with a fork chain that every freeze misses, every rule | pass | `FreezeMisses`: no freeze brings a member of the chain into view, as when a SIGCONT from another process comes before each judgement. The wait's probe reads the chain alive, so `destroy` fails with `HOST_TIMEOUT` instead of recording destroyed. | | `mutant-WaitProbesUnseenGroup-unseen-misses` | violated | R11: without the probe, the wait after a missed freeze reads the chain ended, and `destroy` records destroyed while it runs. | | `mutant-ReusedIdReadsGone` | pass | Without the guard, a group that took the program's id reads alive, so no wait of `destroy` passes while it runs, and `WitnessWaitPassesReusedId` is never reached. The model has no rule for a wait that never ends, so this run checks that witness instead of a rule. | @@ -549,7 +551,7 @@ kill -0 "$other" && echo alive # alive With a token, a kill needs a live member of the group in view, and a wait reads the group gone once no scan shows one. A program whose processes each fork their successor and end within about 2 ms, a fork chain, is almost never in view: by the time a scan reads a pid that its `/proc` listing showed, that process has ended, and the listing missed its successor. `stopProgramGroup` then killed nothing, the wait after it read the group gone, and `destroy` recorded `destroyed` while the chain ran (coder/agent-tty#244). -Now `stopProgramGroup` sends a group that `judgeLiveGroup` reads gone SIGSTOP and judges it again, until the loop's attempts run out. A scan can also show a member that ends before its autogroup read, so the judgement reads `unknown`, or a witness that ends before it is read again. Those judgements get SIGSTOP and another judgement too: every judgement that gets no kill freezes the group, except `unproven` and an `unknown` whose members without an autogroup are all stopped (`running` false) or whose boot id `/proc` refuses. A stopped member cannot end, so `/proc` refused its autogroup, and a group that job control stopped gets no signal. Before its first freeze, a group that shows any member that job control or a tracer stopped gets no SIGSTOP either (`showsStoppedMember`), so the SIGCONT after the judgements cannot resume that member beside a running one. A SIGSTOP takes effect only when the kernel next runs a member (about 30 us idle, longer under load), so `stopProgramGroup` and gc's `judgeFrozenGroup` wait `STOP_SETTLE_MS` (1 ms) after each SIGSTOP before they judge, and a member that still runs gets another SIGSTOP within the 5 judgements. Without that, a loaded CI runner saw `destroy` record `destroyed` after such a judgement while the chain ran. That freezes only a group id that a judgement of gone would freeze too, never one that reads `unproven`. Each judgement that freezes sends SIGSTOP again, so a member that a SIGCONT from elsewhere resumed stops again. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace, so `procShowsOwnPidSpace` reads false and no SIGSTOP goes out: the group id can name the CLI's own group there. The kernel delivers a group signal also to a child that a member forks during the delivery, so the whole chain stops, and a stopped process stays in view. The next judge finds a stopped member with the token, and the group gets the kill. A frozen group that gets no kill, because its members carry another autogroup, only zombies are left, `/proc` refuses the autogroup of its stopped member, or a scan throws, gets SIGCONT from a `finally` block. The model has no member that a scan shows and then cannot read, so it relies on this freeze. In the model, the constant `Unseen` hides every process of the program from the scans: without the guard the kill through the token kills nothing, and, without `WaitProbesUnseenGroup` (below), the wait reads the group gone. `current-unseen` checks every rule with `Unseen`, and `mutant-UnseenBothGuards-unseen`, without the freeze and the wait's probe, must violate R11. The integration test "destroy ends a fork chain that no scan of /proc shows" in `test/integration/lifecycle.test.ts` runs `test/fixtures/fork-chain.py` in a session. +Now `stopProgramGroup` sends a group that `judgeLiveGroup` reads gone SIGSTOP and judges it again, until the loop's attempts run out. A scan can also show a member that ends before its autogroup read, so the judgement reads `unknown`, or a witness that ends before it is read again. Those judgements get SIGSTOP and another judgement too: every judgement that gets no kill freezes the group, except `unproven` and an `unknown` whose members without an autogroup are all stopped (`running` false) or whose boot id `/proc` refuses. A stopped member cannot end, so `/proc` refused its autogroup, and a group that job control stopped gets no signal. Before its first freeze, a group that shows any member that job control or a tracer stopped gets no SIGSTOP either (`showsStoppedMember`), so the SIGCONT after the judgements cannot resume that member beside a running one. A SIGSTOP takes effect only when the kernel next runs a member (about 30 us idle, longer under load), so `stopProgramGroup` and gc's `judgeFrozenGroup` wait `STOP_SETTLE_MS` (1 ms) after each SIGSTOP before they judge, and a member that still runs gets another SIGSTOP within the 5 judgements. Without that, a loaded CI runner saw `destroy` record `destroyed` after such a judgement while the chain ran. That freezes only a group id that a judgement of gone would freeze too, never one that reads `unproven`. Each judgement that freezes sends SIGSTOP again, so a member that a SIGCONT from elsewhere resumed stops again. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace, so `procShowsOwnPidSpace` reads false and no SIGSTOP goes out: the group id can name the CLI's own group there. The kernel delivers a group signal also to a child that a member forks during the delivery, so the whole chain stops, and a stopped process stays in view. The next judge finds a stopped member with the token, and the group gets the kill. A frozen group that gets no kill, because its members carry another autogroup, only zombies are left, `/proc` refuses the autogroup of its stopped member, or a scan throws, gets SIGCONT from a `finally` block. The model has no member that a scan shows and then cannot read, so it relies on this freeze. In the model, the constant `Unseen` hides every process of the program from the scans: without the guard the kill through the token kills nothing, and, without `WaitProbesUnseenGroup` (below), the wait reads the group gone. `current-unseen` checks every rule with `Unseen`, and `mutant-UnseenBothGuards-unseen`, without the freeze and the wait's probe, must violate R11. With `ZombiesInView`, the freeze alone keeps R11: `current-unseen-zombies` checks every rule, and `mutant-FreezesUnseenGroup-unseen-zombies`, without the freeze, must violate R11. The integration test "destroy ends a fork chain that no scan of /proc shows" in `test/integration/lifecycle.test.ts` runs `test/fixtures/fork-chain.py` in a session. ```sh id=$(node --import tsx src/cli/main.ts create --json -- sh -c "python3 test/fixtures/fork-chain.py 30 0.002 $PWD/beat & wait" | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))') diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index ad480ee5..dbd155ea 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -151,7 +151,7 @@ "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", "skill:model/SessionLifecycle.tla": "9d2f5e19d5de78d2", "skill:scripts/facts.mjs": "36ed7de152b0c580", - "skill:scripts/check.sh": "81d1f6f959f1dfca" + "skill:scripts/check.sh": "eaa2d6a36689fc17" }, "callSites": { "writeManifest": [ diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index 48988076..966582c7 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/check.sh +++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh @@ -293,8 +293,11 @@ write_run current-unseen pass "$RULES" "" "the code with a program that no scan write_run mutant-UnseenBothGuards-unseen violated DestroyedProgramStopped "FreezesUnseenGroup=FALSE WaitProbesUnseenGroup=FALSE" "with neither the freeze nor the wait's probe, the kill finds no member in view, and destroy records destroyed while a fork chain runs" DestroyedProgramStopped write_run mutant-GcProbesUnseenGroup-unseen violated RemovedSessionStopped "GcProbesUnseenGroup=FALSE" "without the probe, gc removes program.json while a fork chain that the program left runs" RemovedSessionStopped # Under a PID 1 that never reaps, the chain also leaves zombies in view. -# With every guard, that changes nothing, so current-unseen covers it. +# Scans that show only zombies read the group ended whatever the wait's +# probe finds, so only the freeze keeps destroy from recording destroyed. ZOMBIES=TRUE +write_run current-unseen-zombies pass "$RULES" "" "the code with a fork chain behind zombies of the program's group: every rule holds" +write_run mutant-FreezesUnseenGroup-unseen-zombies violated DestroyedProgramStopped "FreezesUnseenGroup=FALSE" "without the freeze, the kill finds no member in view, the wait reads the chain behind its zombies ended, and destroy records destroyed while it runs" DestroyedProgramStopped write_run mutant-GcFreezesUnseenGroup-unseen-zombies violated RemovedSessionStopped "GcFreezesUnseenGroup=FALSE" "without the freeze, gc reads a fork chain behind its zombies ended and removes program.json while it runs" RemovedSessionStopped ZOMBIES=FALSE # Every freeze misses the chain. The wait then times out. diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 79e8ab2d..f6a8c35f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -221,8 +221,8 @@ jobs: # Model-checks the session lifecycle with the verify-session-lifecycle # skill. Share 1 checks that coverage.json matches the facts and the - # covered code. Each of the 8 shares starts all its runs at once - # (CHECK_JOBS 12: with the model of #327, 10 to 12 runs, of which at most + # covered code. Each of the 9 shares starts all its runs at once + # (CHECK_JOBS 12: of the 94 runs, a share gets 9 to 11, of which at most # 2 explore the whole model), and check.sh gives those runs the 4 vCPUs as # TLC workers. So a share takes about as long as its longest run. With the # model of #324, the shares took 11 to 33 min, and 15 to 43 min with 1 TLC @@ -235,8 +235,8 @@ jobs: strategy: fail-fast: false matrix: - shard: [1, 2, 3, 4, 5, 6, 7, 8] - name: lifecycle-model (${{ matrix.shard }}/8) + shard: [1, 2, 3, 4, 5, 6, 7, 8, 9] + name: lifecycle-model (${{ matrix.shard }}/9) steps: - name: Check out repository uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6 @@ -272,7 +272,7 @@ jobs: if: steps.inputs.outputs.tlc == 'true' env: CHECK_JOBS: '12' - CHECK_SHARD: ${{ matrix.shard }}/8 + CHECK_SHARD: ${{ matrix.shard }}/9 run: .agents/skills/verify-session-lifecycle/scripts/check.sh quality-gates: diff --git a/docs/USAGE.md b/docs/USAGE.md index f8b2bf3d..19559301 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -366,7 +366,7 @@ On macOS and the BSDs, `destroy --force` kills the host only when `/bin/ps` show Limits: 1. `destroy` does not kill a process that has left the program's process group. A process leaves the group when it calls `setsid` (for example `setsid cmd` or a daemon), or when an interactive shell with job control runs it as a job (for example `cmd &` typed into `bash -i`). Stop such a process yourself, or keep it in the program's group. -2. Some sessions have no autogroup record: sessions on macOS and Windows, on Linux kernels without autogroups (`/proc/self/autogroup` is missing), on Linux when `/proc` refuses to show the autogroup, the boot id or the host's pid namespace at start-up, and sessions that an agent-tty version without `program.json` created. For these sessions, `destroy --force`, reconcile and the host's own kill at shutdown or at the idle time-out kill the process group (on Windows, the process) that `session.json` names, without the check, so such a kill can reach an unrelated process that took the group id after the program's group ended. `destroy` of a session whose program has already exited kills nothing. A `program.json` that agent-tty cannot read as a record, for example one that a newer version wrote, proves nothing: `destroy` and reconcile kill nothing for that session. +2. Some sessions have no autogroup record: sessions on macOS and Windows, on Linux kernels without autogroups (`/proc/self/autogroup` is missing), on Linux when `/proc` refuses to show the autogroup, the boot id or the host's pid namespace at start-up, and sessions that an agent-tty version without `program.json` created. For these sessions, `destroy --force`, reconcile and the host's own kill at shutdown or at the idle time-out kill the process group (on Windows, the process) that `session.json` names, without the check, so such a kill can reach an unrelated process that took the group id after the program's group ended. `destroy` of a session whose program has already exited kills nothing. A `program.json` that agent-tty cannot read as a record, for example one that a newer version wrote, proves nothing: `destroy` and reconcile kill nothing for that session. Where `/proc` belongs to another pid namespace, as after `unshare --pid --fork` without `--mount-proc`, and the PID 1 of that namespace never reaps, a `destroy` of such a session fails with `HOST_TIMEOUT` after the program's group has ended: no scan of `/proc` shows the group's zombies, and `kill(-pgid, 0)` still finds them. 3. The check and the kill are separate system calls, a few microseconds apart. If every process of the group exits and an unrelated process takes the group id in that time, the kill reaches the unrelated process. No system call kills a process group through a handle, so this window remains. A group that no scan shows, or whose process ends while agent-tty reads it, gets SIGSTOP before each check and SIGCONT when the checks fail. A group that shows a process that job control stopped (`kill -STOP`, or Ctrl-Z in a shell) gets no SIGSTOP, so that SIGCONT cannot resume the process. `gc` sends the same two signals to a group whose scans show only zombies while its id still names a process (see item 5). A CLI whose `/proc` belongs to another pid namespace sends no SIGSTOP. If the unrelated group is a job of an interactive shell, the shell reports the job as stopped, and after the SIGCONT the job runs in the background. If agent-tty itself dies between the two signals (SIGKILL, SIGINT, SIGTERM, SIGHUP, or the out-of-memory killer), an unrelated group that took the id stays stopped, and a later `destroy` does not resume it. Resume it with `kill -CONT -- -`, where `` is the Child PID that `inspect` shows. 4. The host writes `program.json` a few milliseconds after it starts the program. We timed 150 `create` calls on Linux, from the return of node-pty's spawn to the renamed `program.json`, at 1-minute load averages of 38 to 83: the median was 2.8 ms, the 90th percentile 4.3 ms, and the longest 66 ms. If the host dies in that window and the program ignores the hang-up signal, no file names the program, and `destroy` cannot end it. 5. `gc` kills nothing. It keeps the folder of a session that is not `destroyed` only while it proves that the program's group runs: the autogroup record in `program.json` proves that a live process of the group is the program's, or the group id still names a process that no scan of `/proc` shows, such as a fast fork chain. When the scans show only zombies of the group while its id still names a process, as for a fork chain under a PID 1 that never reaps, `gc` sends the group SIGSTOP, checks it again, and sends SIGCONT, up to twice in each of up to ten checks of the group, and it keeps the session only when such a check proves the group. A group that has ended gets all 20 frozen checks: with about 2,300 processes in `/proc`, they took about 3.5 s at a load of 90. Another `gc` or a `destroy` that runs at the same time can send SIGCONT before a frozen check. Only when that happens before all 20 of them can a live process of the chain escape every scan, and `gc` then removes the folder of a session whose group still runs. A kept session gets the reason "the session's program group still runs (destroy ends it)". When `gc` cannot check the group, it removes `program.json` with the folder, as it does without an autogroup record (see item 2). That happens in another pid namespace than the one that `host.json` names, for example after a container restart that keeps the agent-tty home, when `host.json` cannot be read, and when `/proc` refuses the boot id or the autogroup of a live process of the group, or hides the processes of other users. Otherwise such a session would stay forever, because no `destroy` can prove its group gone. A process that the program left can then no longer be stopped by agent-tty. Run `destroy` before `gc` when a program can leave processes behind.