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 (branchbounded-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
reconcilephase 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
Takekept 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.
- Rindle's change counts are identical with
RINDLE_FANOUT_CUT=off. The join that fans out (comment ⋈ author) has no governingTake:first_take_downstreamgives up at aJoinChildport (graph.rs:3685). Its pre-change band has no upper edge, so the outerTake's mid-push refill admits an issue whose comment has not been delivered yet. - The last hop is governed, and its cut works when the order cooperates. In
back, alignedthe 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. - Deferring the refill fixes one cell, not both. Upstream's boundary refill sees
post-change state at every depth, so
away, alignedis 10.back, opposedis 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:
- The fan-out runs in the window's order, so the first
limitadds to arrive are final and the late cut can end the fan-out. - 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
RemoveorChildfor a non-member is dropped, whatever its position. - An
Addcan 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. memberschanges only together with an emittedAddorRemove. 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
Removeis 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
Addis never emitted during a push. Whetherrbelongs 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
NodeIdis expected to be such an order — S1 checks it.) - Split edits. A split
Editpushes 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_fetchand 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
pif (a) no limiter downstream countspas a member, and nothing between the join and that limiter keeps state per parent; (b)preads post-change for the rest of the push; and (c) any windowpcould enter is dirty by the boundary, or cannot admitp.
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.
memberschanges only in the same step as an emittedAddorRemove. 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
limitrows post-change differ frommembers, 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 itsAdd, which marks dirty; one past it can enter only through a vacancy, which is the first case. A short window has no cut, so everyAddis 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 × bindingskeys.Cappays 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
limitrows 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 × limitchanges in all four cells, flipped and not, at depth 2 and depth 3, plus a leaf-rows-scanned pin in the style ofscan_ends_at_the_cut. - Both paths through the whole
itsuite 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.rsand 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,limit2, 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
- Boundary
Removes. A displaced member still passes, so its node is fetched by key post-change. The flatRemoveis 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'sRemovealso 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. - 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.
- 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.
- Drain per transaction instead of per source change. The rules tolerate a window that stays dirty across changes. Whether anything else does is unexamined.
- 311 and 316. A reconcile scan from
startcarries astart, 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. - 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.
Sign in to join the conversation.
Loading comments…