tantaman

2026-09-21 · markdown

317 — Boundary Window Reconciliation

Status: Proposed, not started (2026-09-21). Nothing here is implemented. The measurements in §2 are real and reproducible (take_bounded_fanout::measure::depth2_exists_chain_rename). The code facts cited were checked against this tree (branch bounded-fanout, 9846363). Everything else is specification and argument, and §12 lists what is least certain.

What this is. A from-scratch answer to the limited backfill cascade (RUNAWAY-PUSH-FINDINGS §3, 316 §17.5), written without regard to what has been built for it. It changes how a limiter decides what is in its window. It keeps the bounded fan-out cut built under 316 §17.5, demoted from a correctness mechanism to an optimization (§6).

Relation to 316 §17.5. That section first sketched "change-scoped window reconciliation" in four steps, then built something smaller — the cut, with the refill left mid-push — and recorded why. Two parts of that record do not survive §2. Its cost argument (a reconcile phase threaded through fourteen operators and the pipeline driver) is upstream's cost and not this engine's (§5.3). And its "Still open" claim that a nested EXISTS cascade "is limited to one child's rows within one partition" is wrong for the outer window. This doc is the four-step sketch made concrete; "retain the old window" is answered by member keys (§5.1).

History. The first design of Zero's Take kept every member of the window (Matt, 2026-09-21). The operator that shipped, and that this engine ported, keeps a count and a bound. This design goes back to members.


1. One defect, not six

Every fault found in this area has the same shape.

# Symptom Where What went wrong
1 The cascade: limit removes each refill with a parent that is removed next findings §3, 316 §3.5 The refill read a parent that was still owed the delta
2 Exists cache poisoning: a doomed row kept past the cut; on main, a Remove of a row the view never held 039274b One refill scan met same-key parents in different states — it starts At the bound row, which may still be owed the delta — and the first one answered for the rest
3 Upstream's [i2, i9] for [i2, i3] rocicorp/mono#6617 tip, §17.5 obligation 4 A window left short by a deferred refill admitted an add as if its input were exhausted
4 Upstream's overlay loses its bound mid-push §17.5 obligation 1 The overlay reads the live bound, which disappears at the first in-window remove
5 Depth 2, removes, inner order aligned with the window: 2N changes, O(N²) when flipped §2 The outer refill admitted roots doomed by an inner fan-out that was still open
6 Depth 2, adds, inner order opposed to the window: 2N changes §2 Nothing was misread. Every delivery legitimately displaced the bound, because deliveries did not arrive in the window's order

The common cause: a limiter decides which rows are in its window from a read — or from an arrival order — taken while the graph is mid-transition. The cut, the late cut, the short-window rule, the cache guard, upstream's gate and upstream's pending rule each make one more of those decisions come out right. None of them removes the decisions. Row 6 shows the limit of that approach: no rule about reads can fix it, because no read is wrong.

2. Measurements: the cut is a depth-1 mechanism

issue.whereExists(comment, c => c.whereExists(author, name = 'bot')).orderBy(id).limit(10). One comment per issue; every doomed comment is by author 1. Author 1 is renamed away and then back. aligned means comment ids run with issue ids; opposed reverses the comment → issue map, so the inner fan-out (which runs in comment order) delivers against the window's order. N = 2,000, release, memory leaf. A many-to-many EXISTS through a junction table is this shape (316 §1.2's R2), so it is not exotic.

Changes that reach the sink (a minimal answer is 10 to 20):

Cell Rindle bounded-fanout Upstream grgbkr/multi-phase-push (1d041c64c)
away, aligned 3,990 (26 ms) 10 (11 ms)
away, aligned, both joins flipped 3,990 (3.2 s; 48.7 s at N = 8k) 10 (0.58 s)
away, opposed 10 10
back, aligned 10 10
back, opposed 3,990 (19 ms) 3,990 (41 ms)
back, opposed, both joins flipped 3,990 (1.6 s; 25.8 s at N = 8k) 3,990 (38.6 s)

Rindle: cargo test --release -p rindle --features testkit --test it -- take_bounded_fanout::measure::depth2_exists_chain_rename --ignored --nocapture. Upstream: the same probe ported to vitest and run at the PR's tip.

