diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index eb9202d4..a4e900b1 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -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. Thirteen runs explore more than 20 million distinct states each, so `CHECK_JOBS=90` 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. 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). What it does: -1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the thirty-nine 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. +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 90 times and prints one line per run. +3. It runs TLC 92 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. @@ -89,8 +89,11 @@ At the sync commit, the expected results are: | `witness-*-no-token` | violated | Eight of those states without a token: a `create` that gave up recorded the session destroyed, a crash is reconciled, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` and `destroy --force`, and a reconcile writes destroyed again over the failed that it wrote. They show that `current-no-token` reaches the fallback kill and the EPERM probe. | | `mutant-CreateRecordsHostPid`, `mutant-HostWaitsForManifest`, `mutant-ReconcileRereads`, `mutant-HostSerializesWrites`, `mutant-ReconcileSkipsLiveHost`, `mutant-HostStopsAfterTerminalWrite`, `mutant-DestroyRecordsDestroyed`, `mutant-DestroyKeepsExitCode`, `mutant-ManifestWriteNeedsFolder`, `mutant-KillsProgramGroup`, `mutant-HostWaitsForGroup`, `mutant-ReconcileWaitsForGroup`, `mutant-ReRunsInNewSession`, `mutant-InsideCheckReadsEnv`, `mutant-RecordsProgramSync`, `mutant-ProvesGroupOwnership`, `mutant-DestroyStopsLeftovers`, `mutant-FallbackNeedsFolder`, `mutant-ReconcileRepairsDestroyed`, `mutant-CreateStopsOnGiveUp`, `mutant-TokenNamesProgram`, `mutant-ProvesHostPid`, `mutant-GcBothChecks`, `mutant-GcKeepsLiveGroup`, `mutant-ShutdownBothChecks` | violated | Each run removes a guard from the model and checks only the rule that the guard protects. That rule must break, which shows the check can fail. | | `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-FreezesUnseenGroup-unseen`, `mutant-GcProbesUnseenGroup-unseen` | violated | Without the freeze, 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). | +| `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-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. | | `mutant-ReconcileRepairsMarked` | violated | R18: without the guard, a `list` that died between its write and its repair leaves `failed`, and the next reconcile skips it as it skips any terminal manifest. | | `mutant-ReconcileSkipsTerminal` | pass | The re-read in `reconcileSession` also returns on a terminal manifest, so the first terminal return alone is redundant. | @@ -546,7 +549,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. 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 the wait reads the group gone. `current-unseen` checks every rule with `Unseen`, and `mutant-FreezesUnseenGroup-unseen` 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. 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))') @@ -554,6 +557,12 @@ sleep 1; node --import tsx src/cli/main.ts destroy "$id" --json # ok: true, de a=$(cat beat); sleep 1; [ "$a" = "$(cat beat)" ] && echo ended # ended ``` +### `WaitProbesUnseenGroup`: a missed freeze lets destroy record destroyed (R11) + +When the probe `kill(-pgid, 0)` found the group but no scan showed a member, live or zombie, `isProcessGroupAlive` read the group ended: the processes that the probe found had been reaped before the scans. A fork chain that no scan shows reads the same way. So when the freeze of `stopProgramGroup` missed the chain, the wait after it read the running chain ended, and `destroy` recorded `destroyed`. A loaded CI runner hit that through the judgements that the freeze did not cover before (an `unknown` from a member that ended before its autogroup read). + +Now `isProcessGroupAlive` probes again after such scans. Processes that were reaped are gone then (ESRCH), and the group reads ended. A fork chain still holds the id, so the group reads alive, and the wait times out with `HOST_TIMEOUT` instead. Scans that show only zombies still read the group ended, because under a PID 1 that never reaps the zombies of a killed group stay. So under such a PID 1, a freeze that misses a chain still lets `destroy` record destroyed. The model leaves that case out: `current-unseen-misses` runs without `ZombiesInView`. In the model, the environment constant `FreezeMisses` makes every freeze of an `Unseen` group miss, as when a SIGCONT from another process comes before each judgement, and `ProbeFindsUnseen` is the second probe. The probe of a group without a token (`ProbeSees`) now reads the program's processes alive under `Unseen` only through that probe, as the code does. `current-unseen-misses` checks every rule with `FreezeMisses`, and `mutant-WaitProbesUnseenGroup-unseen-misses` must violate R11. The unit tests "is alive while no scan shows a member and the probe finds the id" and "on linux, reads a group ended when no scan shows a member and the second probe finds none" in `test/unit/host/programGroup.test.ts` cover both reads. + ## When you change covered code on purpose 1. Read the diff of every item that `STALE` lists, and the commits that the check prints. For a change that is not committed yet, read `git diff`. diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 05ae0f31..ad480ee5 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -33,6 +33,7 @@ "RecordsProgramSync": true, "ProvesGroupOwnership": true, "FreezesUnseenGroup": true, + "WaitProbesUnseenGroup": true, "FallbackNeedsFolder": true, "UnsharedGroupReadsUnknown": true, "TokenNamesProgram": true, @@ -53,7 +54,7 @@ "src/cli/commands/gc.ts#defaultDependencies": "ae2347cdb778b488", "src/host/programGroup.ts#provenProgramGroupRuns": "7b50817618b4b769", "src/host/programGroup.ts#judgeGroupForGc": "fb133ba2739116d1", - "src/host/programGroup.ts#judgeFrozenGroup": "e3a6c281e3f579fc", + "src/host/programGroup.ts#judgeFrozenGroup": "8bfe9ea5c92a1c8f", "src/host/programGroup.ts#FROZEN_JUDGEMENTS": "d4eb06aa7addbaa9", "src/host/programGroup.ts#isUnreadableGroupError": "e2d852aa5b45cb53", "src/host/programGroup.ts#UNREADABLE_ERRNOS": "24de7f719ccf14be", @@ -121,11 +122,11 @@ "src/host/programGroup.ts#procHidesOtherUsers": "214f60a56d6573fa", "src/host/programGroup.ts#groupHasLiveProcess": "1d8026f335463a72", "src/host/programGroup.ts#scanGroup": "babc9d5767424243", - "src/host/programGroup.ts#isProcessGroupAlive": "ce1b8fca10085d51", + "src/host/programGroup.ts#isProcessGroupAlive": "cb20b5d3ec5d2979", "src/host/programGroup.ts#killProcessGroupBestEffort": "6d5d47cb5697681b", "src/host/programGroup.ts#signalProcessGroup": "c5a3a84361b67aa1", "src/host/programGroup.ts#isProgramGroupAlive": "f6fe01a280824f82", - "src/host/programGroup.ts#stopProgramGroup": "215a685d9337aeb3", + "src/host/programGroup.ts#stopProgramGroup": "cf13959e57ccad10", "src/host/programGroup.ts#procShowsOwnPidSpace": "ac852506311bb328", "src/host/rpcClient.ts#toTransportCliError": "dd6531349c62bcbd", "src/host/sessionState.ts#SessionState.setDimensions": "08c4f06122d157e9", @@ -148,9 +149,9 @@ "src/host/hostMain.ts#runHost(final try)": "e0615a9709fefb67", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "cd8639012467f13e", - "skill:scripts/facts.mjs": "ff97d3d2dfab5811", - "skill:scripts/check.sh": "17f2ce5bd1b1b090" + "skill:model/SessionLifecycle.tla": "9d2f5e19d5de78d2", + "skill:scripts/facts.mjs": "36ed7de152b0c580", + "skill:scripts/check.sh": "81d1f6f959f1dfca" }, "callSites": { "writeManifest": [ diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index 7906292c..3c66b8fc 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -137,6 +137,9 @@ CONSTANTS ProvesHostPid, \* lifecycle.ts, hostRecord.ts: destroy --force \* kills the host only while its pid shows the \* boot id and start time that host.json holds + WaitProbesUnseenGroup, \* programGroup.ts: isProcessGroupAlive probes + \* the group again when no scan shows a member, + \* and reads it alive while the probe finds it FreezesUnseenGroup, \* programGroup.ts: stopProgramGroup sends \* SIGSTOP to a group that no scan shows and \* judges it again @@ -150,6 +153,10 @@ CONSTANTS Unseen, \* the environment: no scan of /proc shows a \* live process of the program, as for a fork \* chain whose processes each live about 2 ms + FreezeMisses, \* the environment: with Unseen, no freeze of + \* stopProgramGroup brings a member into view, + \* as when a SIGCONT from another process comes + \* before each judgement ZombiesInView, \* the environment: with Unseen, the scans show \* zombies of the program's group, as under a \* PID 1 that never reaps @@ -173,6 +180,7 @@ CONSTANTS ASSUME MaxListReconciles \in 1..3 ASSUME Token \in BOOLEAN ASSUME Unseen \in BOOLEAN +ASSUME FreezeMisses \in BOOLEAN ASSUME ZombiesInView \in BOOLEAN ASSUME OtherPidSpace \in BOOLEAN ASSUME Win32 \in BOOLEAN @@ -197,7 +205,8 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, GcKeepsLiveGroup, ReconcileRepairsDestroyed, ReconcileRepairsMarked, TokenNamesProgram, ReusedIdReadsGone, ProvesHostPid, CreateRecordsHost, - FreezesUnseenGroup, UnsharedGroupReadsUnknown} : b \in BOOLEAN + FreezesUnseenGroup, WaitProbesUnseenGroup, + UnsharedGroupReadsUnknown} : b \in BOOLEAN Readers == {"gc", "list"} \* the two processes that run reconcileSession \* The group that a kill went through, and that the wait after it probes: @@ -394,7 +403,8 @@ NoKill == UNCHANGED <> ProvenKill == IF ~TokenNamesProgram THEN NoKill ELSE IF ProvesGroupOwnership /\ reused THEN NoKill - ELSE IF Unseen /\ ~FreezesUnseenGroup /\ ~reused /\ ~foreign THEN NoKill + ELSE IF Unseen /\ (~FreezesUnseenGroup \/ FreezeMisses) /\ ~reused + /\ ~foreign THEN NoKill ELSE KillsGroupId \* Without a token, readProgramGroup falls back to the childPid of the @@ -426,8 +436,14 @@ GroupAlive == prog \/ foreign \* isProcessGroupAlive probes kill(-pgid, 0): every process with that group \* id reads alive, also one of an unrelated group that took it. EPERM, when \* every process left belongs to another user, reads alive only with -\* ProbeCountsDeniedGroup. -ProbeSees == prog \/ left \/ reused \/ (ProbeCountsDeniedGroup /\ foreign) +\* ProbeCountsDeniedGroup. When the probe finds the group, the scans after it +\* decide: with Unseen they show no process of the program, and with +\* WaitProbesUnseenGroup a second probe that still finds the group reads it +\* alive. Scans that show only zombies read the group ended either way. +ProbeFindsUnseen == WaitProbesUnseenGroup /\ ~ZombiesInView +ProbeSees == + \/ (prog \/ left) /\ (~Unseen \/ ProbeFindsUnseen) + \/ reused \/ (ProbeCountsDeniedGroup /\ foreign) \* isProgramGroupAlive in waitForProcessesToExit, for the group that the \* kill before it went through. With a token it reads the group alive while @@ -441,9 +457,11 @@ ProbeSees == prog \/ left \/ reused \/ (ProbeCountsDeniedGroup /\ foreign) \* TokenNamesProgram no member carries the recorded autogroup, so the group \* reads gone. Without ReusedIdReadsGone a group that took the id reads \* alive, because its members carry another autogroup. With Unseen the scans -\* show no process of the program, and the probe after them reads the -\* group gone, since the wait does not freeze it. -GroupSeen(kind) == +\* show no process of the program, so the group reads gone, and the probe +\* after them decides (ProbeFindsUnseen). GroupJudged leaves out that probe +\* of a group with a token: gc judges such a group with its own probe +\* (GcSeesGroup). +GroupJudged(kind) == /\ KillsProgramGroup /\ \/ kind = "proven" /\ TokenNamesProgram /\ (((prog \/ left) /\ ~Unseen) \/ foreign) @@ -451,6 +469,11 @@ GroupSeen(kind) == \/ kind = "bare" /\ ProbeSees \/ kind = "numeric" /\ FallbackReaches /\ ProbeSees +GroupSeen(kind) == + \/ GroupJudged(kind) + \/ /\ KillsProgramGroup /\ kind = "proven" + /\ Unseen /\ ProbeFindsUnseen /\ (prog \/ left) + \* The group as destroy and reconcile see it. With OtherPidSpace no scan and \* no probe of theirs shows the program's processes: a group with a token \* reads gone, and gets no kill, because no member is in view. @@ -1240,7 +1263,7 @@ GcReadsReconciled == \* often. GcSeesGroup == /\ ~OtherPidSpace /\ ~Refused - /\ \/ GroupSeen("proven") + /\ \/ GroupJudged("proven") \/ /\ GcProbesUnseenGroup /\ Unseen /\ (prog \/ left) /\ (~ZombiesInView \/ GcFreezesUnseenGroup) diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index c09d2607..48988076 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/check.sh +++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh @@ -166,7 +166,7 @@ TERMINAL=$(node -e ' const c = JSON.parse(require("node:fs").readFileSync(process.argv[1], "utf8")).constants; console.log("{" + c.Terminal.map((s) => JSON.stringify(s)).join(", ") + "}"); ' "$OUT/facts.json") -GUARDS="GcSkipsNonCollectable GcFinalCheck GcKeepsLiveGroup GcProbesUnseenGroup GcFreezesUnseenGroup ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed ReconcileRepairsMarked CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid CreateRecordsHost FreezesUnseenGroup UnsharedGroupReadsUnknown HostChecksCreateFailed HostPollsCreateFailed CreateRetriesMarker ForceSkipsUnreadableGroup" +GUARDS="GcSkipsNonCollectable GcFinalCheck GcKeepsLiveGroup GcProbesUnseenGroup GcFreezesUnseenGroup ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed ReconcileRepairsMarked CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid CreateRecordsHost FreezesUnseenGroup UnsharedGroupReadsUnknown HostChecksCreateFailed HostPollsCreateFailed CreateRetriesMarker ForceSkipsUnreadableGroup WaitProbesUnseenGroup" # One "Guard=TRUE|FALSE" word per guard, read from the code by facts.mjs. FACTS_LINE=$(node -e ' const c = JSON.parse(require("node:fs").readFileSync(process.argv[1], "utf8")).constants; @@ -195,6 +195,10 @@ UNSEEN=FALSE # ZOMBIES: whether, with UNSEEN, the scans show zombies of the program's # group, as under a PID 1 that never reaps. ZOMBIES=FALSE +# MISSES: whether, with UNSEEN, no freeze of stopProgramGroup brings a +# member into view, as when a SIGCONT from another process comes before +# each judgement. +MISSES=FALSE # OTHER: whether destroy, list and gc run in another pid space than the host. OTHER=FALSE # WIN32: whether SIGTERM ends the host at once, as on Windows. @@ -224,6 +228,7 @@ write_run() { done echo " Token = $TOKEN" echo " Unseen = $UNSEEN" + echo " FreezeMisses = $MISSES" echo " ZombiesInView = $ZOMBIES" echo " OtherPidSpace = $OTHER" echo " Win32 = $WIN32" @@ -283,13 +288,20 @@ write_run mutant-ShutdownBothChecks violated TerminalIsFinal "ShutdownChecksComm # group is frozen. UNSEEN=TRUE write_run current-unseen pass "$RULES" "" "the code with a program that no scan shows: every rule holds" -write_run mutant-FreezesUnseenGroup-unseen violated DestroyedProgramStopped "FreezesUnseenGroup=FALSE" "without the freeze, the kill finds no member in view, and destroy records destroyed while a fork chain runs" DestroyedProgramStopped +# The wait probes the group that no scan shows, so the freeze and the probe +# each keep destroy from recording destroyed while the chain runs. +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. ZOMBIES=TRUE 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. +MISSES=TRUE +write_run current-unseen-misses pass "$RULES" "" "the code with a fork chain that every freeze misses: every rule holds" +write_run mutant-WaitProbesUnseenGroup-unseen-misses violated DestroyedProgramStopped "WaitProbesUnseenGroup=FALSE" "without the probe, the wait after a missed freeze reads the chain ended, and destroy records destroyed while it runs" DestroyedProgramStopped +MISSES=FALSE UNSEEN=FALSE # destroy, list and gc run without /proc, or in another pid namespace or on diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index ea63f4b3..2b3a5e1a 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -1273,14 +1273,33 @@ function ownershipFacts() { signalParam === "signal: 'SIGSTOP' | 'SIGCONT'" && !stray, FreezesUnseenGroup: freezeFacts(stop.body), + WaitProbesUnseenGroup: waitProbeFacts(), }; } +// isProcessGroupAlive, which every wait reads through isProgramGroupAlive, +// probes the group again when its probe found the group but no scan showed +// a member, live or zombie, and reads the group alive while that probe finds +// it. Without the second probe it reads such a group ended. +function waitProbeFacts() { + const module = 'src/host/programGroup.ts'; + const alive = requireDeclaration(module, 'isProcessGroupAlive').body + .statements; + return ( + normalize(alive.at(-1)?.getText() ?? '') === + 'return groupHasLiveProcess(pgid) ?? probeFindsGroup(pgid);' && + normalize(requireDeclaration(module, 'probeFindsGroup').body.getText()) === + "{ try { process.kill(processGroupTarget(pgid), 0); return true; } catch (error) { if (hasErrorCode(error, 'ESRCH')) { return false; } if (hasErrorCode(error, 'EPERM')) { return true; } throw error; } }" + ); +} + // In stopProgramGroup's loop, each judgement that gets no kill and is not // unproven sends SIGSTOP to the group and judges again: gone, unknown, and // owned with a witness that ended before its read. So a member that a scan // never shows, or that ends between two reads, stops and stays in view, -// while /proc names this process by its pid. The finally block sends a +// while /proc names this process by its pid. Before the first freeze, a +// group that shows a stopped member gets none, so the SIGCONT cannot resume +// a member that job control stopped. The finally block sends a // frozen group that got no kill SIGCONT, also when a scan throws. function freezeFacts(body) { const guarded = body.statements.find(ts.isTryStatement); @@ -1300,13 +1319,14 @@ function freezeFacts(body) { before.at(-2) === 'let frozen = false;' && before.at(-1) === 'let killed = false;' && guarded.tryBlock.statements.length === 1 && - st.length === 7 && + st.length === 8 && st[1] === "if ( judgement.verdict === 'unproven' || (judgement.verdict === 'unknown' && !judgement.running) ) { return; }" && st[2].startsWith("if (judgement.verdict === 'owned') {") && st.slice(3).join('\n') === [ 'if (!procShowsOwnPidSpace()) { return; }', + 'if (!frozen && showsStoppedMember(group.pid)) { return; }', "frozen = signalProcessGroup(group.pid, 'SIGSTOP') || frozen;", 'if (!frozen) { return; }', 'Atomics.wait(settleCell, 0, 0, STOP_SETTLE_MS);', @@ -1558,7 +1578,10 @@ function frozenJudgesTwice() { judged.catchClause === undefined && judged.finallyBlock !== undefined && statementsOf(judged.tryBlock).join('\n') === - 'verdict = judgeLiveGroup(group).verdict;' && + [ + 'Atomics.wait(settleCell, 0, 0, STOP_SETTLE_MS);', + 'verdict = judgeLiveGroup(group).verdict;', + ].join('\n') && statementsOf(judged.finallyBlock).join('\n') === "signalProcessGroup(group.pid, 'SIGCONT');" && normalize(decides?.getText() ?? '') === diff --git a/docs/USAGE.md b/docs/USAGE.md index 47d48962..f8b2bf3d 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -314,7 +314,7 @@ agent-tty record diff --at-seq-a 0 --json `destroy` ends the session's program and every process that the program left in its process group, then records the session as `destroyed`. On Linux it also ends those processes when the program has already exited or the session has failed. -A group whose processes each fork their successor and end too fast for any scan of `/proc` to show or read one, a fork chain, gets SIGSTOP first. Its stopped processes stay in view, so `destroy` can prove the group and kill it. A frozen group that agent-tty cannot prove is the session's gets SIGCONT. +A group whose processes each fork their successor and end too fast for any scan of `/proc` to show or read one, a fork chain, gets SIGSTOP first. Its stopped processes stay in view, so `destroy` can prove the group and kill it. A frozen group that agent-tty cannot prove is the session's gets SIGCONT. When the freeze misses a fork chain, as when another process resumes it before each check, the wait still finds the group id, and `destroy` fails with `HOST_TIMEOUT` instead of recording the session as `destroyed`. Under a PID 1 that never reaps, a group whose scans show only zombies reads ended, so there such a missed chain can outlive a `destroy` that reports success. `destroy --force` kills the host and the program's group without asking the host first. When a read of the program's group fails with an error that every later read repeats, such as `program.json` that refuses the read (EACCES) or a `/proc` scan that fails (EIO), `gc` keeps the session and reports "failed to check the session's program group (destroy --force removes it)", or "failed to reconcile session (destroy --force removes it)" for a session whose host died. Those errors are EACCES, EPERM, EIO, EISDIR, ENOTDIR, ELOOP and ENAMETOOLONG. A plain `destroy` fails on the same read. When the read of `program.json` or the first check of the group fails that way twice, 100 ms apart, `destroy --force` stops the host alone, without the group, and records the session as `destroyed` once the host has ended, so the next `gc` removes it. A process that the program left can outlive such a `destroy --force`. When the second read passes, `destroy --force` stops the group as usual. A read that fails after that first check, a group that reads alive, or a host that does not end (`HOST_TIMEOUT`) still fails it. Other errors, such as EMFILE, ENOMEM or EAGAIN, can pass, so `gc` gives no such hint and `destroy --force` fails on them too. A `host.json` that cannot be read counts as missing, so the group reads as out of view, as in another pid namespace: `destroy --force` fails with `HOST_TIMEOUT`, and its message names `host.json` and the error. When the read was refused (EACCES or EPERM), make that file readable and run `destroy` again. Until then, `gc` removes such a session once it has ended, but a session whose host died while it ran stays `running`, because its group reads alive. `list`, `inspect`, `destroy` and `gc` reconcile a session whose host died: they kill the program's group and record the session as `failed` (or `exited` or `destroyed`). @@ -367,7 +367,7 @@ 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. -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. `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. +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. 6. Two cases where agent-tty cannot run the check end differently from a session that stays running: diff --git a/src/host/README.md b/src/host/README.md index 1f5ef85f..b8181e4a 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -26,7 +26,7 @@ - `reconcileSession(sessionDirectory)` moves a non-terminal session to a terminal status when its host process is gone. [lifecycle.ts:reconcileSession] - `captureProgram(pid)` returns a `ProgramRecord` (`version`, `pid`, `bootId`, `autogroup`) for the program that the host just spawned, and `writeProgramRecord(sessionDirectory, record)` writes it to `program.json`. `bootId` is a string and `autogroup` a number, or both are `null`. [programGroup.ts:captureProgram] [programGroup.ts:writeProgramRecord] - `readProvenProgramGroup(sessionDirectory)` returns the `program.json` record when it has a token and `sharesHostPids` reads true, the unshared group (below) when it has a token and `sharesHostPids` reads false, else `null`. `readProgramGroup(sessionDirectory, childPid)` returns the same for a record with a token, else `{ childPid, sessionDirectory }`, or `null` when `childPid` is `null` or, on Linux, when `host.json` names another pid namespace or machine id than the CLI's (`sharesHostPids`). For a record with a token where `sharesHostPids` reads false, which includes a missing `host.json`, a CLI that cannot read `/proc/self/ns/pid` and a CLI whose `/proc/self` does not name its own pid, both return the unshared group `{ unshared: true }`: no scan or probe of this process shows the program's processes, so `isProgramGroupAlive` reads it alive and `stopProgramGroup` sends it nothing. A `program.json` that does not validate reads as `null` in both, so it gets no kill and no throw. [programGroup.ts:readProgramRecord] [programGroup.ts:readProvenProgramGroup] [programGroup.ts:readProgramGroup] [hostRecord.ts:sharesHostPids] -- `stopProgramGroup(group)` SIGKILLs the group when the record proves it. A group that no scan shows gets SIGSTOP and another judgement, at each of up to 5 judgements while `/proc/self` names this process's pid, and SIGCONT when it gets no kill. `isProgramGroupAlive(group)` reports whether the group still holds a process that the kill would target. `judgeProgramGroup(record, bootId, rows)` is the pure decision: `owned`, `gone`, `unproven` or `unknown`. `parseProcStat` and `parseAutogroup` parse `/proc//stat` and `/proc//autogroup`. `parseAutogroup` returns `null` for text that names no autogroup, and a member whose autogroup file cannot be read or parsed carries no token. [programGroup.ts:stopProgramGroup] [programGroup.ts:isProgramGroupAlive] [programGroup.ts:judgeProgramGroup] [programGroup.ts:parseProcStat] +- `stopProgramGroup(group)` SIGKILLs the group when the record proves it. A group that no scan shows, or whose member ends between two reads (its stat and its autogroup, or the witness and its re-read), gets SIGSTOP and another judgement, at each of up to 5 judgements while `/proc/self` names this process's pid, and SIGCONT when it gets no kill. A group that shows a member that job control or a tracer stopped gets no SIGSTOP before its first freeze, so the SIGCONT cannot resume that member. Each SIGSTOP is followed by a synchronous wait of `STOP_SETTLE_MS` (1 ms), because the stop takes effect only when the kernel next runs a member. `isProgramGroupAlive(group)` reports whether the group still holds a process that the kill would target. When its probe `kill(-pgid, 0)` finds the group but no scan shows a member, live or zombie, `isProcessGroupAlive` probes again: a group whose processes were reaped meanwhile reads ended, and one that still holds the id, such as a fork chain that a freeze missed, reads alive. Scans that show only zombies read the group ended. `judgeProgramGroup(record, bootId, rows)` is the pure decision: `owned`, `gone`, `unproven` or `unknown`. `parseProcStat` and `parseAutogroup` parse `/proc//stat` and `/proc//autogroup`. `parseAutogroup` returns `null` for text that names no autogroup, and a member whose autogroup file cannot be read or parsed carries no token. [programGroup.ts:stopProgramGroup] [programGroup.ts:isProgramGroupAlive] [programGroup.ts:judgeProgramGroup] [programGroup.ts:parseProcStat] - `captureHost(pid)` returns a `HostRecord` (`version`, `pid`, `bootId`, `startTicks`, `pidNamespace`, `timeNamespace`, `machineId`) on Linux when `/proc` shows the process and the boot id, else `null`. `machineId` is the first of `/etc/machine-id` and `/var/lib/dbus/machine-id` that holds 32 hex characters, else `null`. A record without `timeNamespace` and `machineId`, which a build between #260 and #267 wrote, still reads, and only the checks of those two fields are skipped. `writeHostRecord(sessionDirectory, record)` writes it as `host.json`, and `readHostRecord(sessionDirectory)` returns it, or `null` when it is missing or unreadable. `hostRecordError(sessionDirectory)` returns the error when the file exists but its read or its check fails, else `null`, so that the `HOST_TIMEOUT` of `destroySession` for an unshared group names `host.json` and that error instead of another pid namespace, and says to make the file readable only for EACCES or EPERM. `judgeHost(pid, record)` returns `dead` only when no process has the pid, a zombie has it, or the record names another boot id or start time, `alive` when both match, and `unknown` otherwise: also off Linux for a pid that exists, for a CLI in another pid namespace or on another machine than the record names, and, instead of a start time mismatch, for a CLI in another time namespace. [hostRecord.ts:captureHost] [hostRecord.ts:writeHostRecord] [hostRecord.ts:readHostRecord] [hostRecord.ts:hostRecordError] [hostRecord.ts:judgeHost] - `SessionState` holds the host's in-memory `SessionRecord` (type from `src/protocol/schemas.ts`). Methods: `snapshot`, `setChildPid`, `setDimensions`, `setFailureOrigin`, `requestDestroy`, `recordDestroyed` and `recordExit`. [sessionState.ts:SessionState] - `createSerialManifestWriter(path, snapshot, write?)` returns a function that writes `snapshot()` to `path`. The default `write` is `writeManifest` (`src/storage/manifests.ts`). `runHost` sends every manifest write through one such function. [manifestWriter.ts:createSerialManifestWriter] [hostMain.ts:runHost] diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index d2692173..4e55c9ad 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -442,6 +442,14 @@ function readProcessRow(pid: number): ProcessRow | null { return stat === null ? null : toProcessRow(stat); } +// Whether a scan shows a member of the group that job control or a tracer +// stopped. +function showsStoppedMember(pgid: number): boolean { + return readGroupMembers(pgid).some( + (row) => row.state === 'T' || row.state === 't', + ); +} + function readGroupMembers(pgid: number): ProcessRow[] { let entries: string[]; try { @@ -586,8 +594,11 @@ function isProcessGroupAlive(pgid: number): boolean { throw error; } - // None in view: the kill found processes that were reaped before the scan. - return groupHasLiveProcess(pgid) ?? false; + // None in view: the kill found processes that were reaped before the scan, + // or members of a fork chain that end before a scan reads them. A second + // probe tells them apart: reaped processes are gone, a fork chain still + // holds the id. Scans that show only zombies read the group ended. + return groupHasLiveProcess(pgid) ?? probeFindsGroup(pgid); } function killProcessGroupBestEffort(pgid: number): void { @@ -729,6 +740,8 @@ function judgeFrozenGroup(group: ProvenRecord): boolean | null { } let verdict: GroupJudgement['verdict']; try { + // The SIGSTOP takes effect only when the kernel next runs a member. + Atomics.wait(settleCell, 0, 0, STOP_SETTLE_MS); verdict = judgeLiveGroup(group).verdict; } finally { signalProcessGroup(group.pid, 'SIGCONT'); @@ -774,15 +787,17 @@ export function stopProgramGroup(group: ProgramGroup | null): void { } // A member that forks its successor and ends between scans is never in - // view. One that a scan shows can also end before its autogroup read - // (unknown, running) or before the witness is read again. SIGSTOP freezes - // the group, also a child that a member forks while the kernel delivers - // it, and a stopped member stays in view and cannot end, so a judgement - // that gets no kill and is neither unproven nor an unknown without a - // running member sends SIGSTOP and judges the frozen group again. A group - // that job control stopped, whose autogroup /proc refuses, gets no signal. Each such judgement sends SIGSTOP again, for a member that a + // view. One that a scan shows can also end between two reads: before its + // autogroup read (unknown, running) or before the witness is read again. + // SIGSTOP freezes the group, also a child that a member forks while the + // kernel delivers it, and a stopped member stays in view and cannot end, + // so a judgement that gets no kill and is neither unproven nor an unknown + // without a running member sends SIGSTOP and judges the frozen group + // again. Each such judgement sends SIGSTOP again, for a member that a // SIGCONT from elsewhere resumed. A frozen group that gets no kill gets - // SIGCONT, also when a scan throws. + // SIGCONT, also when a scan throws. So a group that shows a member that + // job control stopped before the first freeze gets no SIGSTOP: the + // SIGCONT would resume that member. let frozen = false; let killed = false; try { @@ -811,6 +826,9 @@ export function stopProgramGroup(group: ProgramGroup | null): void { if (!procShowsOwnPidSpace()) { return; } + if (!frozen && showsStoppedMember(group.pid)) { + return; + } frozen = signalProcessGroup(group.pid, 'SIGSTOP') || frozen; if (!frozen) { return; diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index 8373042a..9a1b242d 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -704,10 +704,12 @@ describe('a program group without a token', () => { expect(isProgramGroupAlive(group)).toBe(true); }); + // ['ok', []]: no scan shows a member while the probes find the id, as for + // a fork chain whose members end before a scan reads them. it.each([ ['ok', ['Z', 'X'], false], ['ok', ['Z', 'S'], true], - ['ok', [], false], + ['ok', [], true], ['EPERM', ['Z'], false], ['EPERM', ['R'], true], ['EPERM', [], true], @@ -722,6 +724,24 @@ describe('a program group without a token', () => { }, ); + // The probe can find processes that are reaped before the scans. The + // probe after the scans then finds none. + it('on linux, reads a group ended when no scan shows a member and the second probe finds none', () => { + Object.defineProperty(process, 'platform', { value: 'linux' }); + procShowsGroup(); + let probes = 0; + vi.spyOn(process, 'kill').mockImplementation(() => { + probes += 1; + if (probes > 1) { + throw errno('ESRCH'); + } + return true; + }); + + expect(isProgramGroupAlive(group)).toBe(false); + expect(probes).toBe(2); + }); + // A process whose main thread called pthread_exit shows Z while another // of its threads runs. it.each([ @@ -1444,6 +1464,23 @@ describe('a program group with a token, as a faked /proc shows it', () => { expect(kill).not.toHaveBeenCalled(); }); + // A member that job control stopped would resume at the SIGCONT after a + // freeze, so a group that shows one gets no SIGSTOP before its first + // freeze, also beside a running member without an autogroup. + it('sends no signal to a group with a stopped member and a running member that shows no autogroup', () => { + procShowsTokenGroup('T', 'S'); + const tokenRead = autogroupFile.read; + autogroupFile.read = (file) => + file === '/proc/100/autogroup' || file === '/proc/101/autogroup' + ? '' + : (tokenRead?.(file) ?? null); + const kill = vi.spyOn(process, 'kill').mockReturnValue(true); + + stopProgramGroup(group); + + expect(kill).not.toHaveBeenCalled(); + }); + // The witness of a judgement can end before it is read again. it('freezes a group whose witness ends before it is read again, and kills it once a stopped member carries the token', () => { procShowsTokenGroup('S'); @@ -1454,8 +1491,9 @@ describe('a program group with a token, as a faked /proc shows it', () => { if (pid !== '100') { return live.get(pid); } - // Each judgement reads the member once, and the read of the witness - // after it finds the member ended. + // The judgement reads the member, the read of the witness after it + // finds the member ended, and the scan for a stopped member before + // the freeze reads it running. reads += 1; return reads % 2 === 0 ? errno('ENOENT') : live.get(pid); } @@ -1464,7 +1502,7 @@ describe('a program group with a token, as a faked /proc shows it', () => { stopProgramGroup(group); - expect(reads).toBe(2); + expect(reads).toBe(3); expect(kill.mock.calls).toEqual([ [-CHILD_PID, 'SIGSTOP'], [-CHILD_PID, 'SIGKILL'], @@ -1702,6 +1740,16 @@ describe('a program group with a token, as a faked /proc shows it', () => { expect(isProgramGroupAlive(group)).toBe(false); }); + // A fork chain whose members end before a scan reads them: a freeze that + // misses it, as after a SIGCONT from elsewhere, leaves the wait to the + // probe, which still finds the id. + it('is alive while no scan shows a member and the probe finds the id', () => { + procShowsTokenGroup(); + probeEnds('ok'); + + expect(isProgramGroupAlive(group)).toBe(true); + }); + it('is not alive when /proc hides other users and the probe finds no process', () => { procShowsTokenGroup(); procHooks.mountinfo = procMount('rw,hidepid=2');