# Reclamation, Retry, and Topology Proof Pack — bd-db300.5.3.3.2
> Implementation-ready proof/evidence pack for `PagerCommittedSnapshot` (M6).
> Covers reclamation contract, bounded retry, starvation, control-mode
> equivalence, logging fields, and verify script extension plan.
---
## 1. Reclamation Contract
### 1.1 Mechanism
`PagerCommittedSnapshot` is published via `Arc<RwLock<Arc<PagerCommittedSnapshot>>>`.
```
Writer (commit path):
1. Build new Arc<PagerCommittedSnapshot> from PagerInner (Mutex held)
2. Take RwLock write-guard (~nanoseconds)
3. Swap the Arc pointer: *guard = new_snapshot
4. Drop RwLock write-guard
→ Old Arc's strong count decrements by 1
Reader (committed_snapshot()):
1. Take RwLock read-guard (~nanoseconds)
2. Arc::clone the inner Arc (atomic refcount bump)
3. Drop RwLock read-guard
→ Reader now owns an independent Arc to the snapshot
```
**Reclamation:** The old snapshot is freed when its `Arc` strong count reaches zero —
i.e., when every reader that cloned it before the swap drops their clone. No explicit
epoch tracking, hazard pointers, or deferred reclamation is needed.
### 1.2 Proof: Readers cannot observe freed metadata
**Claim:** A reader holding `Arc<PagerCommittedSnapshot>` always points to valid memory.
**Proof:**
1. `Arc::clone` increments the strong count atomically before the RwLock read-guard is released.
2. The writer's swap replaces the shared pointer but does not drop the old `Arc` — it merely
decrements the strong count by 1 (from the shared slot).
3. The old `Arc` is freed only when ALL readers who cloned it drop their clones.
4. A reader's clone keeps the allocation alive for the reader's entire scope.
5. `PagerCommittedSnapshot` is `Copy` — even if the `Arc` allocation were freed (which
step 3-4 prevent), the snapshot content is a plain struct with no interior pointers,
dangling references, or heap allocations. There is no use-after-free vector.
**Invariant:** `strong_count(old_snapshot) >= number_of_live_reader_clones` at all times.
This is guaranteed by `Arc`'s atomic reference counting.
### 1.3 Bounded reclamation lag
**Claim:** Memory occupied by stale snapshots is bounded by `O(active_readers)`.
**Proof:**
- Each commit produces one `Arc<PagerCommittedSnapshot>` allocation (~64 bytes + Arc overhead ≈ ~80 bytes).
- Each reader holds at most one `Arc` clone (taken at begin-time, dropped at commit/rollback-time).
- Maximum stale allocations alive = number of concurrent readers holding pre-swap clones.
- With N concurrent readers, worst case = N stale snapshots × 80 bytes = 80N bytes.
- For N=64 (MAX_FC_THREADS): 5120 bytes. Negligible.
### 1.4 No GC, no epoch, no hazard pointers
The `Arc` reference counting is:
- Lock-free on the read side (atomic increment)
- Wait-free on the drop side (atomic decrement + conditional dealloc)
- Deterministic (freed immediately when last reference drops)
- No background GC thread, no epoch advancement, no quiescent-state requirement
This is the simplest correct reclamation strategy for this access pattern.
---
## 2. Bounded Retry and Starvation
### 2.1 Reader retry contract
**Claim:** Readers NEVER retry. The `committed_snapshot()` accessor is wait-free modulo
the RwLock read-guard acquisition.
**Proof:**
- `RwLock::read()` blocks only if a writer holds the write-guard.
- The write-guard is held for exactly one pointer swap (~2 nanoseconds).
- Reader wait time is bounded by the writer's swap duration: ~2ns worst case.
- No retry loop exists in the reader path. It's a single `RwLock::read()` + `Arc::clone()`.
**Contrast with M1 (PublishedPagerState seqlock):** The seqlock reader MAY retry if it
observes an odd sequence number (writer in progress). M6's `Arc` publication has no
retry — the RwLock serializes the pointer swap, and readers always see a consistent
`Arc` pointer.
### 2.2 Writer starvation contract
**Claim:** Writers are not starved by readers.
**Proof:**
- `std::sync::RwLock` on Linux (glibc pthreads) uses write-preferring semantics:
once a writer is waiting, new readers queue behind it.
- The write-guard hold time is ~2ns (one pointer swap). No reader can hold the
read-guard long enough to starve a writer, because `Arc::clone` is a single
atomic increment (~1ns).
- Even under 64 concurrent readers, the writer waits at most for the currently
in-progress `Arc::clone` operations to finish — bounded by ~64ns worst case.
### 2.3 Starvation test scenario
```rust
// Verify: 64 concurrent readers + 1 writer → writer completes within 1ms
// (generous bound; expected ~100ns)
#[test]
fn committed_snapshot_writer_not_starved_by_readers() {
// Spawn 64 reader threads in tight loop: committed_snapshot() + inspect
// Spawn 1 writer thread: publish_committed_snapshot_from_inner() in loop
// Assert: writer completes 1000 publishes within 1 second
}
```
---
## 3. Topology Sensitivity Analysis
### 3.1 Cross-NUMA behavior
The `RwLock` and `Arc` refcount are the two atomic contention points.
**RwLock:** On cross-NUMA, the RwLock's internal futex word bounces between nodes.
Hold times are ~2ns (writer) and ~1ns (reader), so the cache-line migration cost
(~100-200ns cross-node) dominates the hold time. Under c8+ cross-NUMA:
- Reader throughput: ~5M reads/sec/core (bounded by cache-line round-trip)
- Writer throughput: ~5M writes/sec (bounded by same)
This is 200× faster than the current PagerInner Mutex path (~25µs per begin under
contention), so even with NUMA overhead, the snapshot path is a massive improvement.
**Arc refcount:** Each `Arc::clone` and `drop` touches the same cache line (the
refcount). Under 64 readers all cloning/dropping simultaneously, this creates
refcount bouncing. Mitigation: readers clone once at begin-time and drop once
at commit-time — not in a tight loop. The refcount traffic is proportional to
transaction rate, not query rate.
### 3.2 Topology test scenario
```rust
// Pin readers to different NUMA nodes, verify no degradation > 2× vs local
#[test]
#[cfg(target_os = "linux")]
fn committed_snapshot_cross_numa_no_severe_degradation() {
// Use libc::sched_setaffinity to pin threads to different CPUs
// Measure committed_snapshot() latency per-node
// Assert: max_node_latency < 2 * min_node_latency
}
```
### 3.3 Interference with other controllers
Per the Controller Composition Proof (bd-db300.7.8.4):
- **E4 admission controller** reads M1 (seqlock), not M6 (snapshot). No interference.
- **D1 WAL policy** affects commit frequency, which affects snapshot publication rate.
Higher publication rate → more `Arc` allocations → negligible (80 bytes each).
- **E6 placement** may move readers/writers across NUMA nodes. The topology analysis
in §3.1 shows this is still 200× faster than the Mutex path.
No composition guard needed for M6 snapshot publication.
---
## 4. Control-Mode Equivalence
### 4.1 Modes
| `auto` (default) | Snapshot publication active; begin-path reads snapshot | Production |
| `legacy` | Snapshot publication active but ignored; begin-path takes PagerInner Mutex | A/B comparison, rollback |
| `shadow` | Both paths execute; compare results; log divergence | Adoption validation |
### 4.2 Equivalence proof
**Claim:** In all modes, the committed state visible to a reader is identical.
**Proof:**
- The snapshot is published from inside the PagerInner Mutex critical section,
BEFORE the Mutex is released. The snapshot therefore contains exactly the same
state that the Mutex-based path would observe.
- `from_inner(&inner)` copies scalar fields directly from PagerInner.
- No field is transformed, recomputed, or approximated.
- Shadow mode compares `snapshot.commit_seq == inner.commit_seq` (etc.) and logs
any mismatch as `shadow_verdict = "diverged"`. By construction, this can only
happen if the publish was skipped or the Mutex was released before publish.
### 4.3 Shadow-compare implementation sketch
```rust
// In begin() when shadow mode is active:
let snapshot = self.committed_snapshot();
let inner = self.inner.lock()?;
let direct = PagerCommittedSnapshot::from_inner(&inner);
if *snapshot != direct {
tracing::warn!(
target: "fsqlite::metadata",
event = "shadow_divergence",
snapshot_commit_seq = snapshot.commit_seq.get(),
direct_commit_seq = direct.commit_seq.get(),
snapshot_db_size = snapshot.db_size,
direct_db_size = direct.db_size,
);
}
// Proceed with inner (legacy path) regardless
```
---
## 5. Logging Contract
Every snapshot publication and read emits (when tracing is enabled at DEBUG or above):
### 5.1 Publication (write side)
```
target: "fsqlite::metadata"
event: "snapshot_publish"
fields:
trace_id: <connection trace ID>
metadata_class: "M6_pager_committed"
publication_generation: <commit_seq after commit>
db_size: <pages>
journal_mode: <mode>
freelist_count: <count>
writer_active: <bool>
control_mode: "auto" | "legacy" | "shadow"
elapsed_ns: <RwLock write-hold duration>
```
### 5.2 Read (reader side)
```
target: "fsqlite::metadata"
event: "snapshot_read"
fields:
trace_id: <connection trace ID>
metadata_class: "M6_pager_committed"
publication_generation: <snapshot.commit_seq>
snapshot_age_commits: <current_global_commit_seq - snapshot.commit_seq>
control_mode: "auto" | "legacy" | "shadow"
shadow_verdict: "clean" | "diverged" | "not_run"
elapsed_ns: <RwLock read-hold + Arc::clone duration>
```
### 5.3 Fallback
```
target: "fsqlite::metadata"
event: "snapshot_fallback"
fields:
trace_id: <connection trace ID>
metadata_class: "M6_pager_committed"
```
---
## 6. Tracked Verification Gate
### 6.1 `scripts/verify_e3_3_metadata_publication.sh`
The tracked replay entrypoint is `scripts/verify_e3_3_metadata_publication.sh`.
It is intentionally run through `rch exec --` for all Cargo work and emits a
per-run artifact bundle under `artifacts/bd-db300.5.3.3/<run_id>/`:
- `events.jsonl` records phase start/pass/fail events with `trace_id`, `run_id`,
`scenario_id`, elapsed milliseconds, and the phase command.
- `report.json` records the run identifiers, event log path, smoke-benchmark
output path, and final pass result.
- Phase logs capture the committed-snapshot unit matrix, reclamation stress,
writer-progress stress, pager `cargo check`, and a small concurrent-writer
smoke run.
The script changes to `WORKSPACE_ROOT` before invoking Cargo so the gate can be
run from any current directory while still resolving workspace packages and
artifact paths predictably.
### 6.2 Test inventory
| `committed_snapshot_reflects_commit` | pager.rs | Snapshot matches PagerInner after commit |
| `committed_snapshot_survives_reader_hold` | pager.rs | Old snapshot stays valid while reader holds Arc |
| `committed_snapshot_reclamation_stress` | pager.rs | 10K commits + 64 readers → no leak, bounded memory |
| `committed_snapshot_writer_not_starved` | pager.rs | 64 readers can't starve 1 writer |
| `committed_snapshot_shadow_no_divergence` | connection.rs | Shadow compare on 1000 txns → zero divergence |
| `committed_snapshot_control_mode_legacy` | connection.rs | Legacy mode matches auto mode results |
| `committed_snapshot_ddl_invalidation` | connection.rs | DDL bumps snapshot generation correctly |
| `committed_snapshot_cross_numa_bounded` | pager.rs | Cross-node latency < 2× local (Linux only) |
---
## 7. Primitive Re-Selection Gate
If any of the following evidence surfaces, the `Arc<RwLock<Arc<...>>>` primitive
MUST be reconsidered:
| Shadow divergence rate > 0 in production | Any occurrence | Bug in publish ordering; investigate before shipping |
| RwLock write-hold > 1µs (p99) | Sustained > 1000 samples | Possible write-side contention; consider CAS-based swap |
| Arc refcount bouncing > 10% of commit latency | Profiled via perf | Consider thread-local snapshot caching with generation check |
| Memory growth from stale snapshots | > 1MB sustained | Investigate long-lived readers; add snapshot TTL or warning |
| Cross-NUMA latency > 5× local | Profiled | Consider per-node snapshot replicas (sharded publication) |
None of these are expected based on the design analysis, but the gates exist to
force a re-evaluation rather than silently degrading.
---
## 8. Summary: What Makes This Implementation-Ready
1. **Reclamation is automatic** — `Arc` refcount, no manual epoch/GC.
2. **Retry count = 0** — readers never retry (RwLock, not seqlock).
3. **Starvation is bounded** — write-preferring RwLock, ~2ns hold.
4. **Topology impact is analyzed** — 200× faster than Mutex even cross-NUMA.
5. **Control modes defined** — auto/legacy/shadow with equivalence proof.
6. **Logging fields specified** — 12 fields covering publish, read, fallback.
7. **Verify script designed** — 6-phase test plan with artifact collection.
8. **Re-selection gates explicit** — 5 measurable thresholds that force primitive change.