Repository navigation
Conversation
… purge facts check.sh now runs each config against the module it names and writes only that module's code facts into it. facts.go reads 14 more guards from RepoPurger, the sweeper's purge-aware branches and the purge fence checks of the PG, SQLite and S3WAL registries, and fingerprints the code the purge model covers. Change-Id: I4bb9fe727ddff38ead2f2383c006000c246ce54d Signed-off-by: Thomas Kosiewski <tk@coder.com>
RepoPurge.tla checks the repository purge against pre-delete writers, a second purger and the purge-aware sweeper: eligibility, the delete guard, tombstone-then-delete, a clean completion stamp, and that the purge and its quarantine backups finish. Change-Id: Iae4c790a846f924127585286019ec7cec32f308f Signed-off-by: Thomas Kosiewski <tk@coder.com>
…uarantine slot The timing assumptions only hold a backup's aging back, so the liveness config turns them off and keeps weak fairness. One slot keeps the run near two minutes. Change-Id: I3e1a8e3bb475dff79db3f1c8fe24a9c0b252ccaf Signed-off-by: Thomas Kosiewski <tk@coder.com>
…onfigs TLC does not name the temporal property a trace breaks, so one config per property keeps a failure readable. Change-Id: I2b89c50a2875efed0bd4d185124e1dc183b2370f Signed-off-by: Thomas Kosiewski <tk@coder.com>
…e call Breaking HealPurgesFenced also turned this fact FALSE, because the fact looked for purgeMode in healQuarantine's arguments. Change-Id: I30c1eb503320de28d6b2acaa8d4e461a182dcfd6 Signed-off-by: Thomas Kosiewski <tk@coder.com>
ReplacePacks gets the purge fence check RegisterPacks has (separate fix). The model takes the fenced fold as the target, with a FoldsFenced fact per backend that stays FALSE until that fix is in. With the fold fenced nothing registers after the fence, so the purge model drops PackSweep's timing assumptions and its two probes. TombstonesBeforeReap and FoldNeedsOldRows go: breaking either fails no property. Change-Id: I4f7cb8cfc8cb545b8e2866ebadf3c7fec9c9f5e9 Signed-off-by: Thomas Kosiewski <tk@coder.com>
A repack fold can register its consolidated pack in a repository that the purge has already fenced. These tests fail on every backend today: ReplacePacks on a fenced repository wins instead of returning ErrRepoPurged. TestReplacePacksPurgeFence runs on PostgreSQL, SQLite and S3-WAL. The refused fold must leave the pack rows, the retained rows, the quota ledger and the generation unchanged, and the unfenced control repository must still fold. TestS3WALRecoveryPurgeFence gains a ReplacePacks case, so its list of fenced row-creating methods is complete.
On PostgreSQL, a fold that reads "not fenced" while FenceRepoPurge is still open registers its pack after the fence commits. TestReplacePacksSerializesWithPurgeFence holds FenceRepoPurge's transaction open (base-ledger lock plus fence row) and requires ReplacePacks to block until it commits, then to fail with ErrRepoPurged. Today ReplacePacks takes no base-ledger lock and wins at once. Change-Id: Icb20382562f687eec0cf13d26b641ac5be42f6dd Signed-off-by: Thomas Kosiewski <tk@coder.com>
A repack fold could register its consolidated pack in a repository whose purge had already fenced it. The purge-aware sweep treats a fenced repository's unregistered blobs as permanent garbage, so it can delete the fold's uploaded pack before the fold registers it. The fold then commits a pack row that points at no bytes. The purge retires that row later, so users lose no data. But the fence did not do what its comments said, and the purge verification model had to assume extra timing to stay safe. ReplacePacks now reads the fence inside its own transaction on every backend, after the check that all old rows still exist: - PostgreSQL takes the base-ledger lock first, like RegisterPacks and CASRef, so the fence read is ordered against FenceRepoPurge. - SQLite reads the fence inside its single-writer transaction. - S3-WAL reads the manifest's purged_at in the same CAS. On a fenced repository whose old rows still exist the fold fails with ErrRepoPurged and changes nothing. A fold whose old rows the purge already retired still loses cleanly (won=false), as before. If the fence check came first, the repacker would read that case as an ambiguous error and could upload the pack again after the purge deleted it. The repacker needs no change. With the old rows present it sees the error as a rolled-back swap: local mode logs one warning, and River retries within its bounded attempts until the purge retires the rows. The comments on FenceRepoPurge, the purge phases and SweepConfig.PurgedRepoProbe, and the storage lifecycle guide now list repack folds among the writes that the fence blocks. Change-Id: I777a7a75a2df778bce0583740318aaaa0a446c02 Signed-off-by: Thomas Kosiewski <tk@coder.com>
SKILL.md describes the purge properties, the purge facts and actions, the scope of the purge model, and the scratch breaks that make each property fail, including the ReplacePacks race the fence check closes. Change-Id: I3a5aef9292d12fa2ce20c8cc5300b5a8db5f0c20 Signed-off-by: Thomas Kosiewski <tk@coder.com>
…d-row delete The ReplacePacks fix reads the fence after its delete precondition, in the same transaction, so the ErrRepoPurged return rolls the delete back. The fact now asks for the read inside the transaction, after the lock and before the commit. Change-Id: I6302c59c7ca0d00d25622976a5c61a031bacdeb6 Signed-off-by: Thomas Kosiewski <tk@coder.com>
Change-Id: I32c1659e05bf2b517e4a3107297df1888eb69cf1 Signed-off-by: Thomas Kosiewski <tk@coder.com>
Change-Id: I1199d18287394333c4b0627e21cec827f9d1a982 Signed-off-by: Thomas Kosiewski <tk@coder.com>
…oPurge model check.sh --record at the merge of the ReplacePacks fence fix. The covered code differs from origin/main until that fix lands, so the record names HEAD; re-run --record after the merge. Also fill in the clean-run example and the measured run time. Change-Id: I21dd054fab9c821910ec46f66efdf2c78d448341 Signed-off-by: Thomas Kosiewski <tk@coder.com>
Change-Id: I50bbb671227054076355f9fe629205263ecd1ef3 Signed-off-by: Thomas Kosiewski <tk@coder.com>
…nt main origin/main changed PG.casRef (txid_status resolution of a failed COMMIT and an optional in-transaction hook). The base-ledger lock and the purge-fence read still come before the swap, so the model's fenced CASRef still describes it. check.sh --record names HEAD until the ReplacePacks fence fix lands on main. Change-Id: I3512bd7a5b7cc9701921d6166a7e7794c193e0d5 Signed-off-by: Thomas Kosiewski <tk@coder.com>
Readiness review of the ReplacePacks fence change found that no test covered the order the change chose: the fence is read after the check that all old rows are present. A fold whose old rows the purge already retired loses cleanly (won=false, no error), and moving the fence read first would turn that into ErrRepoPurged without any test failing. The new case in TestReplacePacksPurgeFence retires the rows and checks the clean loss on all three backends. The same review noted comments and a docs line that named only registrations: ErrRepoPurged now also reaches a repack as a failed fold, the fleet prerequisite lists repack folds, and the purge comments say that a retired fold loses cleanly. Refs #645 _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_ Change-Id: Ie7bc36f7896d6ea3a2cff8e2dc9bb18f7bfb7f8c Signed-off-by: Thomas Kosiewski <tk@coder.com>
…o issue645-purger-model Change-Id: If0a0b3b53de30fc8a904e2f9e6f7c40c0ea72771 Signed-off-by: Thomas Kosiewski <tk@coder.com>
Change-Id: I8cd2875d12d709153feda781d622de8f6f789bfd Signed-off-by: Thomas Kosiewski <tk@coder.com>
…y with writers PurgeReach.cfg must reach the purge race (a push and a fold commit before the fence, the purge retires both rows and deletes K while both writers are in flight), so a model edit that cuts writers off from RegisterPacks makes check.sh stop with STALE instead of passing an empty check. PurgeSafety.cfg also checks PurgeEligible and GuardRespected with writers running. Change-Id: I2a90332a0bd3d6254042d3ba6e9fa9f9c1270d69 Signed-off-by: Thomas Kosiewski <tk@coder.com>
…y helpers
The fence-read checks now need tx as a whole argument ("tx" inside
"ctx" matched before) and PG's lockBaseLedger on baseRepoOf(...) (on
repo for the LFS path, whose repos are base repos). FenceFirst and
RefsDieFirst also need the phase's error to end the run. The helpers
behind "one key stands for a base key and its +namespace keys"
(baseRepoOf, QuotaRepoGroup and packNamespaceSuffixes, baseOf) get
fingerprints; check.sh is STALE on them until the next --record.
Change-Id: I5d52d1490245735f2ac33d9c61159c0b9599c017
Signed-off-by: Thomas Kosiewski <tk@coder.com>
…erify-orphan-sweep Name both properties that fail without RegistrationsFenced, say why a delete-mode sweep (DeleteSuperseded is on by default) adds no step after the fence, give each left-out item the harm a user sees and the test that covers it, state the LFS lock assumption (ADR 035), and say which test catches a removed PurgedRepoProbe block in the heal. Change-Id: I8460e9f0cef7059e45ddc9f1ec8d13d8e9369ae1 Signed-off-by: Thomas Kosiewski <tk@coder.com>
…ecks Each tightened fact, new fingerprint, the reachability probe and the eligibility and guard invariants in PurgeSafety.cfg were broken once in a scratch checkout, and the check named the expected property, STALE entry or probe result. Change-Id: I7b6021e47de88f4601c0f56ea6fc04a10e86e518 Signed-off-by: Thomas Kosiewski <tk@coder.com>
A fifth full run, with PurgeReach.cfg, took 4 minutes. Change-Id: Ifa22caf975a58069111e3bd5722d33bae1146d45 Signed-off-by: Thomas Kosiewski <tk@coder.com>
Change-Id: Ie1eeef4c0bda3c28e171256c25311cbcb1e29134 Signed-off-by: Thomas Kosiewski <tk@coder.com>
check.sh --record on the merge of origin/main after the ReplacePacks fence fix landed (#704). Every covered function now matches main, so the sync commit is a commit of main and a squash merge cannot orphan it. The four new fingerprints (baseRepoOf, QuotaRepoGroup, packNamespaceSuffixes, baseOf) are recorded. Refs #645 Change-Id: Ibe00aa6b0b6e9c2a6304ea04dd8ca31edfa06b9a Signed-off-by: Thomas Kosiewski <tk@coder.com>
Change-Id: I4198d2704d10193ef6f9e69cfad78ac0eb24234a Signed-off-by: Thomas Kosiewski <tk@coder.com>
Member
Author
|
@codex review |
Member
Author
|
@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: Didn't find any major issues. 🎉 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". |
A clean-context review of the RepoPurger model found six places where the text or the script said more than the check does: - Two promises that nothing checks (nothing clears deleted_at, nothing removes a fence) were listed as fingerprinted. They are now listed as unchecked, with what a user would see if one broke. - The repack-fold check is TestReplacePacksPurgeFence, not TestRepoPurgeSeams. - There are five Purge*.cfg configs, not four. - GuardRespected stops safeDelete's restore, not the heal's restores. - "No timing assumption" holds inside the model. A backup made before the fence is PackSweep's case, and the text says so. - check.sh gives java /dev/null as stdin. A java that reads stdin swallowed the remaining configs of the here-string loop and the run still printed RESULT: PASS: with such a java, the old script ran only PurgeControl.cfg of the two selected configs and the new one runs both. Refs #645 Change-Id: If5f9ed66b5a1a5374085e2eb493c9bfc1f2450cf Signed-off-by: Thomas Kosiewski <tk@coder.com>
Member
Author
|
@codex review |
Member
Author
|
@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. |
![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: 4e7611e6e6
ℹ️ 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".
… path Two findings of the second Codex review of the RepoPurger model: - The fence facts (RegistrationsFenced, RefWritesFenced, FoldsFenced) accepted any later if whose body returned ErrRepoPurged. The if must now test the first result of the fence call alone, and the lock, the fence read and the if must sit in the same transaction closure. Six breaks (`else if false && fenced`, `fenced && repo != ""`, `if false && purged`, a fence read in a second pgx.BeginFunc, in PG and SQLite) kept their fact TRUE before and turn it FALSE now. - Nothing forced a purge-repo run, so a model whose CLI ended before its phases passed every config. The new probe PurgeCliReach.cfg must reach the stamp of a purge-repo run on an old repository. With the CLI branch of PurgerStart cut short, PurgeControl.cfg and PurgeLiveness.cfg still pass and the probe passes, so check.sh exits 2. Refs #645 Change-Id: If2f2c7dfc0c041a984c996779f6b38ae13fda238 Signed-off-by: Thomas Kosiewski <tk@coder.com>
Member
Author
|
@codex review |
Member
Author
|
@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. |
|
Codex Review: Didn't find any major issues. Can't wait for the next one! 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". |
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Why
ThomasK33 asked to fix the open issues and land them on main. This PR does item 1 of #645: the
verify-orphan-sweepskill model-checks the orphan-pack sweeper, but not the repository purger (RepoPurgerandopenstorage purge-repo). The purger deletes a soft-deleted repository's refs, pack rows and blobs while pushes, REST writes and repack folds can still be running. A wrong order there gives a user one of two harms: a repository that a user can still use gets purged, or a pack row stays registered with no bytes behind it, so a push that reported success cannot be read back. Until now no check noticed a change that opened such a window.Items 2 (S3 multipart ModTime on real AWS), 3 and 4 (
osv.sh cleanup) are not in this PR.What changes
model/RepoPurge.tla(711 lines) with six configs.PurgeControl.cfgchecks eligibility and the delete guard with no writer.PurgeSafety.cfgchecks the race of two writers, the background pass, onepurge-reporun and a purge-aware sweeper, with one fault.PurgeLiveness.cfgandPurgeQuarantine.cfgcheck that a purge completes and the quarantine backups are collected.PurgeReach.cfgis a reachability probe: if a model edit cuts the writers off fromRegisterPacks, the probe passes and check.sh exits 2 instead of printing a green result over a model that tests nothing.PurgeCliReach.cfgis the same self-test for thepurge-repopath: it must reach the stamp of apurge-reporun on an old repository, which no config can force by fairness because an operator may never run the command.facts/facts.goreads 13 more code facts from the Go source (22 in all), for example that the fence is taken first (FenceFirst), that registrations, ref writes and repack folds read the purge fence under the base-ledger lock (RegistrationsFenced,RefWritesFenced,FoldsFenced), and that the heal purges only fenced repositories. The lock facts match the lock argument (baseRepoOf(...)) andtxas a whole argument.model/fingerprints.txtgains 51 fingerprints (21 to 72) of the purge code and of the helpers that map a namespace key to its base repository (baseRepoOf,QuotaRepoGroupwithpackNamespaceSuffixes,baseOf). CI'sorphan-sweep-fingerprintsjob fails when one of them changes until someone re-runscheck.sh --record.check.shruns the new configs, a newreachkind of probe, and compares the set of fact names.SKILL.mddescribes the module, the assumptions, what the model leaves out (each item with what a user sees and the test that covers it), a coverage record, and a table of every scratch break that was proven red.SKILL.mdisd7896ef4488ced6c2238f100f4ecea38cfb0a687, a commit of main (the merge of fix(ref): make ReplacePacks honor the purge fence #704), recorded withcheck.sh --recordon this tree.The model found a real race before it had a fix: with
ReplacePacksunfenced, a repack fold could register its pack after the purge fenced the repository and reaped its bytes (NoDanglingRowfails at depth 17). #704 fixed that and has merged.FoldsFencednow keeps it fixed.Verification
check.shon this tree (full run, TLC 1.7.4):RESULT: PASS. All 22 facts TRUE.PackSweep.cfg3,950,676,NoTiming.cfg6,636,617,Liveness.cfg1,138,212,PurgeControl.cfg29,362,PurgeSafety.cfg2,019,265,PurgeLiveness.cfgandPurgeQuarantine.cfg305,681 distinct states each, all PASS.NoThresholdAssumption.cfg,SlowHealEntry.cfg,PurgeReach.cfgandPurgeCliReach.cfgfail as expected.check.sh --fingerprints-only(the CI job) andverify-lane-schedule/check.sh --fingerprints-only: PASS.go build ./...andgo vetof the skill's facts program: clean.shellcheckoncheck.sh: clean.python3 scripts/check-doc-links.py: 0 broken links.python3 scripts/test_check_doc_links.py: OK.SKILL.md("Validation"): 13 purge facts, and 14 breaks of the tighter checks (for examplelockBaseLedger(ctx, tx, repo)in PGRegisterPacks,RegisterPacksunreachable for writers in the model, each new fingerprint changed alone).SKILL.md, a limit that was missing, andcheck.shnow gives java/dev/nullas stdin (with a java that reads stdin, the old script silently skipped the rest of a config loop and still printedRESULT: PASS; the new one runs every selected config).PurgeReach.cfg),PurgeEligibleandGuardRespectedinPurgeSafety.cfg, fingerprints of the base-key helpers, stricter lock andtxfacts, and the correctedSKILL.mdtext. One item is declined with a reason: a strongerHealPurgesFencedfact. In the model every backup comes from asafeDeleteafter the fence, so no RepoPurge property depends on the heal'sPurgedRepoProbeblock, and a FALSE fact would blame the wrong property.TestSweep_ListOnlyRollbackPreservesOrphanBackupsturns red when the block is removed, andSKILL.mdnames it.ifthat returnedErrRepoPurged: theifmust now test the fence call's result alone, in the transaction closure of the lock. Six breaks (else if false && fencedand similar, in PG and SQLite) kept their fact TRUE before and turn it FALSE now. And no config forced apurge-reporun: with the CLI branch of the model cut short,PurgeControl.cfgandPurgeLiveness.cfgstill passed.PurgeCliReach.cfgnow fails the run (check.sh exits 2) in that case.deleted_at, and nothing removes a fence.SKILL.mdlists them with what a user would see if one broke.registerLFSObjectTxlocks onrepo, not onbaseRepoOf(repo), because LFS objects are keyed by the base repository (ADR 035). TheRegistrationsFencedfact pins that argument andSKILL.mdstates it.Refs #645
Generated with
xum• Model:anthropic:claude-sonnet-5-5• Thinking:xhigh