Three readings.

  1. Rindle's change counts are identical with RINDLE_FANOUT_CUT=off. The join that fans out (comment ⋈ author) has no governing Take: first_take_downstream gives up at a JoinChild port (graph.rs:3685). Its pre-change band has no upper edge, so the outer Take's mid-push refill admits an issue whose comment has not been delivered yet.
  2. The last hop is governed, and its cut works when the order cooperates. In back, aligned the outer hop drops 1,990 parents at the cut and the sink sees 10 changes. In both cascading cells it drops 0, because every root is inside the window at the moment its delivery lands — in one cell because the refill just pulled it in on stale inner state, in the other because it belongs there for the moment.
  3. Deferring the refill fixes one cell, not both. Upstream's boundary refill sees post-change state at every depth, so away, aligned is 10. back, opposed is 3,990 in both engines: a deferred refill does nothing for displacement.

3. Why depth 1 works, and why that does not extend

The bounded fan-out rests on two facts about order:

  1. The fan-out runs in the window's order, so the first limit adds to arrive are final and the late cut can end the fan-out.
  2. The fan-out's pre-change band has an upper edge at the cut, so a refill — which starts at the live bound, at or past the cut — meets only post-change rows.

Both hold because the join that fans out is the one the Take governs: its parent fetch is sorted in the Take's order, and it can read the Take's bound. One level down neither holds. The join that fans out is ordered by its own parent table and cannot see the bound. Row 5 of §1 is fact 2 failing; row 6 is fact 1 failing.

Pushing the cut down — an inner parent is owed the delta iff one of its roots is within the captured cut — is self-consistent for removes: the owed set is fixed at capture, the refill admits only roots past the cut, so nothing becomes newly owed. It costs an ancestor probe per inner row, and it needs a second allow-list walk, upward through Cap, FlippedJoin and the OR fans, re-argued per depth. It cannot fix row 6: an opposed-order add is within the bound when it arrives.

The other route needs no argument per depth. Once the source write is committed, no fan-out is in flight at any level and no overlay is live. A fetch made then is just a fetch.

4. Principle

Pushes keep held rows exact. A fetch decides membership, once, at the push boundary.

Pushes and fetches are good at different jobs. A push carries a delta to a row that something holds state for. A fetch answers "which limit rows", and it is trustworthy only when nothing is in flight — which, at arbitrary depth, is the boundary and nowhere else.

Terms used below:

Term Meaning
limiter Take or Cap
window One partition of a limiter
member A row the limiter has emitted an Add for and not yet a Remove. Known by key (§5.1)
held A row some limiter counts as a member, or the view contains
dirty A window whose members may differ from the first limit rows of its input, post-change
boundary The point in try_source_push after the source has pushed to every connection and committed its write
published bound What a window reports to a governed join's cut (Take::window_at). It never sorts before a member

5. Design

5.1 A limiter knows its members

Cap already does: StorageValue::Cap { size, pks }. Take keeps StorageValue::Take { size, bound } (storage.rs:67) and infers membership as "sorts at or before the bound, and passes upstream right now". That inference is what fails mid-push: upstream is in transition, so "passes right now" is not "was emitted". Fault 2's phantom Remove and #594 — a window counting rows the consumer was never sent — are both the inference diverging from the emission log.

Take gains members: the sort keys of its members, in order. Take requires a sort that includes the primary key, so a sort key identifies a row. With it:

  • Membership is exact. A Remove or Child for a non-member is dropped, whatever its position.
  • An Add can be absorbed — noted, not emitted — because the limiter can later tell a row it has emitted from one it has not. Without identity only the refill can be deferred, which is as far as upstream's branch goes and why row 6 survives there.
  • members changes only together with an emitted Add or Remove. The window and the consumer cannot disagree.

At rest, size == members.len() and bound == members.last(). During a push size and bound are not written (§5.2); they describe the last reconciled window, and they are what the cut reads.

5.2 Push rules: bookkeeping, no fetches

A change for a never-hydrated partition is dropped, as today (take.rs:461, cap.rs:218). Otherwise, for a change about row r:

Change Condition Action
Child r is a member Forward
Child otherwise Drop
Remove r is a member Remove r from members, then forward. Mark dirty
Remove r was absorbed in this push Forget it
Remove otherwise Drop
Add r could enter: it sorts at or before the published bound, or the window was short at its last reconcile Absorb: record the key (§5.4). Mark dirty. Emit nothing
Add otherwise Drop, and evict upstream child state as today (evict_upstream_if_full)
Edit old row is a member Update its key, then forward. If the key moved, mark dirty and raise the published bound to it if it now sorts later
Edit old row is not a member, new row could enter Absorb the new key. Mark dirty
Edit otherwise Drop

Two rules carry the design:

  • A member's Remove is forwarded at once. Its node is in hand and agrees, through the overlays, with what the consumer holds. At the boundary the row may no longer pass — or exist — so it could not be fetched.
  • An Add is never emitted during a push. Whether r belongs in the window depends on everything else the source change does, at every depth, in an order the limiter does not control.

