2026-06-02. Three independent read-only red-team Plan agents attacked the design. Headline: the SHIPPED,
COMMITTED CommitRank data-loss fix (cf1f80c) is INCOMPLETE — it has multiple residual data-loss holes. The
50/50 soak + TLA that "verified" it passed only because they didn't exercise the archive-rebuild path, cross-
restart, increment-mixing, or the idempotent-arm race. This vindicates the multi-agent red-team.
reconcile_lww (recovery.rs:253) is the ONLY
generation-ordered consumer. redo_phase (:756), IncrementalRecovery (:932), rebuild_from_wal_segments
(:1443, used by the char recover_from_archives mmap_ctor.rs:1138) replay in raw LSN/physical order,
treating CommitRank as a no-op. $\Rightarrow$ the s019 loss recurs on the archive-rebuild + incremental + recovery-manager
paths. (Design §3.8 said "REC-B must reuse the reconcile"; never wired.)version) is NON-DURABLE and resets to 0 every enable_lockfree
(lockfree_cas.rs:149), while LSNs are globally durable-monotone (writer.rs:135). $\Rightarrow$ cross-restart
generation collision: S1 insert+remove (no checkpoint) → reopen (root v0) → S2 insert@gen1 → crash → reconcile
sorts the S1 remove@gen2 AFTER the S2 insert@gen1 → acked S2 insert lost. Defeats EVEN the fixed
reconcile_lww across a restart. The §3.6 monotonicity holds only within ONE root lifetime.try_increment_cas_durable is rank-FREE (:1492, by design F-3) → generation_of=lsn (large)
$\Rightarrow$ a ranked insert/upsert of the same key (gen=root-version, small) sorts BEFORE a later increment regardless
of real commit order $\Rightarrow$ value corruption (upsert(100) then increment(+1) replays as 101 $\ne$ visible 100). The
commutative-sum argument holds ONLY among increments; ANY ranked op of the same key inverts. (= red-team #3's F3.)reconcile_lww ignores the tx state machine. It expands BatchInsert/BatchIncrement
unconditionally (:343-355), ignoring BeginTx/CommitTx/AbortTx (:356-370), so an aborted/crash-incomplete
document-tx's ops are REPLAYED by the ctor path but DISCARDED by redo_phase (gates on CommitTx) $\Rightarrow$ two paths,
two recovered states; resurrection of uncommitted data on the ctor path. (Masked today only because overlay mode
rejects commit_document; OwnedTree mode uses it + opens via the same ctor → reconcile_lww.)AlreadyExists/AlreadyAbsent arms read generation from a LIVE root re-walk
(lockfree_cas.rs:383,567: lockfree_root.load().version()), NOT the published leaf — the §3.6 stale-read
hazard the design warned against. A no-op can be stamped with a generation HIGHER than a genuine earlier remove
→ resurrection (narrow race).append_commit_rank failure → unranked durable record
(generation_of=lsn); benign in isolation, loses in conjunction with 2/3.SOUND (verified): the winning arms of insert/remove/insert_with_value/upsert rank with the ROOT generation from
the exact published root (:346,532,1660,1758) — single-root-lifetime correct; the §3.6 leaf-vs-root tie is
correctly avoided in the winning arms.
compare_and_swap/get_or_insert phantom = the same class. Ship C1′: R-1 (read-before-append: decide
resident/match BEFORE appending; the cas(Some,absent) branch never appends) + R-2 (rank a bailed orphan with the
read-snapshot root generation g_read, strictly < any superseder's generation). Lemma proven strict+total
with R-1. Self-red-teamed 6 ways (two-bailers race, remove-superseder, IoError) — handled. Rejected C2 (Order-A
violation), C3 (redundant). Re-proof: NoPhantomCasWrite TLA + negative control + loom + proptest. BUT C1′'s
R-2 generation is also a root-version → it inherits hole A.2 (non-durable, cross-restart).
checkpoint() is NOT flipped (mod.rs:1283 captures the OWNED tree + next_lsn reclaim).
$\Rightarrow$ enabling overlay-write-mode (the kill-switch, or F5) WITHOUT flipping the checkpoint (F3) = #41 loss. F3 is a
hard prerequisite for F5; the OverlayWriteMode kill-switch is currently UNSAFE until F3.IoError (liveness, no loss)."generation = per-lifetime root version" is fundamentally wrong as a durable global replay-ordering key. It is
(a) non-durable + resets to 0 per enable_lockfree (A.2), (b) a different number-domain from the LSN fallback used
for unranked records (A.3, A.6), (c) honored by only 1 of 4 recovery paths (A.1). The CommitRank mechanism needs a
PRINCIPLED REDESIGN, not a patch:
reconcile_lww, or wire the generation into
redo_phase/IncrementalRecovery/rebuild_from_wal_segments) — A.1.reconcile_lww must honor the tx state machine (A.4) (= the tx-i follow-on, now mandatory not optional).f0-hack-fixes.md).cf1f80c's CommitRank fix is a PARTIAL fix (better than nothing — closes the single-
session reconcile_lww path — but with the residual holes above); the flip must NOT proceed. db7cb2d+cf1f80c
remain committed; the F0 hacks remain uncommitted/untouched.Can you improve this documentation?Edit on GitHub
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |