Repository navigation
feat(publish): prototype generation-directory publish (not wired), with experiments and a model check - #275
Merged
Conversation
…ts and a model check PROTOTYPE, not wired into any subcommand. It follows the maintainer's decision on #264 to replace per-file writes with a generation-directory publish. It is here so the design can be judged on evidence before any output path uses it. - src/publish.rs: write a generation into <stem>.gen/<id>.partial/, rename it complete, then under an advisory lock move the CURRENT manifest (JCS, with SHA-256 per file) unless a newer generation is already current. Mirrors at the old paths are refreshed by hard link and rename; old generations are collected. Lock-free readers retry when a generation is collected under them. - examples/publish_stress.rs: multi-process race, kill -9 crash and latency experiments comparing in-place fs::write, per-file rename and generation publish. - tests/publish_model.rs: an exhaustive explicit-state check of the protocol (up to 3 writers, 1 reader, a crash at every step, garbage collection of live and crashed writers' partial generations). P1–P3 hold. P4 (mirrors consistent after a crash) fails as expected, matching the crash experiment. Three mutants show the checker detects broken protocols. Two defects the experiments found are fixed here, each with a test that fails without the fix: GC raced a writer's rename of its own partial directory, and a reader could lose a generation to GC. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PFaqv6iBXrt3W5Akd1Fq5k
Contributor
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 57 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. |
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
Hypatia flagged 25 unwrap() calls, one expect() and one panic! in examples/publish_stress.rs (CWE-754). The example now returns anyhow::Result throughout: bad arguments and I/O failures exit with a message and status 1. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PFaqv6iBXrt3W5Akd1Fq5k
…status rows - verification/proofs/tlaplus/GenerationPublish.tla: the protocol for TLC, step for step like tests/publish_model.rs. Eight configs, each stating its expected outcome. P1–P3 pass for 3 writers with keep 0 and 1 (up to 17,744 distinct states). P4 passes without crashes and fails after one, the documented mirror limit. The reader without a retry fails P3. Three mutants each fail P1 or P2. - check.sh checks the jar's SHA-256 (tla2tools v1.7.4, TLC 2.19) and fails on any unexpected outcome. It fails both ways: on a wrong jar, and on a planted wrong expectation. - verify.yml gains a `tlaplus` job that runs it, recording a PROOF-POLICY §6 deviation (TLC is not in Guix or the container yet). actionlint 1.7.7 is clean, and the job uses only the already-locked checkout pin. - The "swap before complete" mutant now moves the pointer when the partial generation is created, in both models, matching its name. - docs/design/GENERATION-PUBLISH.adoc: layout, protocol, guarantees, measurements and open questions. It records the owner's decision to keep hard-link mirrors and document the crash limit. - PROOF-NEEDS.adoc: a TESTED row for the protocol, with bounds and the §4 exception, and an OPEN Creusot/Pearlite + Verus row for the pure decisions. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PFaqv6iBXrt3W5Akd1Fq5k
hyperpolymath
marked this pull request as ready for review
November 9, 2026 15:46
Codex Review Summary: ❌ FailedThis 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. |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
hyperpolymath
enabled auto-merge (squash)
November 9, 2026 22:51
|
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.
Prototype, kept as a draft until the maintainer decides the open design questions. Nothing calls it yet.
Why
On #264 the maintainer chose to replace per-file output writes with a generation-directory publish. This prototype tests that design on evidence first.
The publish is meant to close three gaps that exist in every output mode today:
What is here
src/publish.rsFor a report
D/S.json, the layout is:D/S.gen/<id>/: one complete generation per directory.D/S.gen/CURRENT: a JCS manifest naming the current generation and the SHA-256 of each of its files.D/S.jsonand the other output names: hard links into the current generation, with copies where linking fails.A publish runs in this order:
<id>.partial/, syncing each file.<id>.File::lock:CURRENTnames a newer generation (ids sort by run start);CURRENTby temp file and rename;Readers take no lock. When the generation
CURRENTnamed has been collected, they retry fromCURRENT.examples/publish_stress.rsCompares three strategies:
inplace(fs::write, as on main),perfile(rename each file) andgenset(this prototype). It runs a multi-process race, kill -9 crash trials and a latency bench.tests/publish_model.rsAn exhaustive explicit-state check of the protocol, reported as TESTED with these bounds:
Results:
CURRENTnames only complete generations, it never moves backwards, and manifest readers never fail or return a partial set.Measured on Linux 6.18, ext4, 4 cores
Defects the experiments found, each fixed here with a test that fails without the fix:
.partialdirectory, so a writer crashed with NotFound in 1 of 40 races.Open before this can be wired
currentsymlink pointer (crash-consistent on Unix), or to drop the mirrors.PROOF-POLICY§1.2 and §4:Generated by Claude Code