"Mark dirty" appends (limiter, window key) to a worklist on the Graph, once.

5.3 The boundary is one call site

try_source_push already has an outer boundary: scope_publish_all, where design 316 publishes the scope directories the push touched (graph.rs:4121). The drain goes between s.try_push(...) returning Ok and that call: the write is committed, the source overlay is cleared (source_common.rs:1225), and nothing is in flight. It runs before the publish because a reconcile emits ordinary pushes, whose parent-port arms maintain the directory.

Upstream threads reconcile() through every operator because its operators know only their input and output. Here the graph is an arena: a dirty window is a NodeId and a key, and the drain is a loop in one function.

  • Order: upstream first. A reconcile fetches through every limiter upstream of it, so those must already be reconciled. A reconcile's own emissions flow toward the sink and can only dirty limiters downstream of it. So the drain takes dirty windows in topological order, re-reading the worklist as it grows, and each window reconciles once. (Operators are built after their inputs, so ascending NodeId is expected to be such an order — S1 checks it.)
  • Split edits. A split Edit pushes and writes each half separately (source_common.rs:1417). Windows stay dirty across both halves and reconcile once.
  • Failure. If the push parked a runtime error, the drain is skipped; the host discards the engine, as today. The reconcile scan carries the §6.6 deadline checkpoint that the backfill scan carries now.
  • Scope. One source change. Draining once per transaction would coalesce more and is a separate decision (§12).

5.4 Reconcile

Let start be the earliest position at which the window's membership may differ: the smallest absorbed key, the new position of a member whose key moved, or — if there is only a deficit — just past the published bound. Let k be the number of members sorting before start. Then

W' = (the k members before start)  ∪  (the first  limit − k  rows of  input.fetch(start: At(start)))

for m in members ∖ W':  members −= m;  push Remove(m)      // m still passes: fetch its node by key
for w in W' ∖ members:  members += w;  push Add(w)         // node from the scan
size = |members|;  bound = last(members);  clear absorbed, dirty, provisional bound

Removes go first so the output never exceeds limit. members is updated before each push, so a reentrant fetch through the limiter during its own emission sees exactly what has been emitted. That replaces row_hidden_from_fetch.

With nothing absorbed this is a deferred refill: start is past the bound, every member is retained, and the scan fetches the deficit. A window that was already short and absorbed nothing has nothing past its bound and fetches nothing — the short-window rule, surviving as a shortcut and no longer as an invariant others lean on.

The exact shortcut. The hot path is one row: an insert at the top of a list. If every absorbed key is still held (at most limit of them, none discarded) and no provisional bound was published (§6.3), the candidates are fully known and W' = first limit of (members ∪ absorbed), computed from keys, plus a deficit fetch if that is still short and the window was not exhausted. Each entrant and each displaced member then costs one fetch by key — for a top-of-list insert two, against today's two-row reverse probe. Anything else takes the scan, which is bounded by limit rows and happens only for a push that delivered at least a window's worth of adds.

5.5 Fetch through a limiter answers from members

Both regimes of Take::fetch (take.rs:290) stream the input and keep a row iff it is a member, in place of the comparison against the partition's bound. MAX_BOUND stays as the scan stop for the unconstrained regime. A nested window read while it is dirty — by a parent join building a relationship — therefore shows exactly the rows its consumer has been sent.

5.6 Cap

Cap is Take without order, and it is already most of the way there: membership by PK set, an Add admitted when there is room and dropped when there is not, Child and Edit forwarded by membership. It has no displacement, so admitting an Add at once is final up to bounded churn and needs no read. Its one mid-push fetch is the refill in push_remove (cap.rs:273), and that is the only change: forward the Remove, mark dirty, and refill at the boundary from the first partition rows not in the set.

This matters more than §17.5 allowed. A Cap partition's cascade is bounded by the partition, but a partition can be large — every member of an organization under org.whereExists(members, m => m.whereExists(role, …)) — and each step is a fetch through the inner gate.

Skip is not a limiter in this sense. It is stateless, its bound is the AST's fixed start, and it never fetches on a push (skip.rs:18).

5.7 What this deletes

Every mid-push fetch in Take, and the machinery that exists to make them safe:

  • the displacement probe (take.rs:528, :530);
  • the predecessor probe (take.rs:598) and the refill scan (take.rs:620);
  • the four fetches of the edit matrix (take.rs:743, :754, :784, :821), and with them the (oldCmp, newCmp) case analysis — an edit becomes "forward if a member, update the key, mark dirty";
  • row_hidden_from_fetch and its guard;
  • the short-window rule as an invariant (take.rs:589), and the late cut's lowering (graph.rs:3796), which returns in a simpler form (§6.3).

