diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 02592af5..4841428e 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 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. +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 one job per share. The job's matrix in `.github/workflows/ci.yml` sets `CHECK_SHARD=/` and `CHECK_JOBS`. Each job runs every n-th run that expects pass and every n-th 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. Each job prints its runs on the line `Share / of the runs:`, and its log shows how long the share took. ## 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. 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). +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. Before TLC starts, the check prints the count of runs and of the runs that expect pass on its `Runs:` line. The runs that expect pass explore the whole model and take most of the time, so `CHECK_JOBS` set to that run count 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. +1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the guards that the rules depend on (the `Facts:` line of the result lists each one) 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 94 times and prints one line per run. +3. It prints the run count, runs TLC once per run, 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. @@ -86,7 +86,7 @@ At the sync commit, the expected results are: | `current-no-token`, the code as it is without a token, R1 to R14 and R17 to R19 | pass | The same for a session whose `program.json` holds no token: on macOS, on a kernel without autogroups, when the capture read none, and for a session that an older agent-tty created. Every kill then falls back to the id that a manifest or the host's own record names. R15 and R16 are what the token adds, so this run leaves them out (see Scope). | | `current-unseen`, the code as it is with a token and a program that no scan of `/proc` shows, every rule | pass | A fork chain: each process of the program forks its successor and ends between scans, so the kill through the token sees a member only once the group is frozen. | | `witness-*` without a suffix | violated | Each witness is a state that must be reachable: a `create` that gave up recorded the session destroyed, gc removes a session, a session serves, a resize lands, a clean exit is recorded, a crash is reconciled, a plain destroy completes, a SIGTERM shutdown is recorded, 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` (which ends with `HOST_TIMEOUT` and leaves the session destroying) and `destroy --force` (which ends with `HOST_TIMEOUT` too), a process that the program left meets the kill of `destroy`, an unrelated group has the program's group id when `destroy --force` kills, `destroy --force` stops a program that only `program.json` names, a program whose host died before `program.json` named it outlives `destroy`, a wait of `destroy` through `program.json` reads the group gone while an unrelated group holds its id, a reconcile writes destroyed again over the failed that it wrote, a reconcile's first read writes destroyed over a marked terminal manifest, `destroy --force` reaches its kill while a process that took the ended host's pid runs, and `destroy --force` reaches its kill while a live host has not written `host.json` yet. A witness that passes means the model can no longer reach that state, and the passing rules prove nothing. | -| `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. | +| `witness-*-no-token` | violated | Some of those states, reached 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-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. | @@ -579,7 +579,7 @@ To bring the check back in line after changes that skipped it, use `/maintain-fo ## Scope -The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 64,052,288 distinct states, and without one 63,127,914. The check prints both counts. +The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. The check prints the count of distinct states of the model with a token and without one, on its `Distinct states of current:` and `Distinct states of current-no-token:` lines. It assumes: diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index dbd155ea..814eaa86 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": "eaa2d6a36689fc17" + "skill:scripts/check.sh": "5cf0c5286124ebeb" }, "callSites": { "writeManifest": [ diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index 966582c7..681f0daf 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/check.sh +++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh @@ -401,6 +401,7 @@ PASS_WORKERS=1 if [ "$concurrent" -gt 0 ] && [ "$CPUS" -gt "$concurrent" ]; then PASS_WORKERS=$((CPUS / concurrent)) fi +echo "Runs: $(($(wc -w <<<"$RUNS"))), $passes of them expect pass." echo "CPUs: $CPUS. TLC workers of a run that expects pass: $PASS_WORKERS." run_tlc() { diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f6a8c35f..f1e1d482 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -221,13 +221,14 @@ 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 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 - # worker per run. TLC runs only when coverage.json differs from the base, - # which every change to the model, its scripts, the covered code or a fact + # covered code. Each share starts all its runs at once, so CHECK_JOBS + # must be at least the run count that check.sh prints on the share's + # "Runs:" line. check.sh lists the share's runs on its "Share / of + # the runs:" line. The runs that expect pass explore the whole model, and + # check.sh gives them the runner's CPUs as TLC workers ("CPUs:" line). So + # a share takes about as long as its longest run, and the job log shows + # how long. TLC runs only when coverage.json differs from the base, which + # every change to the model, its scripts, the covered code or a fact # needs. lifecycle-model: runs-on: ubuntu-latest