Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,8 @@ after its public API and format compatibility policies are established.

## [Unreleased]

- Linux public snapshot process laws verify reader-death fence release, persistent lock identity and exclusion of new readers during collection with kernel-observed ordering (#113).

- Retention model histories now include release and restore, with expected generations and anchor sets derived independently from requested operations rather than copied from publication candidates; exact stale/retry refusals remain checked (#128).

- Public filesystem-stage integration laws now exercise production ext4 admission, exclusive creation, canonical sealed bytes, and preservation of unsealed evidence through the promised `segment_filesystem_stage` target (#147).
Expand Down
2 changes: 1 addition & 1 deletion docs/formats/segment-store-v2/requirements.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ case is not evidence.
| `KEEP-RETENTION-005` | Closure derivation is deterministic, bounded, cycle-safe, fail-closed, and verifies complete blob reconstruction | exact accounting, reconstruction, adversarial-catalog, and exhaustive model laws in `tests/retention_closure.rs`; corrupt members refuse through the inherited segment-record admission laws and seeded `segment_format` fuzz target routed by `closure-corruption.md` | Implemented |
| `KEEP-RETENTION-006` | Publication follows the exact ordered durability protocol, including new namespace-directory admission and retention of fixed-stage evidence until head commit, and returns only after cleanup synchronization | typed vocabulary and blocking port in `tests/retention_publication_phase.rs` and `tests/retention_publication_storage.rs`; ordered execution, conditional namespace sync, and all 17 exact storage-fault boundaries in `tests/retention_publication_execution.rs`; production 17-phase forward filesystem execution, exclusive staging, byte-equal inode-substitution refusal, and retained-stage recovery refusal in `filesystem_retention_storage_tests`; orphan namespace directories count against the 4,096 ceiling and refuse a new namespace before any stage is written in `filesystem_retention_capacity_tests`; crash injection remains | In progress in #19 |
| `KEEP-RETENTION-007` | Complete-stage recovery preserves canonical history; incomplete stages require disposition before mutation | Complete publication-prefix recovery and reader-state laws remain; incomplete direct/publication recovery and process-death laws now require typed refusal and preserved bytes. See [landing ledger](../../testing-evidence/retention-landing.md). | Bounded landing in #99; automatic incomplete-stage disposition explicitly deferred |
| `KEEP-RETENTION-008` | Readers double-collect catalog and retention heads and bind one complete catalog, manifest, and root-generation view under a `ReaderFence` | `ReaderFence` holds a shared kernel lock on a verified zero-length `reader.lock`; `collect_retention_view` accepts a view only when both head coordinates agree before and after loading and refuses an exhausted attempt limit (`retention_view_collector_tests`); `FilesystemRetentionSnapshot` binds the catalog snapshot, retention head, and manifest under the fence and verifies each selected root on demand while the fence is held, refusing a substituted root and a replaced fence, and two readers share the fence while an exclusive lock waits (`filesystem_retention_snapshot_tests`) | Implemented |
| `KEEP-RETENTION-008` | Readers double-collect catalog and retention heads and bind one complete catalog, manifest, and root-generation view under a `ReaderFence` | `ReaderFence` holds a shared kernel lock on a verified zero-length `reader.lock`; `collect_retention_view` accepts a view only when both head coordinates agree before and after loading and refuses an exhausted attempt limit (`retention_view_collector_tests`); `FilesystemRetentionSnapshot` binds the catalog snapshot, retention head, and manifest under the fence and verifies each selected root on demand while the fence is held, refusing a substituted root and a replaced fence, and two readers share the fence while an exclusive lock waits (`filesystem_retention_snapshot_tests`); Linux public snapshot process laws prove live-reader exclusion, SIGKILL fence release with persistent inode preservation, and kernel-queued new-reader exclusion until collection releases the fence (`tests/reader_fence_process.rs`; [evidence](../../testing-evidence/reader-fence-process.md)) | Implemented |
| `KEEP-RETENTION-009` | Exact already-committed retry is idempotent only while its successor remains current | byte-identical planning in `tests/retention_transition.rs`; authority-revalidated zero-mutation retry receipt in `tests/retention_publication_execution.rs`; exact already-committed filesystem retry with a byte-identical retention witness in `filesystem_retention_storage_tests`; superseded-candidate filesystem refusal with zero mutation in `filesystem_retention_successor_tests`; committed retry reopens the head-selected manifest entry and root pool bytes, refusing absent, changed, or corrupt evidence in `filesystem_retention_current_tests`; every refusal is a typed `RetentionCurrentStateRefusal` source, with superseded, committed-root-absent, committed-root-changed, and head-absent-with-artifacts pinned by downcast | Implemented |
| `KEEP-RETENTION-010` | Model operation sequences agree with a deterministic namespace-to-anchor-set map and never admit caller identity, paths, clocks, or application policy | all three-operation histories over initial publications of two namespaces, successor, release, restore, byte-identical retry and stale initial (343 histories, each in a fresh migrated store) compare fenced namespace generations, anchor sets and liveness against an operation-derived model after every step; exact typed refusals remain checked. The count describes exploration, not correctness. See [release/restore evidence](../../testing-evidence/retention-release-restore-model.md). Core architecture checks remain separate static evidence. | Implemented; release/restore model coverage added for #128 |

Expand Down
37 changes: 37 additions & 0 deletions docs/testing-evidence/reader-fence-process.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
# Reader-fence process evidence

This change addresses #113 and the process-death/exclusion portion of original T-19.1 and KEEP-RETENTION-008. Change kind: missing verification, with no production behavior change. Owner: `@flyingrobots`. The branch starts from main `6051abb25a9fd33ae7ee0de5614514b709a4d82a`, including #99. This record does not claim mainline delivery before its PR merges.

## Contract and observations

`tests/reader_fence_process.rs` loads a real `FilesystemRetentionSnapshot` in a separate process over a fresh migrated golden store. The child sends readiness only after public snapshot admission completes and keeps the snapshot alive until an explicit release message or SIGKILL. The parent takes actual writer authority before acting as a collector and uses the protocol's exclusive kernel lock on the persistent `reader.lock` file.

`reader_death_releases_collection_without_replacing_the_fence` requires exclusive acquisition to return exactly `EWOULDBLOCK` while that snapshot lives. After killing and reaping the reader with a verified SIGKILL result, the same collector descriptor must acquire the exclusive lock. The persistent pathname must still name the original device/inode and have zero length. This is kernel process-death evidence, not a Rust destructor simulation.

`collection_excludes_a_new_snapshot_until_release` holds the exclusive fence before spawning a reader. It requires Linux `/proc/locks` to report a queued shared flock for that exact child PID and the owned fence inode. A child that announces snapshot readiness before appearing in that queue fails immediately. The parent then releases collection authority and requires successful snapshot admission and normal child completion. The kernel queue is the blocking witness; elapsed time without a message is never accepted as proof of exclusion.

The fixed schedules are live-reader → exclusive refusal → SIGKILL/reap → exclusive admission, and exclusive collector → queued reader → collector release → admitted reader. Unix-domain channels establish readiness. Polling yields to the scheduler without sleeps. Twenty-second watchdogs only fail stuck executions; they cannot produce a passing exclusion result. The tests do not explore arbitrary interleavings, physical power loss, or a complete garbage collector implementation.

## Calibration and replay

The unmodified product passes both laws. In a separately copied source/build tree, replacing shared-lock acquisition with an unlock makes both laws fail: the live-reader check observes `Ok(())` instead of `EWOULDBLOCK`, and the collector-exclusion check reports `snapshot escaped the exclusive collector fence`. This is an observed runtime calibration of missing evidence, not a claim that main contains a production locking bug. The mutation is not included in the branch.

Run `cargo test --all-features --locked --test reader_fence_process` and its `--release` variant. The tests are Linux-only and require `repository-tasks` and a readable `/proc/locks` for their PID namespace; unsupported platforms do not supply this evidence. Their subprocess inherits the same executable and exact test name, keeping process creation outside `src`. Immutable candidate SHA, toolchain and validation results are recorded in the PR.

These are medium-size, single-machine tests with owned filesystem scratch and Unix-domain sockets, no network service, ambient identity selection or random input. The fixture uses repository-only initialization/migration admission to isolate fencing; this is not proof of production platform eligibility. Kernel observations are restricted to the owned child and lock. Child cleanup kills/reaps on failure. Existing ordinary-test memory/resource-ceiling gaps remain as documented in the enforcement profile; watchdogs are not a memory sandbox or suite latency SLO.

Retire these laws only if the reader-fence contract disappears or stronger process/schedule evidence subsumes the same guarantees. Existing same-process sharing, fence substitution, corruption and snapshot-consistency tests remain. No format, API, identity, recovery protocol or performance behavior changes.

## Landing calibration closure

The landing review identified three distinct release/preservation observations not reached by the original missing-shared-lock mutation. One bounded batch closes that evidence gap on source `ee21b01d7b7740eaa56116809630534ea7caa05b`, tracked tree `b2a9420cf78b4196c75747d5db16d099dfb18937`, with Rust 1.96.0 on Linux aarch64 and actual ext4 scratch. Each experiment uses a separate copied source and build directory, preserves expected outcomes, compiles, and exits 101 at the intended runtime failure.

The [retained-authority patch](reader-fence-process/retained-authority.patch) adds a real shared holder in the parent after live-reader exclusion, before SIGKILL. The unchanged exclusive acquisition after killing/reaping the child returns `EWOULDBLOCK`, recorded in its [RED receipt](reader-fence-process/retained-authority-red.txt). This is an OS-boundary negative control demonstrating that the law detects authority remaining after death; it does not allege an existing Keep bug or add a production subprocess path.

The [persistent-fence patch](reader-fence-process/persistent-fence.patch) changes the actual fence length to one after production's last acquisition guard while preserving its shared flock. Live exclusion and post-death reacquisition still succeed; the unchanged persistent-fence assertion then observes the same device/inode with length one instead of zero, as its [RED receipt](reader-fence-process/persistent-fence-red.txt) shows. This calibrates the combined preservation observation, not separate mutations of each metadata coordinate.

The [post-release-admission patch](reader-fence-process/post-release-admission.patch) returns a typed production `Fence` failure after the real shared acquisition. The collector-exclusion law first observes the child in the kernel wait queue, releases collection, and then fails its unchanged admission-readiness read with `UnexpectedEof`; see its [RED receipt](reader-fence-process/post-release-admission-red.txt). Parent and child stderr interleave in that raw receipt; the partial child error is preserved without reconstruction. Source ordering establishes that the failure occurs after the queued wait and collector release, rather than during fixture setup or before exclusion.

Replay each patch independently with `git apply --unidiff-zero` in a fresh copy of the source above. Use `cargo test --all-features --locked --test reader_fence_process reader_death_releases_collection_without_replacing_the_fence -- --exact --nocapture` for the first two experiments; use the same command with `collection_excludes_a_new_snapshot_until_release` for the third. The [restored GREEN receipt](reader-fence-process/restored-green.txt) records the unmodified source tree and both laws passing in debug and release. Final receipt-only successors leave runtime code and test expectations unchanged.

Committed logs replace only the isolated container source/build path prefixes with descriptive placeholders and remove trailing empty lines. Patches use zero-context hunks to avoid incidental whitespace in evidence files. The original raw logs, complete experiment variants and traced launcher remain retained by the author. Signal status and channel markers attest execution of the intended schedule; they are not represented as separate product promises. These calibrations do not extend the two fixed schedules, platform coverage, resource enforcement or power-loss claims above.
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
Compiling rustix v1.1.4
Compiling io-lifetimes v2.0.4
Compiling bitflags v2.13.1
Compiling io-lifetimes v3.0.1
Compiling linux-raw-sys v0.12.1
Compiling io-extras v0.19.0
Compiling proc-macro2 v1.0.107
Compiling quote v1.0.47
Compiling once_cell v1.21.4
Compiling unicode-ident v1.0.24
Compiling cap-primitives v4.0.2
Compiling find-msvc-tools v0.1.9
Compiling shlex v2.0.1
Compiling cap-std v4.0.2
Compiling ambient-authority v0.0.2
Compiling ipnet v2.12.0
Compiling maybe-owned v0.3.4
Compiling cap-fs-ext v4.0.2
Compiling anstyle v1.0.14
Compiling clap_lex v1.1.0
Compiling libc v0.2.186
Compiling cc v1.3.0
Compiling cfg-if v1.0.4
Compiling constant_time_eq v0.4.2
Compiling arrayref v0.3.9
Compiling clap_builder v4.6.2
Compiling arrayvec v0.7.8
Compiling regex-lite v0.1.9
Compiling condtype v1.3.0
Compiling allocation-counter v0.8.1
Compiling syn v2.0.119
Compiling blake3 v1.8.5
Compiling clap v4.6.4
Compiling rustix-linux-procfs v0.1.1
Compiling fs-set-times v0.20.3
Compiling divan-macros v0.1.21
Compiling keep v0.0.0 (<calibration-source>)
Compiling divan v0.1.21
Finished `test` profile [unoptimized + debuginfo] target(s) in 3.30s
Running tests/reader_fence_process.rs (<calibration-target>/debug/deps/reader_fence_process-d5b0d43619bf3bf3)

running 1 test

thread 'reader_death_releases_collection_without_replacing_the_fence' (1942759) panicked at tests/reader_fence_process.rs:45:5:
assertion `left == right` failed: reader death must leave the same empty persistent fence
left: (1792, 130331, 1)
right: (1792, 130331, 0)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
test reader_death_releases_collection_without_replacing_the_fence ... FAILED

failures:

failures:
reader_death_releases_collection_without_replacing_the_fence

test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 1 filtered out; finished in 0.21s

error: test failed, to rerun pass `--test reader_fence_process`
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
diff --git a/src/adapters/retention/reader_fence.rs b/src/adapters/retention/reader_fence.rs
--- a/src/adapters/retention/reader_fence.rs
+++ b/src/adapters/retention/reader_fence.rs
@@ -49,0 +50 @@ impl ReaderFence {
+ root.open_with(READER_LOCK, cap_std::fs::OpenOptions::new().write(true))?.set_len(1)?;
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
Compiling rustix v1.1.4
Compiling io-lifetimes v3.0.1
Compiling io-lifetimes v2.0.4
Compiling linux-raw-sys v0.12.1
Compiling bitflags v2.13.1
Compiling io-extras v0.19.0
Compiling proc-macro2 v1.0.107
Compiling quote v1.0.47
Compiling unicode-ident v1.0.24
Compiling find-msvc-tools v0.1.9
Compiling shlex v2.0.1
Compiling once_cell v1.21.4
Compiling cap-primitives v4.0.2
Compiling maybe-owned v0.3.4
Compiling cap-std v4.0.2
Compiling ipnet v2.12.0
Compiling ambient-authority v0.0.2
Compiling clap_lex v1.1.0
Compiling anstyle v1.0.14
Compiling cap-fs-ext v4.0.2
Compiling libc v0.2.186
Compiling cc v1.3.0
Compiling cfg-if v1.0.4
Compiling constant_time_eq v0.4.2
Compiling arrayvec v0.7.8
Compiling clap_builder v4.6.2
Compiling arrayref v0.3.9
Compiling condtype v1.3.0
Compiling regex-lite v0.1.9
Compiling allocation-counter v0.8.1
Compiling syn v2.0.119
Compiling blake3 v1.8.5
Compiling clap v4.6.4
Compiling rustix-linux-procfs v0.1.1
Compiling fs-set-times v0.20.3
Compiling divan-macros v0.1.21
Compiling keep v0.0.0 (<calibration-source>)
Compiling divan v0.1.21
Finished `test` profile [unoptimized + debuginfo] target(s) in 3.32s
Running tests/reader_fence_process.rs (<calibration-target>/debug/deps/reader_fence_process-d5b0d43619bf3bf3)

running 1 test
Error: Fence { source: Custom { kind: Other, errorError: Error { kind: UnexpectedEof, message: "failed to fill whole buffer" }
test collection_excludes_a_new_snapshot_until_release ... FAILED

failures:

failures:
collection_excludes_a_new_snapshot_until_release

test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 1 filtered out; finished in 0.16s

error: test failed, to rerun pass `--test reader_fence_process`
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
diff --git a/src/adapters/retention/filesystem_retention_snapshot.rs b/src/adapters/retention/filesystem_retention_snapshot.rs
--- a/src/adapters/retention/filesystem_retention_snapshot.rs
+++ b/src/adapters/retention/filesystem_retention_snapshot.rs
@@ -137,0 +138,3 @@ impl FilesystemRetentionSnapshot {
+ if root.exists("reader.lock") {
+ return Err(Error::Fence { source: io::Error::other("calibrated post-lock admission failure") });
+ }
21 changes: 21 additions & 0 deletions docs/testing-evidence/reader-fence-process/restored-green.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
+ git rev-parse 'HEAD^{tree}'
b2a9420cf78b4196c75747d5db16d099dfb18937
+ cargo test --all-features --locked --test reader_fence_process
Finished `test` profile [unoptimized + debuginfo] target(s) in 0.01s
Running tests/reader_fence_process.rs (<restored-target>/debug/deps/reader_fence_process-d5b0d43619bf3bf3)

running 2 tests
test reader_death_releases_collection_without_replacing_the_fence ... ok
test collection_excludes_a_new_snapshot_until_release ... ok

test result: ok. 2 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.07s

+ cargo test --all-features --release --locked --test reader_fence_process
Finished `release` profile [optimized] target(s) in 0.01s
Running tests/reader_fence_process.rs (<restored-target>/release/deps/reader_fence_process-2a35bc062b89d081)

running 2 tests
test reader_death_releases_collection_without_replacing_the_fence ... ok
test collection_excludes_a_new_snapshot_until_release ... ok

test result: ok. 2 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.05s
Loading
Loading