Take becomes bookkeeping plus one procedure that runs when nothing else does. Limiters stop being a source of mixed-state reads; the Exists cache guard (exists.rs:125) stays, as defence for the fetches joins still make mid-push.

6. The cut, re-licensed

6.1 The rule

Once membership is decided by fetch, deliveries no longer decide anything about rows nothing holds. So:

A join may skip delivering a child change to parent p if (a) no limiter downstream counts p as a member, and nothing between the join and that limiter keeps state per parent; (b) p reads post-change for the rest of the push; and (c) any window p could enter is dirty by the boundary, or cannot admit p.

The engine already behaves this way one level down: a limiter drops every push for a partition it has not hydrated and lets the next fetch re-derive it.

6.2 The last hop (built)

For a parent past the published bound of a full window: (a) holds because the published bound never sorts before a member, and the allow-list walk (first_take_downstream) admits only row-preserving, per-row-stateless nodes; (b) is the overlay's upper edge (join_overlay_for, graph.rs:2402); (c) holds because such a parent enters only through a vacancy, and a vacancy is a member's Remove, which marks the window dirty.

The cut carries over as built, reading a bound that no longer moves mid-push. Its argument gets shorter: it no longer has to show that a mid-push refill sees the right thing, because there is none.

6.3 The late cut, as a provisional bound

Absorbing adds would cost the depth-1 rename-back its O(limit): a short window has no bound to cut at, so all N parents would be delivered and absorbed. The scan pins (take_bounded_fanout::scan_ends_at_the_cut) hold that line.

A limiter therefore keeps the best limit absorbed keys in a bounded heap. Once members plus heap reach limit, it publishes the limit-th smallest as a provisional bound, which only ever lowers. The join's existing lower path picks it up and ends the fan-out. This is safe out of order and under later removes, by §6.1: a skipped row holds nothing and reads post-change, and the window is dirty. The price is that reconcile takes the scan instead of the exact shortcut (§5.4).

6.4 Below O(N) at depth ≥ 2 (not in scope)

Under this design an inner fan-out is still delivered in full: about 1–2 µs a row unflipped in §2's non-cascading cells (10–17 ms at N = 8k). The same rule licenses narrowing it. Its deliveries reach a limiter first — the EXISTS child's Cap, or a nested Take — and that limiter drops everything outside its hydrated partitions. So the parents that can observe the delta are bounded by the consumer's hydrated partition keys, and the inner parent fetch can be constrained to them when they are fewer than the fan-in. That is 316's narrowing, with the demand set read from limiter storage, and 316 S5's crossover applies (narrow_max_parents). It is a separate axis and should not be built before §11's S4.

The doomed-tail scan — post-change rows that fail, between the window and its next survivors — remains, as in every design so far. A flipped plan or a better index shortens it; nothing here does.

7. Correctness argument

Four invariants, then an induction.

  • I1 — emission is membership. members changes only in the same step as an emitted Add or Remove. So what a limiter counts is what its consumer was sent.
  • I2 — quiescent reads. A limiter fetches only at the boundary: source committed, no overlay, no fan-out in flight at any depth, every upstream limiter reconciled. Such a fetch returns what a fresh query over the post-change data would return for that input.
  • I3 — members hear everything. No delivery addressed to a member is skipped. For the cut that holds because the published bound never sorts before a member. 311's pre-check and 316's narrowing skip deliveries too, under their own arguments; §12 lists re-reading them against a bound that moves only at the boundary.
  • I4 — dirty is complete. If the first limit rows post-change differ from members, the window is dirty at the boundary. They differ only if a member left — delivered by I3, which marks dirty — or a non-member entered. A non-member at or before the published bound was delivered its Add, which marks dirty; one past it can enter only through a vacancy, which is the first case. A short window has no cut, so every Add is delivered. A provisional bound is published only after adds were absorbed, so the window is already dirty.

Induction, upstream first: a limiter with no limiter upstream reconciles by I2 to the first limit rows of a settled input; its emissions are ordinary pushes. Every limiter downstream then reconciles over settled inputs by the same argument. Non-members hold nothing, so at the end every held row has received every delta (I3) and every window equals the fresh answer (I2, I4). That is view-after-write == fresh-query.

What this argument does not need is the point: no statement about which rows a mid-push scan may meet, no ordering of deliveries, no depth.

