Protect Cassandra snapshot writes from stale writers (full compare-and-set fence)

[tobiajo]

Stacked on (merge first): #838

Problem

The persist-only fence (#838) leaves delete last-write-wins, so a stale writer can still revive a just-deleted key. Events recovery has its own replay-window exposure: a journal fold could regress a key below an existing snapshot's offset and revive it.

Fix

Extend the compare-and-set to the full fence: persist and delete are offset-fenced. A fenced delete always writes an offset-carrying tombstone — even for a never-persisted key — so a later replay of an already-deleted record cannot revive it. Events recovery seeds the replay-window floor from the snapshot store and routes initPersisted through the monotonic cell, closing the journal revive. A guard-expired row is read as absent and repaired via IF offset = null.

The store API changes (breaking): the persist/delete write pair and the get/recover read pair collapse into one Stored[S] ADT — a live snapshot or an offset-carrying tombstone — so the read, the write and the per-key buffer reason about one monotonic cell.

Tests and docs

The compare-and-set suite, the replay-fencing spec (a replayed delete after its tombstone was TTL-reaped stays a fence), the per-key serialization race (the flushCell lost-write), the read-state floor gate, and the TTL-edge timing; the Cassandra ITs pin the image above the mode's version floor. The Cassandra design doc is made self-consistent for the full fence — including why the consumer generation cannot replace the offset as the fence token; persistence.md and the kafka design doc get matching updates.

[tobiajo]

Liveness gap: a tombstoned key self-fences in the CAS replay window

The replay-window fix needs the recovered offset X to seed the buffer's high-water. A tombstone doesn't give one — decode reads null value back as None, and Persistence.read only initPersisteds a Some — so the buffer starts empty, SnapshotFold's record.offset > snapshot.offset is bypassed on None, and a flush mid-replay persists at Oᵢ < X. The IF offset <= :offset guard rejects it → SnapshotWriteConflict out of the PartitionFlow, the owner re-recovers None on restart and loops. Safety holds (X never regresses); liveness only.

Confirmed with a TestControl repro extending SnapshotReplayFencingSpec (branch claude/tombstone-replay-liveness-s2cy1y, b1eba24): the same flush-during-replay that passes for a live snapshot self-fences for a tombstone; a reaped-tombstone control pins the cause to the lingering offset, not the None recovery. One correction — the delete path is shadowed (after None recovery nothing is persisted, so the tick-delete goes out persist=false and never hits the store); the persist path is the only one that fires.

Cassandra.tla (#835) hides this: OwnerRecover/Handover set recoveredAt = store.offset unconditionally, so a Tomb(o)-recovered owner already "knows" X. Giving a tombstone recovery no floor should make RefLive fail, like cassandra_replay_fixoff. A fix would span the stack — the model in #835 and the recovery code here.

[tobiajo]

The Cassandra part that initially looked trivial with lightweight transactions turned out to have many pitfalls. What makes it harder and a fix much more invasive is the lost offset when deleting. There are possible workarounds, but not without changing the APIs and likely also having an inner ADT representing snapshot/deleted with offset/null. Different paths for persist and delete also make it more difficult.

I'm starting to consider less safety as an alternative and skip asserting offset on deletes. This is starting to spiral out of control with all the invasive changes. Maybe better to wait for https://cwiki.apache.org/confluence/display/KAFKA/KIP-939%3A+Support+Participation+in+2PC and in the meantime compare-and-set (CAS) only for persist, or simply hold back.