Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
67 commits
Select commit Hold shift + click to select a range
2054ae4
WIP: term tables as relations + get-fresh! mint + cost on views
oflatt Jul 15, 2026
a04e1e1
WIP: proof/AST/ProofList constructors as relations + mint helper
oflatt Jul 15, 2026
110bee6
WIP: flatten all nested proof-construction sites to mint sequences
oflatt Jul 15, 2026
698657e
Rework proof extraction + container-rebuild for relations
oflatt Jul 15, 2026
4259ec9
Add set-if-empty canonicalization: term-only validated, proof mode WIP
oflatt Jul 15, 2026
c0717a4
Faithful term-construction threading for proof-mode canonicalization
oflatt Jul 16, 2026
e14c288
Thread connectors into union proofs via proof-of-max/min
oflatt Jul 16, 2026
ebd0d39
Fix proof-mode canonicalization: reflexive proof for canonical-childr…
oflatt Jul 16, 2026
b91b748
Fix proof-mode canonicalization: thread connector through let-bound t…
oflatt Jul 16, 2026
b5bc96d
Regenerate proof-testing snapshots after canonicalization fix
oflatt Jul 16, 2026
130b83f
Scope nat_conn per instrumentation unit
oflatt Jul 16, 2026
7a408ed
Canonicalize container elements via a UF-Aux table (uniform, no @Congr)
oflatt Jul 16, 2026
3459497
cargo fmt
oflatt Jul 16, 2026
8de6594
Children-free custom-merge proofs + reflexive rule premises
oflatt Jul 17, 2026
7fce91a
Run custom merges in the FD view's :merge (drop current+rule)
oflatt Jul 18, 2026
c8d59a0
DD backend: fix build + unify fresh-id minting with core-relations
oflatt Jul 18, 2026
33ddfe3
Route get-fresh!/set-if-empty through the backend SPI
oflatt Jul 18, 2026
1788cc3
Fix proof-extraction order-dependence + custom eq-sort output rebuild
oflatt Jul 18, 2026
ea2da6d
Make get-fresh! a single generic primitive (sort as string arg)
oflatt Jul 18, 2026
cc83e75
Drop @ prefix from set-if-empty/view-proof primitive names
oflatt Jul 18, 2026
e58ba7d
Batch (input …) fiat loading into one bodyless rule (avoid per-mint g…
oflatt Jul 19, 2026
5e15bb7
Load (input …) facts natively instead of compiling a loader rule
oflatt Jul 19, 2026
18f82f4
Desugar globals as functions (not constructor+union) in term/proof en…
oflatt Jul 20, 2026
c9425be
core-relations: reset only modified tables' indexes in merge_all
oflatt Jul 20, 2026
47baa22
egglog-bridge: make free_external_func O(1) via reverse id->message i…
oflatt Jul 20, 2026
2b24395
Make proof extraction deterministic (smallest witness row)
oflatt Jul 20, 2026
0842924
Update proof_tests snapshots + hoisting assertion for the relations e…
oflatt Jul 20, 2026
bd9da5d
docs: add "Building nested terms in actions" section (Neg/Add example)
oflatt Jul 20, 2026
448148b
docs: restructure proof_encoding.md around actions then queries
oflatt Jul 20, 2026
7ed414a
Trim CHANGELOG entries to concise bullets (drop impl detail)
oflatt Jul 20, 2026
56547fe
Address PR review: fix prove-exists panic, drop dead code, tidy comments
oflatt Jul 20, 2026
26660c5
core-relations: remove dead set_counter / Counters::set
oflatt Jul 20, 2026
c649d01
docs: clarify union-in-rule and use e/e'/e'' naming for nested terms
oflatt Jul 20, 2026
3418ec6
Fix global-value proofs; narrow skip-rebuild; drop dead Merge path
oflatt Jul 20, 2026
e18b4ad
docs: address review comments (fd_custom_funcs, displaced comment, ba…
oflatt Jul 20, 2026
f9ab314
docs: note backend needs no union/constructor when evaluating actions
oflatt Jul 20, 2026
3225c4e
Register get-fresh! once per e-graph instead of per eq-sort
oflatt Jul 20, 2026
4b738b1
Move run_merge_subexpr to proof_format (raw->proof conversion)
oflatt Jul 20, 2026
915707d
Restore Database::set_counter (used by the differential-dataflow back…
oflatt Jul 20, 2026
1c0761a
Load all (input ...) natively; make native_input annotation-driven
oflatt Jul 20, 2026
c8f34a5
Make fail take a list of commands
oflatt Jul 20, 2026
1e1a162
Review cleanups: local nat_conn map, output_is_eclass helper, dd add_…
oflatt Jul 20, 2026
5f63d52
Make :no-merge unsupported by the term/proof encoding
oflatt Jul 20, 2026
4a64eec
Support primitive/Unit :no-merge natively; drop fd_custom_funcs
oflatt Jul 20, 2026
a19517a
Clean up proof_encoding rebuilding rules; tighten comments
oflatt Jul 21, 2026
6b82140
Make @UF-Aux name fresh + annotation; mint-first in add_term_and_view
oflatt Jul 21, 2026
a809bea
Add env-gated DD perf diagnostics: phase timing, plan dump, W override
oflatt Jul 21, 2026
a90bd49
Compact DD physical layouts: per-ruleset row width + u128 join keys
oflatt Jul 21, 2026
b08f616
Make host-side bookkeeping O(delta): key index + view event logs
oflatt Jul 21, 2026
233c7ca
Share raw-relation arrangements across all join call sites
oflatt Jul 21, 2026
21d54a0
Prototype: rebuild fixpoint as an in-dataflow DD iterate scope
oflatt Jul 21, 2026
4a3802b
Design: general schedule->DD compiler, memoizing mint, monotone-fire …
oflatt Jul 21, 2026
796b97e
Prototype: rising-edge fire and memoizing mint operators
oflatt Jul 21, 2026
e6a066b
Design: concrete run_schedule backend-API extension plan
oflatt Jul 21, 2026
3794916
Add run_schedule backend hook; DD takes whole schedule trees
oflatt Jul 21, 2026
41e47b5
Prototype schedule regions: gated run-N feedback, mint inside saturation
oflatt Jul 21, 2026
b65dd99
Schedule compiler v1: datalog-subset schedules run as one dataflow
oflatt Jul 21, 2026
fe1967d
Compile mints and hash-cons; retry compilation per loop-bearing subtree
oflatt Jul 22, 2026
c6fbdaf
General merge lowering: the merge hub
oflatt Jul 22, 2026
be771f8
Design: record the approved shared-crate roadmap
oflatt Jul 22, 2026
e0e3953
Schedule engine: full in-dataflow execution at hybrid-parity speed
oflatt Jul 22, 2026
f6ea25d
Persistent per-spec engine dataflows
oflatt Jul 22, 2026
91bbd18
Document persistent-dataflow results and v2 delta-feeding design
oflatt Jul 22, 2026
953bd84
Engine: sorted run-fold ingest (run 11: 95.4s -> 79.1s)
oflatt Jul 23, 2026
32a688e
Remove stray benchmark logs committed by accident
oflatt Jul 23, 2026
22ace6f
Prototype: nested-scope consolidation suppresses saturation churn (ta…
oflatt Jul 23, 2026
4288cd1
Doc: DD backend state, lessons, and the FlowLog direction
oflatt Jul 23, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
323 changes: 322 additions & 1 deletion Cargo.lock

Large diffs are not rendered by default.

4 changes: 4 additions & 0 deletions egglog-experimental/dd/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ log = "0.4"
differential-dataflow = "=0.24.0"
timely = "=0.30.0"
serde = "1"
pprof = { version = "0.15.0", features = ["flamegraph"], optional = true }

[[test]]
# Parity harness over egglog's .egg corpus: checks the DD backend against
Expand All @@ -36,3 +37,6 @@ egglog = { path = "../../egglog", default-features = false }
egglog-experimental = { path = "..", default-features = false }
insta = "1.40"
libtest-mimic = "0.8"

[features]
pprof = ["dep:pprof"]
202 changes: 202 additions & 0 deletions egglog-experimental/dd/docs/flowlog-direction.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,202 @@
# The differential-dataflow backend: state, lessons, and the FlowLog direction

A pick-up-later summary of the `oflatt-dd-rebuild-in-dataflow` work. The goal
has been a clean, fast DD backend for egglog: compile rules + schedule into
differential dataflow and saturate entirely in-dataflow. We reached
hybrid-parity performance, then hit a wall that reframed the whole design
around how [FlowLog](https://arxiv.org/abs/2511.00865) (a Datalog→timely/DD
compiler on our exact substrate) structures its dataflow. This document is the
map back in.

## 1. Where things stand

Branches / PRs (against `saulshanabrook/egglog-encoding`):

- **PR #29** — perf pass on the pre-existing (hybrid) DD backend: `211s → 70s`
on math-microbenchmark run 11 (RowN width ladder + u128 join keys + compiled
AtomOps; persistent `by_key` index + per-view event logs; shared
arrangements).
- **PR #31** — the **schedule engine**: a whole schedule (`Run`/`Repeat`/
`Saturate`/`Sequence`, spliced rebuild included) compiled into ONE dataflow.
A stateful `ScheduleEngine` operator walks the schedule as a program counter
and does everything the host interpreter did (mint, hash-cons, merge, delete);
DD does only the incremental joins; effects feed back through a root-scope
`Variable`. Persistent per-spec dataflows across invocations. Reached
~hybrid parity: run 9/10/11 ≈ `1.0 / 6.8 / 79s` after the sorted run-fold
ingest optimization.
- **PR #34** — standalone encoding change: a term-mode constructor's
`get-fresh!` now receives its `(constructor, children)` so a backend can
content-address the mint. (Being extended by a separate effort into a lossy
hash-cons; see §7.)

Not committed:

- **Seminaive fix** (fire-on-positive-delta) and the **interpreter removal**
(`DbHandle`) are stashed on this branch — correct but perf-blocked (§7).
- Prototypes committed on the branch: `tests/rebuild_fixpoint.rs`,
`tests/monotone_fire.rs`, `tests/schedule_regions.rs`,
`tests/scope_consolidation.rs`; operators in `src/monotone.rs`.

Note the schedule engine lives only on this branch; `encoding/main` (upstream,
post-#22) has the **hybrid** DD backend (fused per-ruleset workers), no engine.

## 2. The long-term vision: be like FlowLog

Render the **schedule tree itself as nested DD `iterate` scopes**, instead of a
single flat stateful operator. The backend only ever sees four structural
constructors — `Run`, `Repeat(N)`, `Saturate`, `Sequence` (until-clauses are
filtered out upstream) — and they map directly:

| egglog | DD rendering |
|---|---|
| `Saturate(body)` | `iterate` to fixpoint |
| `Repeat(N, body)` | bounded `iterate` (round-gated `Variable` feedback) |
| `Sequence([a, b])` | sibling scopes: `b` reads `a`'s `leave()`d output |
| `Run(ruleset)` | the ruleset's rule bodies as joins feeding `Variable`s |
| rebuild (UF + congruence) | a recursive-`MIN` fixpoint (= connected components) |
| `:merge` (UF `ordering-min`, `lo`/`hi` min/max) | "iterative"/replacement `Variable` + `reduce` |

Rule *bodies* are already DD joins. The egglog-specific *semantics* Datalog
lacks — minting (`get-fresh!`), hash-cons (`set-if-empty`), monotone-fire
deletes — become custom operators inside the scopes (prototyped in
`monotone.rs`: `memoizing_mint`, `first_per_key`, `rising_edge`).

## 3. Why: the churn problem (what forced this)

The flat engine runs **every rule's join at one timestamp**. During the long
rebuild saturation the tables churn hard (canonicalization = delete old row +
insert canonical), and every delta flows through **all** rules' joins — even
the ~130 user rules that won't fire until rebuild finishes.

Measured on a herbie subset:

- **109M tuples** into arrangements, **67M** match-deltas into the engine, to
produce **172K** real row changes — a **~390×** amplification (math is ~8×).
The single worst arrangement: one user rule at **27.9M** tuples, for a rule
whose leaf fires 6 times.
- Full herbie fully-compiled: **>400s** (times out) vs **4.2s** on the hybrid
fallback vs **0.16s** native. Correct, just catastrophically slow.

The hybrid avoided this by building a dataflow *per ruleset when it ran*, on the
settled state. The flat engine has no boundary where the intermediate churn can
be discarded.

## 4. How FlowLog does it (confirmed in its source + the DD source)

- Each recursive stratum = `scope.iterative` + one `Variable` per recursive
relation. Sequencing between strata falls out of timely frontiers (a
downstream stratum stalls until the upstream fixpoint retires); one
`worker.dataflow` for the whole program.
- Timestamps are `Product<epoch, iter>` — only two levels; strata are siblings.
- **Consolidation is explicit and is the whole trick.** `leave()` re-stamps
inner-iteration records to the outer time via `to_outer()`, and an explicit
`consolidate()` right after nets the cancelling ±1s away. DD's `iterate` does
*not* auto-consolidate — you insert it. FlowLog's own comment: *"Inside the
scope they can't cancel (different inner timestamps); after `leave()` both
project to the same outer time, so consolidate nets them out."*
- Rebuild = **recursive `MIN` aggregation** (connected components), which
FlowLog optimizes by baking `MIN` into the diff monoid `(ℤ, MIN)`. egglog's
union-find leader *is* the component minimum — same computation.
- FlowLog has **no** value creation; the existential-Datalog→DD lineage (USPTO
11,656,868) does, and warns that a mutable counter is fragile under
retraction — use **content-addressed Skolem ids** (hash of rule + position +
substitution). That is exactly the keyed `get-fresh!` we're building.

The consolidation mechanism is validated in `tests/scope_consolidation.rs`:
min-label propagation (= UF leader) in an `iterate` scope, feeding a downstream
join. With `consolidate()` after the loop the join receives **5** tuples (the
net); without it, **17** (every intermediate label leaks). That 17→5 is the
herbie 67M→172K in miniature.

## 5. What egglog needs beyond FlowLog (the honest gaps)

- **Nested loops → 3 timestamp levels.** `Repeat(N, Seq(user, Saturate(rebuild)))`
nests a fixpoint inside a bounded loop; FlowLog only ever uses two levels. DD
supports arbitrary `Product` nesting; FlowLog just never needed it.
- **Minting.** Content-addressed, keyed on `(constructor, canonical children)`
— see §7 for why both parts are required, and lossy hash-cons for how to make
it parallel-safe.
- **Proof mode.** Rebuild composes proof terms host-side. Term-mode-first;
proof mode via provenance reconstruction later.
- **Deletes/subsumes.** Retraction + re-keying interaction needs design.
- **Report parity.** `(print-stats)` wants a per-iteration `changed`/
`num_matches` stream; a run-to-fixpoint scope hides iteration boundaries, so
the report shape has to be reconstructed. (Also note: the DD backend never
filled per-rule `num_matches` — a pre-existing gap.)

## 6. Prototypes that de-risk the plan

- `rebuild_fixpoint.rs` — the entire UF + congruence closure as ONE `iterate`
scope via label propagation + `reduce` (mints nothing; incremental across
epochs). This is the rebuild rendering.
- `monotone.rs` + `monotone_fire.rs` — `memoizing_mint` (content-addressed id),
`first_per_key` (`set-if-empty` as a latch), `rising_edge` (monotone-fire),
all designed to run *inside* `iterate` scopes.
- `schedule_regions.rs` — `(run N)` as gated feedback, minting inside a
`Product`-timestamped saturation.
- `scope_consolidation.rs` — the churn-cancellation-at-`leave` mechanism (§4).

## 7. Key lessons (mostly from things that failed)

- **Seminaive is unsound under merges as we had it.** After a congruence merge
re-canonicalizes a rebuild rule's supporting row, the −1/+1 churn nets to zero
in a per-round fold, so the rule doesn't re-fire — but egglog re-fires it (the
row's timestamp bumps). Collapse rules then lag the growth rules and the term
set explodes (herbie single `(run 6)`). Fix (stashed): **fire on any positive
delta this round**, not just a 0→positive crossing — matches egglog's
timestamp seminaive, ~7% cost on math. Uniform; no naive, no name-gating
(both of which the design rejected).
- **Content-addressed minting must key on `(constructor, children)`.** Keying on
`(sort, children)` collides sibling constructors — `Add(a,b)` and `Mul(a,b)`
are both sort `Math`, so they get the same id and wrongly share an e-class →
congruence collapse → hang. The sort does not identify the term.
- **And on *canonical* children.** Raw-children keying with a persistent memo
returns stale ids once rebuild merges those ids away (the patent's warning).
Canonical children need the union-find at construction — which only the
fixpoint scope has. So **minting is not a clean isolated pre-step; it belongs
inside the scope rendering.** (This flipped the plan order.)
- **Lossy hash-cons is the right minting model** (matches egglog constructors):
usually the same id, occasionally two ids for one term under a thread race,
which rebuild merges. It won't break DD convergence **provided it is
append-only / eventually-stable** — new ids only on first-insertion races,
never re-minting an interned term. DD's deterministic partitioning keeps a
term on one worker → stable id → the fixpoint converges; cross-worker
duplicates are bounded one-time merges. A global `Mutex<HashMap>` is the wrong
implementation (serializes all mints); shard it or use a per-worker memo. The
current single-worker engine has no races anyway.
- **Flattening to a single `u32` scope was a local win, global loss.** It saved
~12% (no subgraph layer) but removed the only place churn could consolidate.
Fine for low-amplification schedules (math), fatal for high (herbie).

## 8. Concrete next steps

1. **Content-addressed minting foundation** — keyed `get-fresh!` (PR #34) +
lossy, append-only hash-cons. Enables terms to be built inside a fixpoint
without re-minting each round.
2. **Schedule-tree → scope lowering** — the re-architecture. Render each
`Saturate`/`Repeat` leaf as a native `iterative` scope with `Variable`s per
written relation and `consolidate()` after `leave()`; downstream leaves read
the consolidated output. This is where the churn dies and herbie becomes
viable; it also shrinks math's rebuild. Rebuild is the first client, rendered
as the recursive-`MIN` fixpoint — recognized by schedule *structure* (a
leaf-level loop), not by ruleset name.
3. **Content-address minting within the scope**, keyed on `(constructor,
canonical children)` where the labels are in hand.
4. **Follow-ons**: subplan sharing (FlowLog's canonical-hash CTE reuse, for the
many-rule cost), proof mode, deletes/subsumes, report parity.

Sequence-wise, (1) and (2) are more coupled than they first look: the churn win
*requires* a loop's rules to live in their own scope with downstream rules
outside it, which is most of (2). Expect to build the scope skeleton and
content-addressing together.

## 9. Reference points

- Design doc with the rebuild-in-dataflow formulation and walls:
`docs/rebuild-in-dataflow.md`.
- FlowLog: paper `arxiv.org/abs/2511.00865`; source `github.com/flowlog-rs/flowlog`
(`codegen/flow/{recursive,non_recursive}.rs`, `codegen/dedup.rs`,
`stratifier/core.rs`).
- Timely `leave`/`to_outer`: `timely/src/dataflow/operators/core/enterleave.rs`.
- DD `iterate` (note: no auto-consolidate):
`differential-dataflow/src/operators/iterate.rs`.
Loading