8. Costs

  • Memory. One sort key per row in every maintained window. On the client the view holds those rows already. On the daemon it is new: a family root keeps one window per binding, so limit × bindings keys. Cap pays this today for EXISTS. If it bites: store a hash per member and recover order by fetch, as now (§12).
  • Reconcile work. The exact shortcut keeps a single-row change at a constant number of keyed fetches. A scan is at most limit rows and is paid only by pushes that are already fan-out sized.
  • Emission moves later. Adds reach the consumer after the source change's last connection has pushed, not in the middle of it. Nothing downstream is known to depend on the old position; §10's differential lanes are the check.
  • Still O(N): inner deliveries at depth ≥ 2, and the doomed-tail scan (§6.4).

9. Alternatives considered

Alternative Why not
The cut with a mid-push refill (316 §17.5 as built) Correct and measured at depth 1. One level down the cut never engages (§2)
Upstream's TakeGate + reconcile Fixes aligned removes at any depth; leaves opposed adds (§2). The gate must be opened around the Take's own scans; the overlay reads a live bound that disappears mid-push; the pending window is a third state its readers must know
The cut, a captured bound, and a deferred refill The same coverage as upstream with the bound fixed. At depth 2 every inner delivery after the first in-window remove starts an outer fan-out against a pending window, so that third state is on the main path, in window_at, in both eviction guards and in the short-window rule
Push the cut down to inner joins §3: sound for removes, an ancestor probe per row, an upward allow-list per depth, and nothing for opposed adds
Keep the mid-push path when every in-flight fan-out is governed; defer otherwise Two limiters to keep correct instead of one, and the intricate one is the one kept
Let the cascade run and coalesce the output Fixes the change count and none of the work; the O(N²) flipped cells remain

10. Verification

  • Pins from §2: at most 2 × limit changes in all four cells, flipped and not, at depth 2 and depth 3, plus a leaf-rows-scanned pin in the style of scan_ends_at_the_cut.
  • Both paths through the whole it suite and every fuzz lane while the kill switch exists, as the cut had. The widened decorated-push lanes already mutate every table of an OR-ed, flipped, depth-3 skeleton; each gains an assertion that the boundary path fired.
  • Operator state after later writes: exists_partition_churn_leak.rs, take_partition_leak.rs and the #594 regressions stay green unchanged. Eviction parity is the part of §5 most likely to need a second look.
  • One source change through more than one connection, in both orders (take_bounded_fanout.rs), and both halves of a split edit hitting one window.
  • A self-join where one source change edits a member's sort key through the parent connection and fans out through the child connection — the case the published bound's "never before a member" rule exists for.
  • Optional: a small TLA+ model beside the four in tla/ — one window, limit 2, four rows, arbitrary deliveries then a boundary — checking I1 and I4.

11. Slices

Slice Content Gate
S0 Take stores members; fetch answers from them; behaviour otherwise unchanged Every lane green on the unchanged push paths. Reviewable alone
S1 The dirty worklist and the drain in try_source_push; §5.2 and §5.4 for changes that arrive while a child fan-out is in flight; kill switch §10's pins; both paths green
S2 The provisional bound (§6.3) The scan pins and the depth-1 measure table unchanged
S3 Every change takes the same routine; delete the in-place paths (§5.7) Both paths green one last time, then the switch goes
S4 Cap (§5.6) A large-partition probe
S5 Inner narrowing (§6.4) Its own design pass against 316

12. Open questions

  1. Boundary Removes. A displaced member still passes, so its node is fetched by key post-change. The flat Remove is row-only (flat.rs:64) and the view's remove path consumes only the row, so the node's subtree should not matter — but a nested limiter's Remove also enters an outer join's child port, and this is the #594 class. Pin it first. If the whole row were stored per member, the fetch could go.
  2. Key representation. Sort key, whole row, or hash — a memory trade on the daemon (§8). Needs a number from a family workload before S0 fixes the storage shape.
  3. Eviction parity. Rows absorbed and then not admitted sit past the new bound with hydrated upstream partitions until something touches them. That matches today's non-members left behind by a bound that moved down, but it is argued, not measured.
  4. Drain per transaction instead of per source change. The rules tolerate a window that stays dirty across changes. Whether anything else does is unexamined.
  5. 311 and 316. A reconcile scan from start carries a start, so 311's observation rule ignores it as it ignores refills today. 316 §7.4 ("limit movement and empty scopes") should be re-read against a bound that moves only at the boundary.
  6. Upstream. The same split would need member identity in take.ts. Row 6 of §1 is open on their branch.

conversation

Comments

Select any passage above to comment on it inline.

Loading comments…

powered by rindle