Repository navigation
Conversation
gc deleted program.json with the folder of an exited session while a process that the program left still ran, so nothing could prove or stop that process later. gc now skips such a session until destroy ends the group. The lifecycle model gets the GcKeepsLiveGroup guard, rule R20 RemovedSessionStopped and the mutant run that breaks it. check.sh gains --drift-only and a job pool.
The lifecycle-model job runs check.sh --drift-only on every run, and the whole check when coverage.json differs from the base. coverage.json syncs the model with gc's group check.
|
@codex security review |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
|
@codex review |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 9a3716504b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Codex on #302: gc sends no SIGSTOP, so a fork chain that the program left read gone and gc removed program.json while it ran. A group id that kill(-pgid, 0) finds while no scan shows a member, live or zombie, now keeps the session. The model gets GcProbesUnseenGroup, R20 covers the Unseen runs, and mutant-GcProbesUnseenGroup-unseen must violate it.
# Conflicts: # .agents/skills/verify-session-lifecycle/SKILL.md # .agents/skills/verify-session-lifecycle/coverage.json # .agents/skills/verify-session-lifecycle/scripts/check.sh
|
@codex review |
|
@codex security review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8b4deb2d0d
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
…eps a group it cannot check Codex on #302: an exited session whose group reads unknown stays after gc, and USAGE said gc could remove it.
One job of 4 vCPUs took 63 min for the 73 TLC runs. check.sh gains CHECK_SHARD=<i>/<n>, which takes every n-th run that expects pass and every n-th of the rest, and the lifecycle-model job runs four shares.
coverage.json now records the facts (every guard and status set) that facts.mjs read at the sync, and check.sh --drift-only compares them. The facts come from the source text with its comments while the hashes leave comments out, so one new comment in reconcileSession's repair block turned ReconcileRepairsDestroyed FALSE and the drift check still passed.
# Conflicts: # .agents/skills/verify-session-lifecycle/SKILL.md # .agents/skills/verify-session-lifecycle/coverage.json # .agents/skills/verify-session-lifecycle/scripts/check.sh # docs/USAGE.md # test/integration/lifecycle.test.ts
…in merge check.sh --update-coverage at c9dd5be gave 74/74 runs as expected. The record now holds the facts. current has 26,798,236 distinct states and current-no-token 26,648,756.
|
@codex review |
|
@codex security review |
|
Codex Review: Didn't find any major issues. What shall we delve into next? Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
# Conflicts: # .agents/skills/verify-session-lifecycle/SKILL.md # .agents/skills/verify-session-lifecycle/coverage.json # .agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla # .agents/skills/verify-session-lifecycle/scripts/check.sh
A group that gc cannot check proved nothing but kept its session forever. After a container restart that keeps the home, host.json names a pid namespace that no longer exists, the group reads unshared, and no destroy can prove it gone. provenProgramGroupRuns now counts only a live member that carries the token, or the probe of a fork chain that no scan shows. In another pid space, or behind a refused read of /proc, gc removes the session as main did. The model reads the group not proven in another pid space, R20 covers a gc in the host's pid space, and witness-WitnessUnsharedGcRemovesLeftover-otherspace shows the trade-off. The gc integration tests now let the program exit only once program.json is in place, and skip when the host captured no token: /bin/sh could exit before the capture under load. A unit test covers the gc skip when the group check throws. SKILL.md gives the measured time of a whole run.
GcRemoves clears rec in the same step, so the witness asks for the state that R20 leaves out instead: a gc in another pid space removed the session while a process that the program left runs.
|
@codex review |
|
@codex security review |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: dcbf0c8e91
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
CI at dcbf0c8: gc removed a session whose fork chain ran. A member can end between its stat and its autogroup read (unknown), or show up only after the judge's scans, and both now read false. judgeGroupForGc reads them as inconclusive, and provenProgramGroupRuns judges again, at most ten times. A judgement that stays inconclusive, as behind a refused read of /proc, still proves nothing, so gc removes that session.
check.sh --update-coverage at dcbf0c8 gave 78/78 runs as expected in 3,304 s. The model and check.sh are unchanged since, and facts.mjs reads the same values, so this record comes from facts.mjs at this commit. current has 29,309,460 distinct states and current-no-token 29,186,546.
|
@codex review |
|
@codex security review |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a31fe8973c
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Codex on #302: GC_JUDGEMENTS = 0 would skip every judgement, so gc would keep no session, and no fact or hash changed. facts.mjs now reads GcKeepsLiveGroup FALSE unless the limit is a positive integer literal, and coverage.json hashes the declaration. The model, check.sh and every fact value are unchanged since the 78/78 check at dcbf0c8.
|
@codex review |
|
@codex security review |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f263f56d6e
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Why
gcdeleted the folder of an exited session while a process that the program left still ran. The folder holdsprogram.json, the only record that proves that process is the session's, so aftergcnodestroycould find or stop it. The lifecycle model (scripts/check.shof theverify-session-lifecycleskill) also never ran in CI, so a change to the covered code could merge with a model that no longer describes it.Follow-up of #291 (verifier note N3) and #283. Refs #203.
What changes for users
gckeeps a session that is notdestroyedwhile itsprogram.jsonautogroup record proves that a process of the program's group runs. It reportsthe session's program group still runs (destroy ends it)inskippedSessions, also with--dry-run. A failed check skips the session too.gcalso keeps it whilekill(-pgid, 0)finds the group id and no scan of/procshows a member, live or zombie, such as a fast fork chain.gcsends no SIGSTOP, so without this probe such a chain read as gone.gckeeps a session only while it proves the group, so thatdestroycan end it. When it cannot check the group, it removes the session as main does: in another pid namespace than the one thathost.jsonnames (for example after a container restart that keeps the agent-tty home), and when/procrefuses the boot id or a member's autogroup, or hides other users' processes. Else such a session would stay forever, because nodestroycan prove its group gone.destroythen ends the leftover, and the nextgcremoves the session.No JSON shape changes:
skippedSessions[].reasonis an existing free-text field.docs/USAGE.mdalso adds one case to the CLIs that cannot prove they share the host's pid space: a CLI whose/procbelongs to another pid namespace (/proc/selfnames another pid than its own). It counts the host as running, so itsdestroy --forcecan fail withHOST_TIMEOUT(verifier follow-up of #303).What changes for maintainers
GcKeepsLiveGroupandGcProbesUnseenGroup, the gc stepGcChecksGroup, rule R20RemovedSessionStopped, and the runsmutant-GcKeepsLiveGroup,mutant-GcProbesUnseenGroup-unseenandwitness-WitnessUnsharedGcRemovesLeftover-otherspace. R20 covers a gc in the host's pid space. In another pid space gc reads the group not proven, and the witness shows that such a gc removes an exited session while a leftover runs. With fix(host): record the host at create, read a token without host.json as unshared, freeze again #303 and fix(host): a create that gives up leaves a create-failed marker, and its host stops on it #312 that makes 78 runs and thirty-five guards.facts.mjsreads the new guards fromgcSessions,defaultDependencies,provenProgramGroupRuns,judgeGroupForGcandprobeFindsGroup.check.shgains--drift-only. It compares the facts and the covered code withcoverage.jsonand needs no Java.coverage.jsonnow also records the facts: the value of each guard and the two status sets.--drift-onlyprintsfact <name> changed: was true, now falsewhen one differs. Before, the facts were not recorded. The facts come from the source text with its comments, but the hashes leave comments out. So one new comment inside a guarded block turned a guard FALSE, every hash stayed the same, and the drift check passed (details below).check.shnow starts a new TLC run as soon as one ends (wait -n). Before, each batch ofCHECK_JOBSruns waited for its slowest run. Bash 3.2 on macOS keeps the batch behavior.check.shgainsCHECK_SHARD=<i>/<n>. It takes every n-th run that expects pass and every n-th of the rest.lifecycle-modeljob (four shares), which the Linuxquality-gatesjob needs. Share 1 callscheck.sh --drift-only. The TLC runs start only whencoverage.jsondiffers from the base of the pull request, the merge group or the pushed commit. Each change to the model, its scripts, the covered code or a fact needs such a sync.facts.mjssay thatRecordsProgramSyncalso guards "a token only besidehost.json", and that the model leaves out a host whose capture fails (verifier follow-up of fix(host): record the host at create, read a token without host.json as unshared, freeze again #303). The model has no rule that such a token breaks, so I added no guard.The guard-value drift gap
At b0c2b8d I added one comment line in the repair block of
reconcileSession:existsSync(destroyMarkerPath(sessionDirectory)) ) { + // The destroy marker outranks the status that this reconcile read. await writeManifest(manifestFile, {facts.jsonReconcileRepairsDestroyed=falseReconcileRepairsDestroyed=falsecheck.sh --drift-onlyCovered code matches the sync record., exit 0STALE…fact ReconcileRepairsDestroyed changed: was true, now false, exit 3Exit 3 fails the drift step of every
lifecycle-modelshare. A newcoverage.jsonwith the FALSE fact differs from the base, so CI then runs TLC, and thecurrentrun fails.Known limit (open review thread)
Under a non-reaping PID 1, a fast fork chain can show only zombies to gc's scans while a live successor escapes both scans. gc then reads the group as stopped and removes the session. b4e1b83 behaved the same, and main removes every such session. Only a freeze (SIGSTOP) would show the successor, and gc sends no signals. The maintainer decides whether a follow-up adds that.
Validation
faa14b11adds the unit testkeeps a terminal session whose proven program group still runsand the integration testgc keeps an exited session while a process that the program left runs. Both fail on main (removedSessionCount: 1).check.sh --update-coveragewithCHECK_JOBS=26at dcbf0c8 (after the merge of main at 6a052fc): 78/78 runs as expected in 3,304 s.currenthas 29,309,460 distinct states andcurrent-no-tokenhas 29,186,546. The later commits change no model input and no fact value, so a31fe89 and f263f56 write the record fromfacts.mjsat their heads. CI runs TLC on it again.lifecycle-modelshares took 18.8, 10.4, 12.3 and 14.8 min of TLC, and 20 + 19 + 19 + 20 = 78 runs gave the expected results. At dcbf0c8, before the record sync, share 1 failed withSTALEas designed. Before the main merges, one job took 63 min 14 s for 73 runs (dispatch run 41737109486).provenProgramGroupRuns. Each one flipsGcKeepsLiveGroupto FALSE.gc removes an exited session whose host.json names another pid namespaceand three unit cases (unshared, no autogroup, hidepid) fail on b4e1b83. The unit testjudges again after a member that ended before its autogroup readfails on dcbf0c8. A unit test covers the gc skip when the group check throws.unknownread as running, or with an inconclusive end read as running, both gc guards read FALSE. Without the probe, onlyGcProbesUnseenGroupreads FALSE.GC_JUDGEMENTS = 0turns both FALSE, and any other value changes its recorded hash.tsc --noEmit,oxlint,oxfmt --check,mise run workflow-lintand the targeted unit tests pass./bin/shexit only onceprogram.jsonexists, and skip when it holds no token. On 4 pinned CPUs with two busy loops, both fork-chain tests passed 8 of 8 runs at a31fe89's code.host.jsonpidNamespaceedited topid:[1]on an exited session whose leftover runs):gcdestroy --forceHOST_TIMEOUTAGENT_TTY_HOME, main vs this branch (sh -c 'trap "" HUP; sleep 300 & exit 0'):gcof the exited sessiondestroySESSION_NOT_FOUND, leftover runsgcGenerated with
xum• Model:anthropic:claude-opus-5-5• Thinking:xhigh