Repo: /home/dylon/Workspace/f1r3fly.io/libdictenstein · 2026-06-06 · supersedes V8
(tool-results/toolu_01GKFczksRv4QueaqK35mXKS.json) per the owner's
$plan \to red-team \to refine \to repeat-until-converge \to final-red-team$ instruction.
This document records red-team round 1 (4 adversarial agents) and the V8→V9 refinements that
answer every finding. The headline change: V8's carve-out category 2 ("multi-key fold into ONE
BatchInsert + ONE generation") is REFUTED and replaced by the project's own already-converged
design (docs/design/f0-hack-fixes.md, 2026-06-02) — N per-op Order-A records reusing proven
primitives — plus a minimal new piece for merge_* (a per-key CAS-retry-loop over the existing,
already-phantom-safe compare_and_swap_cas_durable primitive).
| # | Target | Verdict | Severity |
|---|---|---|---|
| A1 | increment trait removal (cat 1) | SAFE — zero generic/dyn/Shared/downstream callers of .increment(); ARTrie is intentionally not object-safe (artrie_trait.rs:717); fetch_add is inherent-only; sibling uses only ARTrie::create | framing fixes only |
| A2 | multi-key overlay fold (cat 2) | REFUTED — 3 BLOCKERS — BatchInsert can't encode removals/increments (resurrects deleted terms on reopen); one generation for N terms is outside the TLA envelope (GAP_LEDGER #88; CommitRank carries ONE term); merge-via-Upsert drops concurrent writes. Contradicts f0-hack-fixes.md §1.1. | BLOCKER |
| A3 | F4 lock collapse (deadlock + audit) | SOUND — graph $CK\to OR$, $CK\to EC$, $OR\to EC$, EC leaf = DAG, acyclic; CK at exactly 2 sites, no reentrancy; 8-field audit COMPLETE (per-variant union: byte=5, char=7) | 2 gaps (below) |
| A4 | F2 activation + triage | PARTLY REFUTED — real feature-on failures = 124, not 246; $\ge$24 orphans outside the 5 buckets, incl. a real semantic bug (insert_with_value insert-once vs upsert); get() confirmed trait-free | BLOCKER (orphans) |
Full agent transcripts: this session's tool results (agents a4b54fb06…, a6b9ac561…, a8bab96b4…,
a1aa89e89…). Empirical artifacts under docs/benchmarks/redteam-f2-*.txt.
The working tree (indexed 2026-06-06) is far ahead of f0-hack-fixes.md (2026-06-02). Already
present and proven:
compare_and_swap_cas_durable_default (overlay/durable_write.rs:461-529) — and its
append-before-failed-CAS phantom hole is ALREADY closed: mismatch $\Rightarrow$ Ok(false) no WAL
(:495-498); match $\Rightarrow$ append Upsert{new} durable $\Rightarrow$ publish with per-iteration expected-recheck
$\Rightarrow$ on recheck-miss mark_committed_burned(lsn) (NEVER ranks) (:524-527). Unranked records are
dropped on Overlay reopen (recovery.rs:332 RankRegime::Overlay => continue, per-segment at
:265-284). "burn = unranked = dropped" is the mechanism that makes conditional/recomputed value
writes phantom-safe.get_or_insert_durable_default (durable_write.rs:537) — atomic read-your-write.remove_cas_durable, upsert_cas_durable_default, insert_cas_durable,
insert_cas_with_value_durable_default, try_increment_cas_durable — all proven primitives.LockFreeOverlayDurableReplay.tla(+_Unsafe), LockFreeOverlayRemoveCas.tla(+_Unsafe),
OverlayEvictionCas.tla(+_Unsafe), LockFreeCounterMergeAtomicity.tla, LockFreeIndexedOverlay*.$\Rightarrow$ C2 is mostly "wire the already-built primitives into the rejecting call sites," not "design a new
batch protocol."
increment/fetch_add compile-time specialization (A1: SAFE)Refinements from A1:
increment/fetch_add ALREADY exist on the generic `impl<V: DictionaryValue + Serialize
blocks (charatomic_ops.rs:41/:274; byte:35/increment_bytes:53/:321`).PersistentARTrieChar::<String>::increment
is a compile error, not a runtime reject), bound the inherent methods to a sealed Counter marker
trait (impl'd only for the counter value types), i.e. move them to impl<V: Counter, S> …. This is
cleaner than a single monomorph because callers use multiple counter types (A1: char counter tests
use PersistentARTrieChar<i64>; byte uses PersistentARTrie<i64>; the lock-free seam is u64
internally). Counter must cover both i64 and u64 (verify the exact set during impl).fn increment in the ARTrie trait (artrie_trait.rs:532, per "never delete to
disable"); comment-out the 3 trait-impl delegations (byte shared_trait_impl.rs:232, char
mod.rs:1463, vocab reject mod.rs:708); add the Counter bound to the inherent blocks. Keep the
ARTrie trait itself (sibling depends on ARTrie::create)..increment() from the Shared* handles — state that,
don't claim "no loss."compile_fail doc-test that PersistentARTrieChar::<String>::increment does not exist.Reversibility: signature-reversible; coverage-lossy (retyped increment tests). MINOR.
Replace V8's fold entirely. The converged design = f0-hack-fixes.md (N per-op Order-A records,
reusing proven primitives) + the insert_with_value upsert fix + a minimal merge primitive. No
BatchInsert fold, no batch-rank codec variant, no "one generation for N", zero on-disk/codec change.
insert_with_value upsert bug (A4 BLOCKER) — fix FIRSTOwned insert_with_value overwrites on duplicate (mutation_core.rs:151-154: already-final $\Rightarrow$
node.value = Some(value); Ok(false)), matching upsert, the map laws (dictionary_law_correspondence),
and test_value_update_persistence. The overlay routes to insert_cas_with_value_durable_default
(insert-once) in BOTH char (mutation_api.rs:72) and byte (mutation_api.rs:62) $\Rightarrow$ stale values via
get_value() $\Rightarrow$ owned↔overlay divergence. Fix: route overlay insert_with_value →
upsert_cas_durable_default (overwrite), both variants. Correct the dedicated test
(persistent_arbitrary_v_overlay.rs:110-119) which currently asserts the buggy insert-once contract.
insert_batch + insert_batch_bytes (currently has NO overlay route — latent F5 data-loss gap) →
loop per entry: membership $\Rightarrow$ insert_cas_durable; valued $\Rightarrow$ upsert_cas_durable (match §2.0). Count
Ok(true); first Err stops and returns the count so far (the failed entry's record is durable, replays).
Per-op durable, not batch-atomic (matches owned insert_batch). _chars/_sorted/_grouped inherit.
Replace the route_overlay() reject (byte document_tx.rs:189/193, char :326/339): apply SETs via
upsert_cas_durable/insert_cas_durable, increments via try_increment_cas_durable (counter-monomorph
only, §1); DROP BeginTx/CommitTx/sync on the overlay arm (skip the orphan BeginTx in begin_document
under route_overlay()); reject a negative aggregated increment delta (don't silently owned-write).
Per-op durable, not all-or-nothing — matches the owned path's actual recovery semantics
(reconcile_lww ignores tx brackets, f0-hack-fixes.md §1.2). Document as a named residual. (tx-i =
all-or-nothing via a reconcile tx-bracket = a separate, pre-existing recovery-path-convergence task,
not Phase-F scope — surface to owner, do not silently defer.)
The atomic primitive get_or_insert_durable_default already exists. Verify the route
(lockfree_value_route.rs) calls it (not the racy 2-step insert + get_lockfree); rewrite if stale.
Implemented + phantom-safe (§0.1). Action: confirm the burned-record drop is covered by
LockFreeOverlayDurableReplay.tla; add an explicit LockFreeOverlayValueCas.tla +
NoPhantomConditionalWrite + _Unsafe.cfg (negative control: NOT burning $\Rightarrow$ phantom write appears) so
CAS+merge are formally pinned (owner: "formal verification of Phase F + G5"; no-deferral).
The minimal new piece. A merge value is state-dependent (merge_fn(self_val, other_val)), the
same hazard class as CAS. Resolve by reusing the proven CAS primitive:
fn merge_value_cas_durable(&self, key, other_val, merge_fn) -> Result<()> {
loop { // obstruction-free; bounded-retry → brief lock fallback
let self_val = self.value_read_faulting(key)?; // re-read each iteration (overlay, NOT empty owned)
let merged = merge_fn(self_val.as_ref(), &other_val);
match self.compare_and_swap_cas_durable_default(key, /*expected=*/self_val, /*new=*/merged)? {
true => return Ok(()), // won: ranked + marked by the CAS primitive
false => continue, // concurrent change: CAS burned an unranked record → retry
}
}
}
value_read_faulting (overlay) fixes the "reads empty owned tree" bug
(merge_api.rs:34). No new ValueWriteMode — the re-resolve lives in the OUTER loop; the inner
CAS already re-checks expected against the fresh root and burns on miss.merge_replace = merge_fn = |_self, other| other.clone() (last-writer); merge_from = the custom
fn; parallel variants resolve merge_fn in parallel (rayon, disjoint key partitions — A2 TASK H:
resolve-only parallelism confirmed race-free) then funnel each key through merge_value_cas_durable
(per-key atomic; not batch-atomic, matches owned).Upsert is unranked $\Rightarrow$ dropped on Overlay reopen $\Rightarrow$ no phantom
merge. The winning attempt is ranked $\Rightarrow$ survives. Same envelope as CAS (§2.4 TLA covers it).&mut self for now (works: &mut self can call the &self-CAS internally) — A4's
"C2 depends on F4" is over-stated; routing the body needs no &self conversion. F4 later collapses
the signature.doc-tx/batch/merge on the overlay are per-op durable, not all-or-nothing crash-atomic — because
that is exactly what the owned path delivers (reconcile_lww ignores tx brackets). This achieves the
Phase-F goal (overlay $\equiv$ owned). All-or-nothing (tx-i) would make the overlay better than owned and is a
separate task. Surface to owner; do not bury.
get()/try_get() (A4: trait-free, confirmed)get/try_get are inherent-only (NOT on ARTrie; the trait has get_value, artrie_trait.rs:325).
They already return None under route_overlay(). Final contract: #[deprecated(note=…use get_value())],
keep returning None (graceful). get_value() (owned clone, overlay-routed) is the canonical reader. No
trait-surface change.
Real: 2618 run, 2494 passed, 124 failed, 3 skipped (build compiles clean feature-on). The 5 V8 buckets
miss $\ge$24 orphans. Six remediation categories:
Counter handles (§1).InvalidOperation→success).get()→None (part of 38) → use get_value().walk_map,
reopen-InvalidMagic corruption-injection, walk-under-eviction, dirty/epoch) → these inspect the
OWNED rep, which is empty post-flip. Pin to OverlayWriteMode::OwnedTree (construct un-flipped) —
they are owned-tree white-box tests and must say so.
Plus the two real bugs (NOT contract-flips): §2.0 insert_with_value→upsert (fixes
dictionary_law_correspondence, test_value_update_persistence); and root-cause
test_mixed_value_recovery (membership insert() + valued insert_with_value() on a non-()
V — likely the same insert-once vs upsert divergence; verify).Honesty (A4 TASK F): most of the 124 are contract-flip rewrites (asserting the carved-out
behavior), not "new functionality proven." State as "N tests migrated to the F2 contract," not "N now
pass." Genuinely-new arbitrary-V coverage = the dedicated persistent_arbitrary_v_overlay.rs suite.
Default-flip (A4 TASK E): one line, BUT adding overlay-arbitrary-v to default also pulls
persistent-artrie (→ memmap2/dashmap/lru/sysinfo/…) into every default build — a bigger blast radius
than "feature into default set." This is the F2-default-on irreversible flip (owner GO #1).
Graph $CK\to OR$, $CK\to EC$, $OR\to EC$, EC leaf — acyclic, CK at exactly 2 sites, no reentrancy. Field audit
COMPLETE as a per-variant union: byte = 5 (root(OR), eviction_coordinator(EC),
overlay_write_mode(AtomicU8), durability_policy, dirty_prefixes); char = 7 (root(OR),
eviction_coordinator(EC), overlay_write_mode, durability_policy, memory_monitor,
checkpoint_manager, group_commit(cfg)). Document per-variant (wrapping dirty_prefixes on char or
memory_monitor on byte = compile error).
GAP 1 (BLOCKER-class impl constraint): the eviction disable rewrite MUST use a statement-
temporary so the EC guard drops BEFORE shutdown().join():
let coord = self.eviction_coordinator.lock().take(); /* guard dropped */ if let Some(c)=coord { c.shutdown(); }.
Binding the guard across the join reintroduces the production deadlock (disable holds EC + joins; worker
holds OR + waits EC). The current code is safe only by the outer-RwLock temporary; the Mutex<Option<Arc>>
wrap does NOT auto-preserve it.
GAP 2 (MAJOR): the 3 sister subsystems also join() a thread in Drop; their disable_*
(memory_monitor observability.rs:224, group_commit :154, epoch_checkpointing :103) need the
same drop-before-join temporary. Critical for memory_monitor: its user-supplied callback can
re-enter the trie (force_eviction → OR/EC) $\Rightarrow$ holding the field mutex across the join is a real
cross-subsystem deadlock.
Plus the existing F4 mechanics (V8 §6): &mut self→&self ripple, ~266 .read()/.write() shared-handle
sites (mechanical; check the liblevenshtein sibling), delete downgrade, ctor &mut self.root fixes, C2
debug-assert fix. IRREVERSIBLE — owner GO #2. No new unsafe.
load_root_immutable (arena→OverlayNode) — generic over V from the start; both-loaders
correspondence proptest over every on-disk format BEFORE F7 switches reopen to it. Reversible (flag).compact carve-out (byte-only); CK-gate compact
(closes R15: compact renames the file but isn't CK-gated today); watermark-bounded WAL retain +
synced_frontier ≤ watermark assert + post-rename-retain test. Reversible until wired. Resolves F2
bucket 4.load_root_immutable; lock graph CK>OR>EC→CK>EC.
IRREVERSIBLE — owner GO #3 FINAL. Per-sub-step green.| Obligation | Model | New? | Phase |
|---|---|---|---|
| conditional/recomputed value write (CAS + merge) phantom-safety | LockFreeOverlayValueCas.tla + NoPhantomConditionalWrite + _Unsafe (don't-burn $\Rightarrow$ phantom) | NEW | §2.4/2.5 |
| per-op batch/doc-tx replay ordering | LockFreeOverlayDurableReplay.tla (existing) + a deterministic batch_overlay_replay_orders_by_commit_rank regression | existing | §2.1/2.2 |
| lock-collapse no-lost-write (no writer-exclusion) | LockFreeDurableCheckpoint.tla (existing; already no-writer-exclusion) — re-run as regression | existing | F4 |
| concurrent-checkpoint serialization (CK) | ConcurrentCheckpointSerialization.tla (committed F3) — re-run + real-disk 2-checkpoint+reopen test | existing | F4 |
| eviction CK>OR>EC deadlock-freedom | loom checkpoint(+eviction) ‖ disable_eviction ‖ writer + the drop-before-join discipline (§5) | NEW loom | F4 |
| compaction WAL bound | synced_frontier ≤ watermark assert + post-rename-retain disk test | existing reasoning | F6 |
Each phase gate: full suite green + scripts/verify-formal-correspondence.sh exit 0 (SANY + TLC +
_Unsafe negative controls MUST fire) + verify-unsafe-boundary-inventory.sh exit 0 + 0 new unsafe.
TLC under systemd-run … MemoryMax; loom $\le$3 threads/2 keys; disk tests real-disk (never tmpfs).
insert_with_value→upsert bug fix (§2.0) — cheapest, unblocks F2 correspondence. Reversible.Counter-bound specialization (§1). Reversible (signature).&mut self (NOT F4-dependent — A4 over-stated).get()/try_get() (§3). Reversible.Each irreversible flip = isolated commit behind its own owner GO, after a soak. C1 before F4 is
defensible (specialize before the collapse moves methods) but the V8 "&mut→&self ripple" justification is
imprecise (increment is already &self; the ripple is F4's). The only true cross-dep is F2 bucket 4 $\vdash$
F6.
LockFreeOverlayDurableReplay.tla actually prove "an unranked durable record is dropped on
Overlay reopen" generally (so it subsumes CAS-burn + merge-burn), or is the new LockFreeOverlayValueCas
strictly required? Verify against the .tla.merge_value_cas_durable = loop{read;merge;cas} genuinely lost-write-free AND livelock-bounded?
Find a trace where a merge is lost or never terminates. Confirm merge_replace/parallel funnel reuse it
safely; confirm self-read uses value_read_faulting not get.insert_with_value→upsert_cas_durable_default correct for empty-string ""
and for the counter monomorph (does upsert vs insert-once matter for try_increment paths)? Verify
no regression to the empty-string-value support or the increment path.Counter sealed-trait bound cover exactly the value types the increment tests
instantiate (i64 AND u64, char AND byte)? Enumerate every .increment(/.fetch_add( receiver type.disable_* +
eviction use a statement-temporary; find any 4th join()-under-lock site.insert_batch_bytes missing overlay route — confirm it currently silently writes owned under the
flip (data-loss), and that the §2.1 route closes it.Round 2 (agents ae3431df2… merge/CAS, a6d9d87ee… wiring, a58059086… Counter/F4) found NO
fundamental refutation — the V9 core designs are sound. The deltas below close the completeness/precision
gaps + one genuinely-new concern (merge termination). Convergence trajectory: round 1 = wrong approach
(C2 fold); round 2 = right approach, fix these specific sites.
Fn(&V,&V)->V; absent key inserts other WITHOUT calling
merge_fn):
let self_val = self.value_read_faulting(key)?; // Option<V>
let merged = match &self_val { Some(s) => merge_fn(s, &other_val), None => other_val.clone() };
// compare_and_swap_cas_durable_default(key, expected = self_val, new = merged)
crossbeam_utils::Backoff (spin→yield)
— the CAS primitive's OUTER gate (durable_write.rs:495) already catches most concurrent changes with
NO fsync, so backoff bounds the expensive read-consistent-then-lose-root-CAS window; (b) the whole-trie
merge_from driver takes a dedicated per-trie merge_lock: Mutex<()> (a NEW leaf lock,
independent of CK/OR/EC — merge takes no other lock under it, so no cycle) serializing merge‖merge (kills
merge-vs-merge livelock). merge‖{insert,increment,upsert,remove} stays obstruction-free but practically
terminating (those ops are quick; the CAS wins between them) — document the residual: a bulk merge under
sustained single-key external writes is obstruction-free (unrealistic workload; the system is making
progress, just this merge is slow). WAL amplification $\le$ backoff-bounded.merge_replace = direct per-key upsert_cas_durable (no read-compare needed; absent-key already
inserts other, present-key overwrites) — cheaper than the CAS loop.other's entries in parallel (read-only, race-free), collect, then apply via
the serial driver (merge_lock + per-key CAS). The funnel-through-CAS made the parallel write illusory
anyway (R2-1 TASK E); document parallel-merge applies serially under the overlay.merge_lock is a leaf acquired ONLY by merge_from/merge_replace/parallel_merge;
never held across CK/OR/EC; checkpoint (CK) snapshots the lock-free root concurrently as designed. No
interaction.Counter = {i64, u64} (empirically sufficient: lib + all 5 inherent-increment test crates compile
with the bound). byte counter = i64, char increment callers use BOTH <i64> and <u64> → Counter
must cover both.pub fn increment(&self,…) where V: Counter, same for
fetch_add, byte increment_bytes) — do NOT add Counter to the whole impl block:
try_increment_impl_no_wal (char atomic_ops.rs:120) stays on DictionaryValue (arbitrary-V recovery
caller mmap_ctor.rs:1062, BatchIncrement mutation_core.rs:335).tests/persistent_artrie_recovery_tests.rs:2537/2541/2545 (SharedCharTrie<i64> → retype to inherent
PersistentARTrieChar<i64>); tests/vocab_trait_honesty.rs:195-208 (asserts the trait-level
increment-reject which ceases to exist → rewrite to assert vocab has no .increment() /
inherent-only). Round-1 A1's "zero Shared callers" is REFUTED.insert_batch_entry_overlay's valued arm (persistent_artrie/mutation_api.rs)
— it calls insert_cas_with_value_durable_default (insert-once) DIRECTLY, bypassing insert_with_value,
so fixing only insert_with_value leaves byte batch insert-once while byte single becomes upsert
(silent divergence). Change its valued arm → upsert_cas_durable_default. (char batch delegates to
self.insert_with_value so it auto-inherits the fix.) The "insert_batch_bytes has no overlay route"
premise is STALE (both already routed — tree ahead of f0-hack-fixes); the real issue is the valued-arm
insert-once.DocumentTransaction has NO increments field (increments
are folded into shadow_terms as absolute SETs at buffer-time) → byte overlay arm = upsert(shadow_terms)
ONLY (NEVER route through try_increment_cas_durable — would double-count). char = upsert(shadow_terms)
try_increment_cas_durable(aggregated_increments) with negative-aggregate reject. Reuse char's
existing aggregate/overflow preflight (document_tx.rs:412-423).get_or_insert_durable_default); only the stale byte get_or_insert_bytes docstring
(atomic_ops.rs:338-342) needs correction.persistent_arbitrary_v_overlay.rs:110-114 → flip to
assert overwrite (value becomes the 2nd insert).let x = self.field.lock().take(); /*guard drops*/ if let Some(c)=x { c.shutdown(); }): (1) disable_eviction [byte+char], (2) disable_memory_monitor
[char], (3) disable_group_commit [char], (4) disable_epoch_checkpointing [char], (5) close() /
Drop [byte dict_impl.rs:536-557, char mod.rs:567-577] — joins eviction thread by a bare &self
field read, runs on EVERY teardown → MUST get the temporary (the missed site). (6) compact
wal_writer=None [byte compaction_impl.rs:295/309] — WAL-sync join, no trie re-entry → benign,
hygiene note only (don't hold CK across it).overlay_write_mode is a plain Copy enum (NOT atomic) — wrap as an atomic-backed cell or Mutex;
byte=5/char=7 field union CONFIRMED.LockFreeOverlayValueCas.tla (+.cfg+_Unsafe.cfg) is STRICTLY required — LockFreeOverlayDurableReplay.tla
never models a durable-but-refused (burned) record. Must add: RecomputeAndAppend (read→merge→append+sync
durable, per-iteration expected), WinAndRank (expected==fresh-current → publish+rank), BurnOnLoss
(refused → durable-but-unranked), recovery ranging over durable-WAL-incl-burned with the regime-drop +
checkpoint-skip, invariants NoPhantomConditionalWrite + NoLostConditionalWrite, and _Unsafe.cfg
(don't-burn $\Rightarrow$ phantom MUST fire). Include a Checkpoint(watermark) action so burn-drop is checked via
BOTH regime AND checkpoint-skip. Covers CAS + merge. Wire into verify-formal-correspondence.sh.merge_lock leaf vs CK/OR/EC and
checkpoint; does serial-apply parallel_merge regress any correctness; is the obstruction-freedom residual
truly acceptable.insert_cas_with_value_durable_default that should be upsert (byte batch + any others); EVERY
trait/dyn/UFCS .increment()/ARTrie::increment caller (the 2 found + any others); EVERY join()
reachable from a &self/Drop/disable_* path (the 5th + any 7th).LockFreeOverlayValueCas.tla action set actually capture the
merge bounded-retry + the byte-batch-upsert + the doc-tx per-op semantics, and does _Unsafe fire.Round 3 (agents a8ae65a79… merge_lock, a3338a3f0… sweeps) found NO new data-loss; sweeps A/B CLOSED;
remaining = deadlock-discipline with known in-repo fix patterns. Trajectory: R1 wrong-approach → R2
right-approach-fix-sites → R3 fix-deadlock-discipline-sites (narrowing).
char union_with (mod.rs:1130-1132) holds other.read() + self.write() SIMULTANEOUSLY (other-then-self)
$\Rightarrow$ A.union_with(&B) ‖ B.union_with(&A) = AB/BA deadlock. Pre-existing in committed code (the reject
is inside merge_from, AFTER both locks taken); merge wiring WIDENS the held-both window to O(terms).
merge_lock does NOT fix it. FIX (the vocab pattern, already correct at persistent_vocab_artrie/mod.rs:476-483):
snapshot other fully into an owned Vec under other.read(), DROP other's guard, THEN take self's
write/merge_lock and apply. Mandate for ALL merge entry points (merge_from/merge_replace/merge_from_batched*/
parallel_merge/union_with/union_replace, byte+char). Rewrite char union_with accordingly. (byte
SharedARTrie has no union_with — char-only via union_with, plus any future byte Shared merge wrapper.)
Snapshot cost: O(other) memory — acceptable (merge is bulk/rare); for a huge other, snapshot in chunks
under repeated short read-locks (still never two OR locks at once).
merge_lock: Arc<parking_lot::Mutex<()>> — mirror checkpoint_lock EXACTLY (ships F4-ready, not a Tier-2
Mutex<Option<Arc>> wrap). Add to the F4 audit: byte=6, char=8 (the V9 §5 "complete" union must grow).CK > merge_lock > OR > EC (pre-F7) → CK > merge_lock > EC (post-F7, OR gone).
merge_lock is acquired ONLY by the merge drivers, never by any CK/OR/EC holder.merge_lock in exactly the innermost private driver
(merge_from/_with_options); public wrappers (merge_replace, merge_from_batched,
merge_from_batched_grouped) must NOT re-take it (parking_lot is non-reentrant → double-take = self-
deadlock). Audit the delegation chains.std::hint::spin_loop() + std::thread::yield_now()
(NO new crossbeam-utils dep). Obstruction-free residual vs sustained single-key external writers is
ACCEPTABLE (matches the shipped lock-free writers; system makes progress; merge_lock kills only
merge‖merge livelock). merge_replace = direct per-key upsert_cas_durable (no read-compare).other; apply serially (the parallel write was illusory).
Drop the "4-6$\times$" docstring (byte parallel_merge.rs:50).The complete drop-before-join set (statement-temporary: let x=self.field.lock().take(); /*drop guard*/ if let Some(c)=x { c.shutdown(); }):
1-2. disable_eviction [byte+char]; 3-4. close()/Drop [byte+char] (bare-read 5th site, every teardown);
5-7. char disable_{memory_monitor,group_commit,epoch_checkpointing}.
ADDED — 8. vocab disable_eviction (persistent_vocab_artrie/mod.rs:795-803) — holds self.write()
LIVE across shutdown()/join; the vocab eviction callback re-enters via trie.write() $\Rightarrow$ latent deadlock
TODAY (fix now regardless of F4; vocab is otherwise out of byte+char F4 scope).
ADDED — 9 (a CLASS). the enable_* re-arm path — enable_{memory_monitor,group_commit,epoch_checkpointing, eviction} do self.field = Some(new); if already enabled, the assignment drops the OLD Arc → its Drop
joins the old worker $\Rightarrow$ post-F4 *self.field.lock() = Some(new) joins UNDER the held guard (re-entrant
callback $\Rightarrow$ deadlock on re-arm). FIX: let old = { let mut g=self.field.lock(); g.replace(new) }; drop(old);
(take-old-then-drop-guard-then-let-old-drop). Apply to all enable_* (both variants where the field exists).
Benign (hygiene only): byte compact wal_writer=None; close() wal stop_sync.
upsert_cas_durable_default: byte mutation_api.rs:63
(insert_with_value), byte mutation_api.rs:360 (insert_batch_entry_overlay valued arm), char
mutation_api.rs:77 (insert_with_value). LEGITIMATE insert-once (do NOT change): byte
lockfree_cas.rs:1314 + char lockfree_cas.rs:1854 (the public insert-once primitive bodies), core
durable_write.rs:541 (get_or_insert). char insert_batch/insert_batch_bytes auto-inherit via
self.insert_with_value; byte batch routes through site #360; vocab has NO value-write overlay path
(warn-stubs). doc-tx forward-looking: SET arm uses upsert; byte has NO increments field.tests/persistent_artrie_recovery_tests.rs:2537/2541/2545
(SharedCharTrie<i64>→retype inherent), tests/vocab_trait_honesty.rs:203 (rewrite). Counter={i64,u64}
sufficient; all 3 impl ARTrie blocks drop increment together.Round 4 verifies V11 has converged: (T1) any OTHER pre-existing cross-instance / two-trie deadlock the
focused sweeps missed (byte/vocab merge wrappers, any op taking two tries' locks); (T2) the
snapshot-other-then-release fix is correct + complete + memory-safe for large other; (T3) the enable_*
re-arm + vocab disable_eviction fixes are correctly specified; (T4) a final no-data-loss re-confirm that
V11's refinements didn't reintroduce a hole. If round 4 is clean (only confirmations) $\Rightarrow$ CONVERGED $\Rightarrow$ one
final confirming round-5 per the owner's "red-team once more."
Round 4 (agents a1862c213… holistic-deadlock, a89093da6… fresh-skeptic) did NOT converge — it found 2
NEW blockers the merge-focused rounds missed, BOTH in F5/F7 scope. The EARLY phases (C0/C1/C2/C4/F2/F4) are
CONFIRMED converged + data-loss-sound (both agents failed to break the merge/CAS/upsert/lock-collapse core).
zipper.rs:99-118, char/byte root() mod.rs:616-631). Exercised by the FORMAL GATE
(zipper_language_correspondence.rs:522-557 in verify-formal-correspondence.sh:45; GAP_LEDGER:63). NOT
in any carve-out. F2-default-on → empty results; F7 → permanently broken + gate regression.phase-f-g5-delete-owned-tree.md §3.1/§3.4: Option A = new arena→OverlayNode parser reading EVERY legacy
on-disk format = "weeks of parser + back-compat work", and RECOMMENDS Option B (keep owned dormant +
retain kill-switch; "almost nothing owned is deletable"). F7 deletes the kill-switch in the same arc $\Rightarrow$
new single-soak parser becomes the ONLY reopen path with NO fallback $\Rightarrow$ misread any legacy format = brick.union_with mod.rs:1130-1132
(AB/BA, both modes), vocab disable_eviction mod.rs:796-800 (guard across join). Out-of-scope but real:
DynamicDawg/DynamicDawgChar union_with (same AB/BA).\Rightarrow$ introduce merge_lock AT F4 (it replaces OR-write's role); resolves the "merge_lock>OR
impossible" inconsistency. merge_lock needs a loom schedule (merge‖checkpoint‖insert/remove‖disable_evict).ln_phase (recovery.rs:768-856) HONORS tx brackets; must
prove it's unreachable on every production reopen (else overlay per-op is a real atomicity downgrade).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 |