Skip to content

Commit 48784f4

Browse files
committed
Research: add a persist-only section; re-grade the SnapshotFold filter
- §1.1 'What ships: the persist-only subset': the study audits the full (deferred, evolution-gaming#834) fence, but the shipped artifact is persist-only - persist offset-fenced, delete plain LWW; evolution-gaming#732 closed for persists, left open for deletes (the documented residual, modelled by cassandra_notomb + tested by SnapshotSpec). Records what actually ships, not only the deferred design. - claims R6: SnapshotFold's filter is the *primary* liveness mechanism in the shipped persist-only mode (no monotonic buffer), not belt-and-suspenders, and it is unit-tested (SnapshotFoldSpec) - graded code+test.
1 parent 6031aa5 commit 48784f4

2 files changed

Lines changed: 18 additions & 1 deletion

File tree

research/claims.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ defect can hide.
4646
| R3 | `Snapshots.append` drops a lower-offset live append (buffer monotonic); sound under deterministic folds | code `Snapshots.put`; `SnapshotsSpec`; determinism is an assumption (A2) | ✅ (modulo A2) |
4747
| R4 | Delete fenced on `max(currentOffset, highWater)`; legitimate owner presents `X`, stale writer still fenced | code `put` tombstone lift; `SnapshotReplayFencingSpec`; IT `FlowSpec` delete-during-replay; model `cassandra_refines` ||
4848
| R5 | Re-derived snapshot below `X` never re-persisted (flush no-op; buffer stays `persisted`) | code `put` (below ⇒ keep cell); `SnapshotsSpec` ||
49-
| R6 | `SnapshotFold` filter (`record.offset > snapshot.offset`) makes monotonic-append belt-and-suspenders for persists; tick-delete bypasses the filter, so the buffer is the only protection for it | code `SnapshotFold`, `TickToState` ||
49+
| R6 | `SnapshotFold` filter (`record.offset > snapshot.offset`) keeps only records past the recovered offset. In the full design it makes monotonic-append belt-and-suspenders for persists (tick-delete bypasses it, so the buffer is the only protection there); in the **shipped persist-only mode it is the *primary* liveness mechanism** — there is no monotonic buffer, so it alone keeps the owner from re-persisting below its recovered high-water | code `SnapshotFold`, `TickToState`; test `SnapshotFoldSpec` (equal-offset drop) ||
5050
| R7 | Fence live only for `KafkaSnapshot`/CAS wiring (`Some(_.offset)`); others `None` unfenced | code wiring — **finding F2: LWW-mode Cassandra also wires fenced** (see seams S9) | ⚠️ |
5151

5252
## Deleted-key recovery

research/report.md

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,23 @@ argument; where the design depends on Cassandra behaviour, verify against primar
5353
study's own predictions differ from reality, report the discrepancy (§4.1 contains one). The load-bearing
5454
hedge against self-review bias is external: a fresh-context review committee (§10).
5555

56+
### 1.1 What ships: the persist-only subset
57+
58+
The studied subject is the *full* fence; the *shipped* artifact is a deliberate subset —
59+
**persist-only** (`tj/…-cassandra-persist-only`). It gates every `persist` (`IF offset <= :offset`, the
60+
first-write compound, and the F-1 guard-expired repair) but leaves `delete` a plain last-write-wins
61+
`DELETE`. So #732 is closed **for persists** — a stale owner cannot overwrite a newer snapshot — and
62+
left **open for deletes**: during an overlap a stale writer can still erase a newer snapshot or
63+
resurrect a just-deleted key, and with events-recovery a crash alone can revive one (the same revive
64+
that exists under plain last-write-wins). That residual is a documented boundary, not an oversight, and
65+
it is pinned as such — modelled (`cassandra_notomb` = `Guarded ∧ ¬Tombstone`, VIOLATES
66+
`INV_NoCorruptDurable`) and integration-tested (`SnapshotSpec`, "a delete is unguarded … persist-only
67+
gap"). Fencing the delete is what pulls in the offset-carrying tombstone, the monotonic buffer,
68+
tombstone-floor recovery and the events-recovery floor (the F-2/F-3/F-6/F-7 machinery) — a breaking API
69+
and a liveness trap on each recovery path — so the full design was verified here but **deferred**
70+
(upstream #834), not shipped. The rest of this report audits that deferred design; persist-only is the
71+
conservative first step whose cost/benefit the audit is what justifies.
72+
5673
## 2. Method
5774

5875
1. **Claim inventory** (`claims.md`): 40+ claims extracted from the docs and load-bearing comments,

0 commit comments

Comments
 (0)