From 2418f9fe34600f6553f944e59da9c24e9be0fe7e Mon Sep 17 00:00:00 2001 From: Avi Avni Date: Thu, 27 Aug 2026 16:51:42 +0300 Subject: [PATCH] topic 44: e-matching is a join, and the two testing systems topic 16 only named MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Topic 44 — E-graphs as a Database: Relational E-matching & egglog. The sequel to topic 21, placed here because the fix for equality saturation's bottleneck came out of the database literature: e-matching is 60-90% of its run time (POPL'22 §1) and it is a conjunctive query. Lane 1, provided: on the POPL'22 Figure 2 e-graph (3N e-nodes standing for N²+2N terms), the pattern f(a, g(a)) has N matches and costs a backtracking matcher N²+N+1 units of work while generic join does 5N — 2,561,601 against 8,000 at N=1600, a measured 21.72x. Both counters are closed forms and reproduce exactly. The second table is the honest one: rename the repeated variable, the pattern goes linear, every candidate becomes an answer, and generic join comes out 0.56x — 1.8x slower. Same result POPL'22 reports in Table 1's Worst column (0.76, and 0.03 with index building charged). Theorem 10's O(sqrt(|Q(I)| · prod|Ri|)) predicts both rows: 64,000 against 8,000 measured, and 2,560,000 against 2,561,603 measured, i.e. *at* the bound. Lane 2 prices naive evaluation without implementing the fix: a 24-tuple delta re-derives 20,008 matches with 100,040 probes for 8 new answers. Lane 3's generator keeps the answer size flat at (E/V)³ = 125 while the graph grows 8x, so generic join's probes grow linearly and the binary plan's intermediate — the reader's stub — grows as E²/V. experiments/: a minimal e-graph, egg's Bind/Compare/Scan VM with the op index (so the baseline is a strategy, not a strawman), Figure 8's unnesting, tries, most-constrained-first ordering, generic join. Six provided tests pass; four stub tests are the specification (semi-naive evaluation, and a left-deep binary-join plan for the triangle multi-pattern). Four reading guides. The source guide's finding is that the papers understate the codebase: core-relations is a database, semi-naive evaluation is a binary search on a clustered sort column (table/mod.rs:497-510), the planner does hypertree decomposition with a min-fill heuristic (plan.rs:1-46), and congruence closure is compiled into a rule rather than implemented (egglog-bridge/src/lib.rs:945). egglog's union-find declines union-by-rank for union-by-min-id and says why — the same class of finding as egg's non-compressing find. Topic 16 gains the two guides it had been name-dropping: - reading-hypothesis.md — shrinking the choice sequence rather than the value; shortlex order worked on real indices; the shrink-pass determinism invariant; the DataTree as a trie over executions; and Hypothesis's documented deviation from the swarm-testing paper. find_integer(100) was executed rather than hand-traced: 16 calls. - reading-antithesis.md — read against the open SDK, since the platform is closed. The no-caching contract on get_random only makes sense for a branching simulation, not a replayed one; Sometimes as a coverage property (crash_matrix's None row is the hand-rolled version); the linker-assembled assertion catalog; guidance as Hypothesis's target phase at fleet scale. No Antithesis figure is quoted, because none can be checked from this side. One benchmark bug, caught by the counters disagreeing with the clock: gj allocated a Vec per intersection key, which left every counter identical and doubled the wall clock. Plumbing: PLAN.md §44 and the map, FINDINGS row, verify.sh lane, PROGRESS status + M44, SUMMARY entries, SESSION-LOG entry, topic counts 44 -> 45 and crate count 45 -> 46. Pin table regenerated: adds egglog, hypothesis, antithesis-sdk-rust and y-crdt, and refreshes mention counts that had gone stale since the guides doubled in size. Gates: verify.sh 44 PASS, check-reading-depth.py --check --all 236/236, pin-table.py --check current, mdbook build clean, mermaid validated, no broken relative links. Co-Authored-By: Claude Opus 5 --- .github/workflows/verify.yml | 2 +- CLAUDE.md | 2 +- CONTRIBUTING.md | 2 +- FINDINGS.md | 4 +- PLAN.md | 15 +- PROGRESS.md | 4 +- README.md | 2 +- SESSION-LOG.md | 41 + SUMMARY.md | 8 + resources/codebases.md | 160 ++-- topics/16-testing-correctness/README.md | 2 + .../reading-antithesis.md | 558 ++++++++++++++ .../reading-hypothesis.md | 664 ++++++++++++++++ topics/44-egraphs-egglog/README.md | 353 +++++++++ .../44-egraphs-egglog/experiments/Cargo.lock | 134 ++++ .../44-egraphs-egglog/experiments/Cargo.toml | 11 + .../experiments/src/backtrack.rs | 184 +++++ .../experiments/src/bin/ematch_bench.rs | 259 +++++++ .../experiments/src/binary_join.rs | 89 +++ .../experiments/src/egraph.rs | 214 +++++ .../44-egraphs-egglog/experiments/src/gen.rs | 133 ++++ .../44-egraphs-egglog/experiments/src/lib.rs | 17 + .../experiments/src/pattern.rs | 178 +++++ .../experiments/src/relational.rs | 319 ++++++++ .../experiments/src/semi_naive.rs | 101 +++ topics/44-egraphs-egglog/notes.md | 161 ++++ .../reading-egglog-pldi23.md | 507 ++++++++++++ .../reading-egglog-source.md | 597 ++++++++++++++ topics/44-egraphs-egglog/reading-free-join.md | 452 +++++++++++ .../reading-relational-ematching.md | 728 ++++++++++++++++++ verify.sh | 1 + 31 files changed, 5817 insertions(+), 85 deletions(-) create mode 100644 topics/16-testing-correctness/reading-antithesis.md create mode 100644 topics/16-testing-correctness/reading-hypothesis.md create mode 100644 topics/44-egraphs-egglog/README.md create mode 100644 topics/44-egraphs-egglog/experiments/Cargo.lock create mode 100644 topics/44-egraphs-egglog/experiments/Cargo.toml create mode 100644 topics/44-egraphs-egglog/experiments/src/backtrack.rs create mode 100644 topics/44-egraphs-egglog/experiments/src/bin/ematch_bench.rs create mode 100644 topics/44-egraphs-egglog/experiments/src/binary_join.rs create mode 100644 topics/44-egraphs-egglog/experiments/src/egraph.rs create mode 100644 topics/44-egraphs-egglog/experiments/src/gen.rs create mode 100644 topics/44-egraphs-egglog/experiments/src/lib.rs create mode 100644 topics/44-egraphs-egglog/experiments/src/pattern.rs create mode 100644 topics/44-egraphs-egglog/experiments/src/relational.rs create mode 100644 topics/44-egraphs-egglog/experiments/src/semi_naive.rs create mode 100644 topics/44-egraphs-egglog/notes.md create mode 100644 topics/44-egraphs-egglog/reading-egglog-pldi23.md create mode 100644 topics/44-egraphs-egglog/reading-egglog-source.md create mode 100644 topics/44-egraphs-egglog/reading-free-join.md create mode 100644 topics/44-egraphs-egglog/reading-relational-ematching.md diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 31618f6..7d7a76c 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -39,7 +39,7 @@ jobs: # takes precedence over .cargo/config.toml's ../.dlp-target. Necessary # because actions/cache rejects any path containing ".." — it logs # "Invalid pattern" and then silently caches nothing, so every run - # recompiles all 45 crates from scratch. The reason the checked-in config + # recompiles all 46 crates from scratch. The reason the checked-in config # points outside the clone is mdbook, which never runs in this workflow. - name: Cache cargo uses: actions/cache@v6 diff --git a/CLAUDE.md b/CLAUDE.md index 4abca0f..1980c03 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -4,7 +4,7 @@ This file provides guidance to Claude Code (claude.ai/code) when working with co ## Project Overview -A self-paced database-internals learning path, rendered as an mdBook (`book.toml`, content in `topics/`, exercises in `capstone/`). `PLAN.md` is the curriculum plan — 44 topics, the source of truth. `PROGRESS.md` tracks status and capstone milestones; `SESSION-LOG.md` is the detailed build log, one entry per topic, newest first. `CONTRIBUTING.md` documents the topic package format and the conventions below. +A self-paced database-internals learning path, rendered as an mdBook (`book.toml`, content in `topics/`, exercises in `capstone/`). `PLAN.md` is the curriculum plan — 45 topics, the source of truth. `PROGRESS.md` tracks status and capstone milestones; `SESSION-LOG.md` is the detailed build log, one entry per topic, newest first. `CONTRIBUTING.md` documents the topic package format and the conventions below. ## Working rules diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index c0b47b2..c78bc51 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -125,7 +125,7 @@ python3 tools/check-reading-depth.py --stats # rollout prog ``` A second workflow ([verify.yml](.github/workflows/verify.yml)) runs -`./verify.sh --summary` and a `-D warnings` build of all 45 crates on every push and +`./verify.sh --summary` and a `-D warnings` build of all 46 crates on every push and pull request. It is the gate that keeps the repo's central claim true, so a lane that stops running is a red build. Note that `cargo test` is deliberately **not** a gate: the stub tests are the specification and are supposed to fail on a fresh clone. diff --git a/FINDINGS.md b/FINDINGS.md index f076dcc..a64705a 100644 --- a/FINDINGS.md +++ b/FINDINGS.md @@ -5,7 +5,8 @@ whole argument for this format over a reading list in one table: a link collection cannot be wrong in a way you can detect, and every row below can. Every figure here comes from a benchmark in this repo, measured on an **Apple M3 -Pro (5P + 6E, 36 GB)** on 2026-07-28. Generators are seeded, so counts, +Pro (5P + 6E, 36 GB)** on 2026-07-28, except topic 44's row, measured on +the same machine on 2026-08-26. Generators are seeded, so counts, ratios and distributions reproduce exactly; timings will differ on your hardware. Run everything with `./verify.sh`, one topic with `./verify.sh 12`, or `./verify.sh --list` to see every lane. @@ -59,6 +60,7 @@ instead. | 41 | [On-Chain Analytics](topics/41-onchain-analytics/README.md) | The industry-default haircut rule marks **98% of addresses** tainted from one theft; 658 of them are under 0.1% tainted. An 1816 court case does better. | `./verify.sh 41` | | 42 | [Recommendations & Social](topics/42-recommendations-social/README.md) | Recommending bestsellers to everyone gets **34.0% hit-rate@50** with **92.3% overlap** with the global bestseller list. Popularity is not a weak baseline. | `./verify.sh 42` | | 43 | [Ops Dependency Graphs](topics/43-ops-dependency-graphs/README.md) | One gray failure: **34 of 55 services alert** and the broken one is not among them — it ranks 35th by failure count, 41st by error rate, at exactly the baseline. | `./verify.sh 43` | +| 44 | [E-graphs as a Database](topics/44-egraphs-egglog/README.md) | `f(a, g(a))` has **N matches** and costs a backtracking matcher **N²+N+1** units of work; generic join does **5N**. At N=1600: 2,561,601 against 8,000, a measured **21.7×**. Make the pattern linear and generic join is **1.8× slower** — the win is avoided waste, not speed. | `./verify.sh 44` | ## How to read this table diff --git a/PLAN.md b/PLAN.md index 97a1dbf..20d5df3 100644 --- a/PLAN.md +++ b/PLAN.md @@ -42,6 +42,7 @@ flowchart TD end subgraph CORRECT["Correctness"] T16["16 testing"] --> T21["21 formal methods"] + T21 --> T44["44 e-graphs as a database"] end subgraph STREAM["Streaming & temporal"] T27["27 incremental views"] @@ -228,7 +229,7 @@ flowchart TD **Why:** The topic that separates hobby DBs from production DBs. Turso and FoundationDB made this their identity. - **Concepts:** deterministic simulation testing (DST), fault injection, property-based testing (proptest), fuzzing (cargo-fuzz/AFL), metamorphic testing (SQLancer's pivoted queries / TLP), Jepsen & elle (checking linearizability), model checking with TLA+ (taste of), SMT solvers (Z3): proving query rewrites equivalent (Cosette-style), checking optimizer rules and constraint/invariant satisfiability. -- **Read code:** turso's simulator + DST setup (they blog about it), FoundationDB simulation docs, SQLancer, antithesis blog posts, redis `test/` harness, Z3 (`z3.rs` bindings; skim the tactic/solver architecture — treat Z3 itself as a masterclass codebase: it's a high-performance search engine over logic). +- **Read code:** turso's simulator + DST setup (they blog about it), FoundationDB simulation docs, SQLancer, `HypothesisWorks/hypothesis` (the `internal/conjecture/` engine — the choice sequence, `sort_key`'s shortlex order, the shrink-pass determinism invariant, the `DataTree`, and swarm testing in `featureflags.py`), `antithesishq/antithesis-sdk-rust` (the open half of Antithesis: `Sometimes` assertions as a coverage property, the linker-assembled assertion catalog, guidance as a fitness signal, and the no-caching contract on `get_random` that betrays a *branching* rather than replaying simulation), redis `test/` harness, Z3 (`z3.rs` bindings; skim the tactic/solver architecture — treat Z3 itself as a masterclass codebase: it's a high-performance search engine over logic). - **Papers:** "Testing Database Engines via Pivoted Query Synthesis" (OSDI'20), "Finding Logic Bugs via TLP" (OOPSLA'20), Jepsen analyses (pick redis-raft and a graph DB one), "Z3: An Efficient SMT Solver" (TACAS'08), "Cosette: An Automated Prover for SQL" (CIDR'17). - **Build & bench:** add proptest model-checking to the capstone (graph ops vs an in-memory model oracle); build a mini DST harness (simulated clock + fault-injecting IO layer); fuzz your parsers (Cypher + page/SST decoders); use Z3 to verify two of your topic-10 rewrite rules are equivalent (and to find a counterexample when you break one on purpose). - **Capstone M16:** openCypher TCK subset runner as the correctness oracle + DST harness + fuzzers (the reference's `fuzz/` and `tck_done.txt` show the bar). Graduation of the correctness spine. @@ -523,4 +524,16 @@ flowchart TD --- +## 44. E-graphs as a Database: Relational E-matching & egglog + +**Why:** Topic 21 built the e-graph and measured what it repairs; this topic is the sequel, and it belongs in a database course rather than a compilers one, because the fix for the *next* bottleneck came from our literature. E-matching — pattern matching modulo equality — is **60–90% of equality saturation's run time** (POPL'22 §1, citing egg's own measurements), and it is a **conjunctive query**: the e-graph is a set of tables, a pattern is a query, and the *equality constraint* a backtracking matcher checks last is a join key. Measured lane 1 is the whole argument in two columns: on the POPL'22 Figure 2 e-graph (3N e-nodes standing for N²+2N terms) the pattern `f(a, g(a))` has **N matches and costs a backtracking matcher N²+N+1 units of work** — 2,561,601 at N=1600 — while generic join does **5N**, i.e. 8,000, for a measured **21.7×** at that size. And the second table is the honest one: rename the repeated variable and the pattern goes *linear*, every candidate becomes an answer, and generic join is **1.8× slower** — the same result POPL'22 reports in Table 1's `Worst` column (0.76, and 0.03 with index building charged). Then egglog (PLDI'23) takes the last step: stop copying an e-graph into a database whenever you want to match and make the database primary, at which point Datalog's **semi-naive evaluation** applies — measured against a naive re-derivation that finds **20,008 matches and 100,040 probes for 8 new answers**. And SIGMOD'23's Free Join is where the asymptotics get their constants back. + +- **Concepts:** the **relational view of an e-graph** (POPL'22 §3.1 — one tuple per e-node, `R_f` of arity k+1, all ids canonical, and the hashcons invariant restated as a **functional dependency** from the children columns to the id column, §4.3); **structural vs equality constraints** and why a top-down walk can only exploit the first (§2.1), with **linear patterns** as the case where there is nothing to win; **unnesting** a pattern into a conjunctive query (Figure 8's `Aux`/`Compile`), which makes **multi-patterns free**; **conjunctive queries, the AGM bound and fractional edge covers** (the triangle at `M^1.5` against a binary plan's `M²`); **generic join** (Algorithm 1) and its two implementation requirements — intersect in `O(min |R_j.x|)` and reach a residual relation in constant time, which is what the trie index buys; the **complexity results** (Theorem 9 worst-case optimality, Theorem 10's `O(√(|Q(I)|·Π|Rᵢ|))`, which predicts *both* of this topic's lanes) and why NP-completeness (data vs query complexity) does not contradict them; **egglog** as Datalog plus two extensions — user-extensible equality and functions with a **`:merge` expression** — where a function is a *map* enforcing a functional dependency, `:merge` is the conflict policy, `min` is the join of a lattice ordered by worseness, and **`:merge = union` is congruence closure**, not implemented but derived (PLDI'23 §3.2–3.4); `:default` as **get-or-make-set**, which is `EGraph::add` arrived at from the other side; the inflationary consequence operator `T_P↑` and the rebuilding operator `R` (§4.2), including the footnote that egglog rules are **not always monotone**; **semi-naive evaluation** as m delta rules per rule (§4.3, Theorem 4.1), the duplicate derivations it necessarily produces, and its production form — a **timestamp column** plus a `GeConst` constraint that a clustered sort order turns into a binary search rather than a filter; the **engine** as an actual database (a sorted-writes table with a sharded hash index and a merge function, dense/sparse row subsets, a planner with **hypertree decomposition** by min-fill variable elimination and Yannakakis-style message variables, then per-bag join planning), **rebuilding compiled to a rule** and planned by the same planner, and a **union-find that unions by min id** rather than by rank because its real cost is the rebuild it triggers; **Free Join** (SIGMOD'23) — the design space parameterised by relations-and-attributes per join step, the **GHT** that is a hash table at two levels and a trie at one-tuple keys, plans as lists of nodes of subatoms with a **cover**, converting an existing binary plan and **factoring** it, **COLT** (a column-oriented *lazy* trie that materialises a level only when probed), vectorized execution, and the measured **2.94×/9.61× geometric means with a 0.85× minimum**. +- **Read code:** `egraphs-good/egglog` — read it as a database, not as an e-graph library: `core-relations/src/free_join/plan.rs:1-46` (the best short description of a modern join planner in any source file), `core-relations/src/table/mod.rs:1-5` and `:136-152` (the table, and the deliberate ignorance of what a timestamp means), `:445-512` `fast_subset`, `core-relations/src/offsets/mod.rs:333` (`Subset::Dense | Sparse`), `core-relations/src/query.rs:252-256` (semi-naive as a cached plan plus a `GeConst`), `free_join/execute.rs:1418-1560` (the intersect stage, smallest-side-first at `:1464`), `egglog-bridge/src/lib.rs:932-1050` (congruence closure, compiled to rules), `union-find/src/lib.rs` entire (104 lines, and it explains why it declines union-by-rank). Then re-read `~/repos/egg` from topic 21 and note what the two designs share. +- **Papers:** Zhang, Wang, Willsey & Tatlock, "Relational E-matching" (POPL'22 — Figure 2, §2.1's constraint taxonomy, §3.1–3.2, §3.4's Theorems 9 and 10, Table 1 including its `Worst` column); Zhang, Wang, Flatt, Cao, Zucker, Rosenthal, Tatlock & Willsey, "Better Together: Unifying Datalog and Equality Saturation" (PLDI'23 — §3's language tour, §4.2's two operators and footnote 4, §4.3's semi-naive, §5.3's 3.34×/9.27× attribution, §6's two case studies); Wang, Willsey & Suciu, "Free Join: Unifying Worst-Case Optimal and Traditional Joins" (SIGMOD'23 — Figure 1's design space, §3's GHT and plan language, §4.2's COLT, §5's JOB/LSQB evaluation); revisit "egg: Fast and Extensible Equality Saturation" (POPL'21) from topic 21. +- **Build & bench:** lane 1 provided — a minimal e-graph (union-find, hashcons, rebuild to fixpoint) whose internals are visible enough to be walked *and* read as tables, egg's `Bind`/`Compare`/`Scan` VM as the backtracking baseline (with the op index, so the comparison is honest), Figure 8's unnesting, trie indexes, a most-constrained-first variable ordering and generic join — measured on both a non-linear and a linear pattern so the negative result is a column rather than a caveat; implement **semi-naive evaluation** (contracts: the delta rules' union, deduplicated, equals `matches(after) − matches(before)` as sets; 8 answers from a 24-tuple delta; probes at least 10× below the naive re-derivation) and **a left-deep binary-join plan for the triangle multi-pattern** (contracts: same substitution set as generic join; the largest materialised intermediate exceeds 4× the output, and grows as `E²/V` while the answer stays at `(E/V)³`), then measure both against the provided columns. +- **Capstone M44:** the rewrite stage of the planner, priced — replace the capstone's hand-ordered rewrite pass with an e-graph stage whose patterns are matched **relationally** rather than by walking, and report both numbers (plan cost against the hand-ordered pass, match time against a backtracking matcher); timestamp the e-node table and run the saturation loop semi-naively, measuring iterations-to-saturation and total probes against the naive loop on the same rule set; and put one **cyclic** rewrite pattern in the rule set with the binary-join plan measured next to generic join, so the AGM bound is a column rather than a claim. + +--- + - FPGA / SmartNIC / computational storage offload (beyond GPU) diff --git a/PROGRESS.md b/PROGRESS.md index 2379b55..0524a7f 100644 --- a/PROGRESS.md +++ b/PROGRESS.md @@ -4,7 +4,7 @@ Two different things get tracked here, and conflating them is misleading: - **Package** — does `topics/NN-name/` exist and hold up? That means a study guide, four to seven reading guides, `notes.md`, and an experiments crate - whose provided lane runs and whose numbers are recorded. All 44 are built; + whose provided lane runs and whose numbers are recorded. All 45 are built; `./verify.sh` re-derives every one of their measured lanes. - **Studied** — have *I* actually worked through the material and the two exercise lanes? That is a much smaller number, and it is the honest one. @@ -60,6 +60,7 @@ is done. | 41 | On-Chain & Crypto Analytics (graph use case 4/6) | done | todo | | | 42 | Recommendations & Social Graphs (graph use case 5/6) | done | todo | | | 43 | Network & IT-Ops Dependency Graphs (graph use case 6/6) | done | todo | | +| 44 | E-graphs as a Database: Relational E-matching & egglog | done | todo | | ## Capstone milestones (falkordb-rs-next-gen from scratch) @@ -109,6 +110,7 @@ is done. | M41 provenance & identity (incremental FIFO taint queues in the property layer, maintained union-find cluster index, BlockSci-shaped columnar transaction store for scan queries) | 41 | todo | | M42 real-time recommendations (GraphJet-style temporal index segments + doubling edge pools, Pixie random-walk procedure with sub-linear step allocation and early stopping, TAO-shaped association-list API) | 42 | todo | | M43 observability path (trace ingest as an incrementally-maintained dependency graph with sketched edge weights, walk + Ferret localization procedures over the CSR, happened-before join operator with Pivot Tracing pushdown) | 43 | todo | +| M44 relational rewrite stage (e-graph planner pass whose patterns compile to conjunctive queries and run through generic join, a timestamped e-node table driving a semi-naive saturation loop, and one cyclic rewrite pattern measured against a binary-join plan) | 44 | todo | ## Session log diff --git a/README.md b/README.md index 29b6d20..61b0c6a 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ **A self-paced curriculum in database internals, where every claim is measured.** -44 topics, from B-trees to GPU query execution to attack graphs. Each one walks you +45 topics, from B-trees to GPU query execution to attack graphs. Each one walks you through the papers and the production code, then hands you a Rust benchmark that demonstrates the thing being claimed — so you finish with a number you produced yourself, not a fact you read. diff --git a/SESSION-LOG.md b/SESSION-LOG.md index e307467..a221037 100644 --- a/SESSION-LOG.md +++ b/SESSION-LOG.md @@ -9,6 +9,47 @@ Every performance figure quoted below is reproducible with `./verify.sh` (see [README.md](README.md)); timings depend on hardware, everything else is seeded. +## 2026-08-26 — topic 44 + two topic-16 guides — e-matching is a join, and the two testing systems that were only named + +**New topic 44, `E-graphs as a Database: Relational E-matching & egglog`** — the sequel to topic 21, placed here because the fix for equality saturation's bottleneck came out of the database literature. Plus two guides for topic 16, which had been name-dropping Antithesis inside its FoundationDB chapter and referring to property testing without ever reading one. Package: README, four reading guides, `notes.md`, a Rust crate with lane 1 implemented and two lanes stubbed, `FINDINGS.md` row, `verify.sh` lane, `PLAN.md` §44, capstone M44, SUMMARY entries. `check-reading-depth.py --check --all` reads **234/234**. + +**The measured headline, and it is a closed form rather than a curve.** On the POPL'22 Figure 2 e-graph — N constants, one e-class of `g(1..N)`, one of `f(1..N, i_g)`, so **3N e-nodes standing for N²+2N terms** — the pattern `f(a, g(a))` has exactly N matches. Backtracking (egg's `Scan`/`Bind`/`Compare` VM, reimplemented with the `classes_by_op` index so the baseline is not a strawman) does **N² + N + 1** units of work; generic join over the same e-graph read as tables does **5N**. Both counters are exact at every size, which is how the harness is known to be measuring the algorithm: + +``` + N e-nodes matches bt visits bt µs gj probes index µs gj µs speedup + 100 300 100 10101 137.9 500 71.7 24.8 1.43x + 200 600 200 40201 398.9 1000 101.8 39.0 2.83x + 400 1200 400 160401 1119.8 2000 92.4 37.2 8.64x + 800 2400 800 640801 2586.1 4000 180.4 85.0 9.75x + 1600 4800 1600 2561601 10152.5 8000 322.4 145.0 21.72x +``` + +10101 = 10000 + 100 + 1; 500 = 5 × 100 (2N to intersect `a`, 2N for the auxiliary `x`, N for the root). **The speedup lags the work ratio by 14.7×**, and that gap is arithmetic rather than hand-waving: at N = 1600 a visit costs 10152.5 µs / 2,561,601 = **4.0 ns** (a walk down a `Vec`) while a probe costs (145.0 + 322.4) µs / 8,000 = **58.4 ns** with the trie build charged. 320 / 14.7 = 21.8, which is the last row. + +**The negative result is a column, not a caveat.** Rename the repeated variable — `f(a, g(b))`, a *linear* pattern with no equality constraint — and every candidate becomes an answer: bt visits and gj probes converge to N²+N+1 and N²+N+3, and generic join comes out **0.48–0.59×**, i.e. about **1.8× slower**, because it does the same work through a hash lookup instead of a pointer walk. POPL'22 reports its own version: Table 1's `Worst` column is **0.76** for `math` at 217,396 e-nodes without index building and **0.03** in the `+ math 8,205` row with it — a pattern on which their generic join was 33× slower. §5.2 gives the rule in one sentence ("Speedup tends to be greater when the output size is smaller"), and the guide leads with it rather than with the six-orders-of-magnitude headline. + +**Theorem 10 predicts both lanes, which is the reason it is in the guide.** `O(√(|Q(I)| × Π_i |R_i|))` with m = 2 atoms of N tuples: the non-linear pattern has |Q(I)| = N, bound `N^1.5` = **64,000** at N = 1600 against 8,000 measured; the linear one has |Q(I)| = N², bound `N²` = **2,560,000** against 2,561,603 measured — *at* the bound. Worst-case optimality bounds waste, not time. + +**Lane 2 prices naive evaluation without implementing the fix.** 20,000 constants (60,000 tuples), then a delta of 8 constants (24 tuples): the naive re-derivation finds **20,008 matches with 100,040 probes in 11.0 ms**, for 8 new answers. The semi-naive stub's specification is the union of the m delta rules, deduplicated, equalling `matches(after) − matches(before)` as sets — and the guide works out that on this query **each of the 8 answers is derived twice**, once by each delta rule, because every new answer uses one new `f` tuple *and* one new `g` tuple. + +**Lane 3's generator makes the AGM point without needing the stub.** Edges scale with vertices, so for a uniform random directed graph the expected 3-cycle count is `E³/3V³` and each is reported three times (once per rotation) — expected matches `(E/V)³` = **125** at every row, measured 129 / 123 / 123 / 138 while the graph grows 8×. Generic join's probes grow linearly (10,155 → 79,416); the binary plan's intermediate, which the reader implements, is `Σ_v indeg·outdeg` ≈ `E²/V` ≈ **40,000** at the last row for 138 answers. That estimate is labelled an estimate in both README and notes. + +**Tests: 6 provided pass, 4 stubs fail, which is the intended shape.** The load-bearing one is `relational::tests::agree`, which runs both matchers over the same e-graph for the non-linear pattern (60 matches), the linear one (1600) and the triangle multi-pattern, and asserts set equality — without it the timing table compares nothing. `egraph::tests::rebuild_closes_congruence` pins the fixpoint behaviour that `Fig2` depends on. + +**One benchmark bug, caught by the counters disagreeing with the clock.** The first `gj` allocated a `Vec` per intersection key; replacing it with a fixed-size scratch array left every counter identical and took N = 1600 from 310.0 µs to 145.0 µs. Recorded in `notes.md` under surprises, because the general lesson is the useful part: when the work counters and the wall clock disagree, the clock is measuring the allocator. + +**Paper numbers, each read at the section cited.** POPL'22: e-matching is **60–90%** of equality saturation's run time (§1, citing egg's POPL'21 measurements); relational e-matching is ~80 lines inside egg plus a generic-join library "in fewer than 500 lines" against egg's own ~500-line matcher (§5); Table 1 `math`/217,396 without indexing gives best **8,575,830.58**, median **80.84**, worst **0.76**. PLDI'23: at iteration 100 on the `math` suite, `egglogNI` — semi-naive disabled, *same e-graph* — is **3.34×** faster than egg and full egglog is **9.27×** with a slightly larger e-graph (§5.3, footnote 8: M2, 16 GB), which is why the guide attributes 3.34× to joins and only the increment to semi-naive; the points-to case study is **4.96×** over the fastest sound Soufflé encoding, **1.94×** over cclyzer++, **1.59×** over egglogNI (§6.1); Herbie's sound analysis wins **104** benchmarks and the unsound ruleset still wins **135** (§6.2), which the guide states rather than rounding to a win. SIGMOD'23: geometric means **2.94×** over binary join (DuckDB) and **9.61×** over Generic Join, maxima 19.36× and 31.6×, minima **0.85×** (a 17% slowdown) and 2.63×; JOB Q13a at >10 s / 7 s / just over 1 s with a binary intermediate "over 100 million tuples". + +**Anchors, verified line by line against `egraphs-good/egglog` at `e264c37a`.** The finding that shaped the source guide is that the papers understate the codebase: `core-relations` is a database. `plan.rs:1-46` documents a two-phase planner — hypertree decomposition by variable elimination with a min-fill heuristic (`:420` `next_var_to_eliminate`), Yannakakis-style message variables, then per-bag join planning with `PlanStrategy::Gj` or Free Join's `MinCover` (`:32-41`). `table/mod.rs:1-5` says outright that "timestamp" and "merge function" are "abstracted away from the core functionality of the table", and `SortedWritesTable` (`:136-152`) is a row buffer plus a sharded hash index plus one nominated `sort_by` column. That column is what makes semi-naive cheap: `fast_subset` answers `Constraint::GeConst` with a binary search returning a dense offset range (`:497-510`, `:983`) and returns `None` on any other column — a clustered index, and the code says so by declining. `query.rs:252-256` is the delta rule in five lines of doc comment. And `egglog-bridge/src/lib.rs:945` **compiles congruence closure into a rule** — two atoms, planned with `MinCover`, executed by the ordinary join executor — with `:994` a non-incremental variant and `:703`/`:722` choosing between them. + +**Three things the source says that the technique's textbook version does not.** egglog's `union-find/src/lib.rs:6-12` unions **by min id**, and states that this "_does not_ guarantee the same asymptotic complexity as the main techniques in the literature (e.g. union by rank)" — chosen to perturb fewer ids during congruence closure, i.e. tuned for the rebuild it triggers rather than for itself, which is the same class of finding as egg's non-compressing `find(&self)` in topic 21. `plan.rs:41` admits the default Free Join strategies are "not worst-case optimal because [they do] not necessarily pick[] the smallest side to scan". And the module doc names a `JoinStage::fuse` that does not exist under that name; the function on disk is `fuse_single_scans` (`:163`), so the guide cites both. + +**Topic 16 — `reading-hypothesis.md`.** Read against `HypothesisWorks/hypothesis` at `49a797bdf`, whose layout has moved to `hypothesis/src/hypothesis/`. The spine is that Hypothesis shrinks the **choice sequence**, not the value: `ChoiceT = int | str | bool | float | bytes` with per-type constraints (`internal/conjecture/choice.py:60-68`), ordered by shortlex (`shrinker.py:73-94`), with per-type complexity indices from a **zigzag** around `shrink_towards` (`choice.py:306-312`). Worked on real numbers: with `shrink_towards = 0`, index(10) = 19, index(3) = 5, index(−3) = 6, so `[10]` (key `(1,(19,))`) beats `[0,3]` beats `[3,0]` — length first, earliest position next. Two things the source admits and a summary would not: `choice_to_index` is documented as non-injective for floats (`:335-337`, "nothing has blown up - yet"), and the shrink-pass invariant is that *whether* a pass makes progress must be deterministic while *which* progress it makes need not be (`shrinker.py:187-199`) — "fine to try each of N deletions in a random order, not OK to try N random deletions". `find_integer` (`junkdrawer.py:435-470`) was **executed rather than estimated**: the answer 100 costs **16** calls (4 linear + 6 doubling + 6 bisection), not the 17 a hand trace produced. And Hypothesis's swarm testing deviates from Groce et al. deliberately and says so in a comment (`featureflags.py:54-58`): the enable *probability* is drawn up front rather than a fair coin per feature, because all-on and all-off have probability 2^-n in the original model — about one in a million at 20 features. + +**Topic 16 — `reading-antithesis.md`.** The platform is closed, so the chapter reads the open SDK (`antithesishq/antithesis-sdk-rust` at `78c9db5`) and is explicit about the boundary. The load-bearing observation is that the SDK's rules about randomness only make sense for a **branching** simulation, not a replayed one: `random.rs:3-15` forbids both caching a random value and seeding a PRNG from it, giving the same reason for each — the simulation may branch, and both branches would then hold identical values, "which defeats the purpose of branching". Under seeded replay neither rule would be necessary. The rest: `Sometimes` as a **coverage** property rather than a safety one, with the observation that this topic's own `crash_matrix` already has a hand-rolled version (the `None` row at 0.0%, and `TornWriteAccepted`'s 48.8% as the "did we reach the interesting state" number); the assertion catalog assembled by the **linker** via `linkme`'s `#[distributed_slice]` (`assert/mod.rs:20-24`, `:112-124`), which is how an assertion that never ran is still reportable; guidance as a scalar fitness signal (`guidance.rs:197-201`, `:209`) — the same idea as Hypothesis's `target` phase, at fleet scale; and a platform boundary that is exactly three C symbols, `fuzz_json_data` / `fuzz_get_random` / `fuzz_flush`, dlopened from `/usr/lib/libvoidstar.so` (`voidstar_handler.rs:7-18`), with a three-way handler fallback (`internal/mod.rs:57-66`) that keeps an instrumented binary runnable on a laptop. **No Antithesis performance or coverage figure is quoted anywhere in the chapter**, because none of them can be checked from this side; Step 8 says so explicitly. + +**Corrections made while writing.** `GuidanceType` has three variants (`Numeric`, `Boolean`, `Json`), not the two an early draft named. The PLDI'23 paper's repository footnote points at `mwillsey/egg-smol`, which is now `egraphs-good/egglog`. And `FINDINGS.md`'s header date is annotated rather than overwritten: every other row was measured 2026-07-28, topic 44's on 2026-08-26, same machine. + ## 2026-08-08 — topics 34–43 — the last 40 guides, and the rules turned on for the whole book **Final batch of the rollout: topics 34 through 43, 40 guides, 9,163 lines of prose becoming 14,975.** With these the ratchet reads **230 of 230**, and `.github/workflows/book.yml`'s depth job is switched from `--check` (started files only) to `--check --all`, so a new guide that skips the rules now fails CI rather than being quietly exempt. Same contract and method as batches 1–3: one agent per topic on disjoint directories, `tools/check-reading-depth.py` printing *N/N* as the gate, two or three anchors per topic re-verified against the pin afterwards. Every spot-check confirmed the agent. diff --git a/SUMMARY.md b/SUMMARY.md index 9e026c7..148db86 100644 --- a/SUMMARY.md +++ b/SUMMARY.md @@ -141,6 +141,8 @@ - [SQLancer: 450+ bugs from three tiny oracles](topics/16-testing-correctness/reading-sqlancer.md) - [turso's simulator: every failure is a u64 seed](topics/16-testing-correctness/reading-turso-simulator.md) - [Z3 & Cosette: testing every input at once](topics/16-testing-correctness/reading-z3.md) + - [Hypothesis: shrinking a choice sequence, not a value](topics/16-testing-correctness/reading-hypothesis.md) + - [Antithesis: assertions as a search signal, and a simulation that branches](topics/16-testing-correctness/reading-antithesis.md) - [Topic 16 notes — testing & correctness engineering](topics/16-testing-correctness/notes.md) - [Topic 17 — SIMD & Hardware-Conscious Data Processing](topics/17-simd/README.md) - [FastLanes: bit-unpacking at memory bandwidth](topics/17-simd/reading-fastlanes.md) @@ -327,6 +329,12 @@ - [Pivot Tracing: a join operator over causality](topics/43-ops-dependency-graphs/reading-pivot-tracing.md) - [Gray failure: when the system and its users disagree](topics/43-ops-dependency-graphs/reading-gray-failure.md) - [Topic 43 notes — Network & IT-ops dependency graphs](topics/43-ops-dependency-graphs/notes.md) +- [Topic 44 — E-graphs as a Database: Relational E-matching & egglog](topics/44-egraphs-egglog/README.md) + - [Relational e-matching: the pattern is a query, the e-graph is the database](topics/44-egraphs-egglog/reading-relational-ematching.md) + - [egglog: a Datalog engine that happens to be an e-graph](topics/44-egraphs-egglog/reading-egglog-pldi23.md) + - [Reading egglog: the e-graph that is a database engine](topics/44-egraphs-egglog/reading-egglog-source.md) + - [Free Join: the plan space that contains both hash join and generic join](topics/44-egraphs-egglog/reading-free-join.md) + - [Topic 44 notes — e-graphs as a database](topics/44-egraphs-egglog/notes.md) --- diff --git a/resources/codebases.md b/resources/codebases.md index 463f786..5b386f9 100644 --- a/resources/codebases.md +++ b/resources/codebases.md @@ -87,89 +87,93 @@ are worth fetching first. | clone | read at | dated | mentions | origin | |---|---|---|---|---| -| `FalkorDB` | `ccb449a9a` | 2026-07-15 | 282 | [https://github.com/FalkorDB/FalkorDB](https://github.com/FalkorDB/FalkorDB) | -| `redis` | `a176d1225` | 2026-03-24 | 242 | [https://github.com/redis/redis](https://github.com/redis/redis) | -| `postgres` | `701f021` | 2026-07-10 | 226 | [https://github.com/postgres/postgres](https://github.com/postgres/postgres) | -| `duckdb` | `6c0c1a68` | 2026-07-10 | 191 | [https://github.com/duckdb/duckdb](https://github.com/duckdb/duckdb) | -| `rocksdb` | `7c80a5a` | 2026-07-09 | 146 | [https://github.com/facebook/rocksdb](https://github.com/facebook/rocksdb) | -| `neon` | `8f60b04` | 2026-05-25 | 118 | [https://github.com/neondatabase/neon](https://github.com/neondatabase/neon) | -| `GraphBLAS` | `1fd5475` | 2026-02-05 | 104 | [https://github.com/DrTimothyAldenDavis/GraphBLAS](https://github.com/DrTimothyAldenDavis/GraphBLAS) | -| `sqlite` | `951de30` | 2026-07-09 | 83 | [https://github.com/sqlite/sqlite](https://github.com/sqlite/sqlite) | -| `turso` | `dd775bc` | 2026-07-10 | 76 | [https://github.com/tursodatabase/turso](https://github.com/tursodatabase/turso) | -| `datafusion` | `1e77af8` | 2026-07-10 | 75 | [https://github.com/apache/datafusion](https://github.com/apache/datafusion) | -| `hashbrown` | `d69025b` | 2026-07-06 | 69 | [https://github.com/rust-lang/hashbrown](https://github.com/rust-lang/hashbrown) | -| `qdrant` | `44ad62f` | 2026-06-03 | 68 | [https://github.com/qdrant/qdrant](https://github.com/qdrant/qdrant) | -| `valkey` | `8891441ab` | 2026-05-03 | 64 | [https://github.com/valkey-io/valkey](https://github.com/valkey-io/valkey) | -| `memgraph` | `8f87f6a` | 2026-07-09 | 61 | [https://github.com/memgraph/memgraph](https://github.com/memgraph/memgraph) | -| `fjall` | `80cf6bc` | 2026-07-05 | 54 | [https://github.com/fjall-rs/fjall](https://github.com/fjall-rs/fjall) | -| `egg` | `f94c346` | 2026-04-14 | 50 | [https://github.com/egraphs-good/egg](https://github.com/egraphs-good/egg) | -| `LAGraph` | `e2539e2` | 2025-09-08 | 49 | [https://github.com/GraphBLAS/LAGraph](https://github.com/GraphBLAS/LAGraph) | -| `tiflash` | `b5093dd` | 2026-07-09 | 49 | [https://github.com/pingcap/tiflash](https://github.com/pingcap/tiflash) | -| `z3` | `1d425e5` | 2026-07-09 | 49 | [https://github.com/Z3Prover/z3](https://github.com/Z3Prover/z3) | -| `materialize` | `b06b3d6` | 2026-07-10 | 47 | [https://github.com/MaterializeInc/materialize](https://github.com/MaterializeInc/materialize) | -| `lmdb` | `704dc70` | 2026-06-24 | 45 | [https://github.com/LMDB/lmdb](https://github.com/LMDB/lmdb) | -| `clickhouse` | `4d598fb2c` | 2026-07-10 | 42 | [https://github.com/ClickHouse/ClickHouse](https://github.com/ClickHouse/ClickHouse) | -| `leanstore` | `90fcf18` | 2025-09-11 | 42 | [https://github.com/leanstore/leanstore](https://github.com/leanstore/leanstore) | -| `prometheus` | `f282b5c` | 2026-07-10 | 41 | [https://github.com/prometheus/prometheus](https://github.com/prometheus/prometheus) | -| `BlockSci` | `14ccc93` | 2020-11-13 | 40 | [https://github.com/citp/BlockSci](https://github.com/citp/BlockSci) | -| `kuzu` | `89f0263` | 2025-10-10 | 39 | [https://github.com/kuzudb/kuzu](https://github.com/kuzudb/kuzu) | +| `postgres` | `701f021` | 2026-07-10 | 511 | [https://github.com/postgres/postgres](https://github.com/postgres/postgres) | +| `redis` | `a176d1225` | 2026-03-24 | 495 | [https://github.com/redis/redis](https://github.com/redis/redis) | +| `FalkorDB` | `aa75821ab` | 2026-08-25 | 347 | [https://github.com/FalkorDB/FalkorDB](https://github.com/FalkorDB/FalkorDB) | +| `duckdb` | `6c0c1a68` | 2026-07-10 | 334 | [https://github.com/duckdb/duckdb](https://github.com/duckdb/duckdb) | +| `rocksdb` | `7c80a5a` | 2026-07-09 | 299 | [https://github.com/facebook/rocksdb](https://github.com/facebook/rocksdb) | +| `neon` | `8f60b04` | 2026-05-25 | 207 | [https://github.com/neondatabase/neon](https://github.com/neondatabase/neon) | +| `sqlite` | `951de30` | 2026-07-09 | 200 | [https://github.com/sqlite/sqlite](https://github.com/sqlite/sqlite) | +| `GraphBLAS` | `1fd54756ca` | 2026-02-05 | 187 | [https://github.com/DrTimothyAldenDavis/GraphBLAS](https://github.com/DrTimothyAldenDavis/GraphBLAS) | +| `qdrant` | `44ad62f` | 2026-06-03 | 171 | [https://github.com/qdrant/qdrant](https://github.com/qdrant/qdrant) | +| `turso` | `dd775bc` | 2026-07-10 | 170 | [https://github.com/tursodatabase/turso](https://github.com/tursodatabase/turso) | +| `valkey` | `8891441ab` | 2026-05-03 | 155 | [https://github.com/valkey-io/valkey](https://github.com/valkey-io/valkey) | +| `datafusion` | `1e77af8` | 2026-07-10 | 145 | [https://github.com/apache/datafusion](https://github.com/apache/datafusion) | +| `fjall` | `80cf6bc` | 2026-07-05 | 143 | [https://github.com/fjall-rs/fjall](https://github.com/fjall-rs/fjall) | +| `egg` | `f94c346` | 2026-04-14 | 135 | [https://github.com/egraphs-good/egg](https://github.com/egraphs-good/egg) | +| `hashbrown` | `d69025b` | 2026-07-06 | 126 | [https://github.com/rust-lang/hashbrown](https://github.com/rust-lang/hashbrown) | +| `polars` | `f8bcc3d` | 2026-07-10 | 100 | [https://github.com/pola-rs/polars](https://github.com/pola-rs/polars) | +| `leanstore` | `90fcf18` | 2025-09-11 | 96 | [https://github.com/leanstore/leanstore](https://github.com/leanstore/leanstore) | +| `z3` | `1d425e5` | 2026-07-09 | 96 | [https://github.com/Z3Prover/z3](https://github.com/Z3Prover/z3) | +| `memgraph` | `8f87f6a` | 2026-07-09 | 93 | [https://github.com/memgraph/memgraph](https://github.com/memgraph/memgraph) | +| `clickhouse` | `4d598fb2c` | 2026-07-10 | 92 | [https://github.com/ClickHouse/ClickHouse](https://github.com/ClickHouse/ClickHouse) | +| `LAGraph` | `e2539e2` | 2025-09-08 | 91 | [https://github.com/GraphBLAS/LAGraph](https://github.com/GraphBLAS/LAGraph) | +| `lsm-tree` | `8526dd3` | 2026-07-05 | 85 | [https://github.com/fjall-rs/lsm-tree](https://github.com/fjall-rs/lsm-tree) | +| `egglog` | `e264c37a` | 2026-08-25 | 76 | [https://github.com/egraphs-good/egglog](https://github.com/egraphs-good/egglog) | +| `lmdb` | `704dc70` | 2026-06-24 | 71 | [https://github.com/LMDB/lmdb](https://github.com/LMDB/lmdb) | +| `raft-rs` | `ad13f3d` | 2026-05-13 | 69 | [https://github.com/tikv/raft-rs](https://github.com/tikv/raft-rs) | +| `tiflash` | `b5093dd` | 2026-07-09 | 62 | [https://github.com/pingcap/tiflash](https://github.com/pingcap/tiflash) | +| `prometheus` | `f282b5c` | 2026-07-10 | 61 | [https://github.com/prometheus/prometheus](https://github.com/prometheus/prometheus) | +| `materialize` | `b06b3d6` | 2026-07-10 | 56 | [https://github.com/MaterializeInc/materialize](https://github.com/MaterializeInc/materialize) | +| `kuzu` | `89f0263` | 2025-10-10 | 55 | [https://github.com/kuzudb/kuzu](https://github.com/kuzudb/kuzu) | +| `tikv` | `eb8dd65` | 2026-07-09 | 53 | [https://github.com/tikv/tikv](https://github.com/tikv/tikv) | +| `hypothesis` | `49a797bdf` | 2026-08-25 | 50 | [https://github.com/HypothesisWorks/hypothesis](https://github.com/HypothesisWorks/hypothesis) | +| `neo4j` | `eccd584a` | 2026-07-02 | 50 | [https://github.com/neo4j/neo4j](https://github.com/neo4j/neo4j) | +| `go-ycsb` | `f030f99` | 2025-12-31 | 49 | [https://github.com/pingcap/go-ycsb](https://github.com/pingcap/go-ycsb) | +| `tantivy` | `7152d53` | 2026-07-10 | 49 | [https://github.com/quickwit-oss/tantivy](https://github.com/quickwit-oss/tantivy) | +| `BlockSci` | `14ccc93` | 2020-11-13 | 48 | [https://github.com/citp/BlockSci](https://github.com/citp/BlockSci) | +| `ligra` | `8763202` | 2024-02-18 | 46 | [https://github.com/jshun/ligra](https://github.com/jshun/ligra) | +| `pgwire` | `6bb6299` | 2026-06-29 | 46 | [https://github.com/sunng87/pgwire](https://github.com/sunng87/pgwire) | +| `cockroach` | `a7e11788` | 2026-07-06 | 45 | [https://github.com/cockroachdb/cockroach](https://github.com/cockroachdb/cockroach) | +| `usearch` | `9fd6b01` | 2026-05-24 | 45 | [https://github.com/unum-cloud/usearch](https://github.com/unum-cloud/usearch) | +| `benchbase` | `33c0047` | 2025-12-13 | 40 | [https://github.com/cmu-db/benchbase](https://github.com/cmu-db/benchbase) | +| `rayon` | `6d9e94b` | 2026-06-27 | 40 | [https://github.com/rayon-rs/rayon](https://github.com/rayon-rs/rayon) | +| `ALEX` | `4370da6` | 2024-03-12 | 39 | [https://github.com/microsoft/ALEX](https://github.com/microsoft/ALEX) | | `tidesdb` | `810507a` | 2026-07-10 | 39 | [https://github.com/tidesdb/tidesdb](https://github.com/tidesdb/tidesdb) | -| `polars` | `f8bcc3d` | 2026-07-10 | 37 | [https://github.com/pola-rs/polars](https://github.com/pola-rs/polars) | -| `lsm-tree` | `8526dd3` | 2026-07-05 | 35 | [https://github.com/fjall-rs/lsm-tree](https://github.com/fjall-rs/lsm-tree) | -| `neo4j` | `eccd584a` | 2026-07-02 | 35 | [https://github.com/neo4j/neo4j](https://github.com/neo4j/neo4j) | -| `ligra` | `8763202` | 2024-02-18 | 34 | [https://github.com/jshun/ligra](https://github.com/jshun/ligra) | -| `cockroach` | `a7e11788` | 2026-07-06 | 33 | [https://github.com/cockroachdb/cockroach](https://github.com/cockroachdb/cockroach) | -| `slatedb` | `323ed1b` | 2026-07-10 | 32 | [https://github.com/slatedb/slatedb](https://github.com/slatedb/slatedb) | -| `tantivy` | `7152d53` | 2026-07-10 | 32 | [https://github.com/quickwit-oss/tantivy](https://github.com/quickwit-oss/tantivy) | -| `tikv` | `eb8dd65` | 2026-07-09 | 31 | [https://github.com/tikv/tikv](https://github.com/tikv/tikv) | -| `gunrock` | `748f79e` | 2026-02-09 | 27 | [https://github.com/gunrock/gunrock](https://github.com/gunrock/gunrock) | -| `raphtory` | `5d0d286` | 2026-07-21 | 26 | [https://github.com/Pometry/Raphtory](https://github.com/Pometry/Raphtory) | -| `rayon` | `6d9e94b` | 2026-06-27 | 26 | [https://github.com/rayon-rs/rayon](https://github.com/rayon-rs/rayon) | -| `ALEX` | `4370da6` | 2024-03-12 | 24 | [https://github.com/microsoft/ALEX](https://github.com/microsoft/ALEX) | -| `raft-rs` | `ad13f3d` | 2026-05-13 | 24 | [https://github.com/tikv/raft-rs](https://github.com/tikv/raft-rs) | -| `simdjson` | `c783809` | 2026-07-10 | 24 | [https://github.com/simdjson/simdjson](https://github.com/simdjson/simdjson) | -| `splink` | `04189f5` | 2026-07-23 | 24 | [https://github.com/moj-analytical-services/splink](https://github.com/moj-analytical-services/splink) | -| `cudf` | `2f082a7` | 2026-07-10 | 23 | [https://github.com/rapidsai/cudf](https://github.com/rapidsai/cudf) | -| `RediSearch` | `87276ca` | 2026-07-09 | 23 | [https://github.com/RediSearch/RediSearch](https://github.com/RediSearch/RediSearch) | -| `risingwave` | `119de0a` | 2026-07-10 | 23 | [https://github.com/risingwavelabs/risingwave](https://github.com/risingwavelabs/risingwave) | -| `memchr` | `5fdb40c` | 2026-07-07 | 21 | [https://github.com/BurntSushi/memchr](https://github.com/BurntSushi/memchr) | -| `pgwire` | `6bb6299` | 2026-06-29 | 21 | [https://github.com/sunng87/pgwire](https://github.com/sunng87/pgwire) | -| `quickwit` | `a5ad540` | 2026-07-08 | 21 | [https://github.com/quickwit-oss/quickwit](https://github.com/quickwit-oss/quickwit) | -| `foundationdb` | `4c775a9` | 2026-07-10 | 19 | [https://github.com/apple/foundationdb](https://github.com/apple/foundationdb) | -| `gapbs` | `b5e3e19` | 2024-05-11 | 19 | [https://github.com/sbeamer/gapbs](https://github.com/sbeamer/gapbs) | -| `loro` | `b81abfc` | 2026-07-07 | 19 | [https://github.com/loro-dev/loro](https://github.com/loro-dev/loro) | -| `tidb` | `b94006d` | 2026-07-10 | 19 | [https://github.com/pingcap/tidb](https://github.com/pingcap/tidb) | -| `usearch` | `9fd6b01` | 2026-05-24 | 19 | [https://github.com/unum-cloud/usearch](https://github.com/unum-cloud/usearch) | -| `cr-sqlite` | `891fe9e` | 2024-10-25 | 18 | [https://github.com/vlcn-io/cr-sqlite](https://github.com/vlcn-io/cr-sqlite) | -| `SimSIMD` | `63a254f` | 2026-05-23 | 16 | [https://github.com/ashvardanian/SimSIMD](https://github.com/ashvardanian/SimSIMD) | -| `sqlancer` | `af6ae85` | 2026-06-21 | 16 | [https://github.com/sqlancer/sqlancer](https://github.com/sqlancer/sqlancer) | -| `wgpu` | `f945c78` | 2026-07-10 | 15 | [https://github.com/gfx-rs/wgpu](https://github.com/gfx-rs/wgpu) | +| `slatedb` | `323ed1b` | 2026-07-10 | 38 | [https://github.com/slatedb/slatedb](https://github.com/slatedb/slatedb) | +| `cudf` | `2f082a7` | 2026-07-10 | 37 | [https://github.com/rapidsai/cudf](https://github.com/rapidsai/cudf) | +| `gunrock` | `748f79e` | 2026-02-09 | 35 | [https://github.com/gunrock/gunrock](https://github.com/gunrock/gunrock) | +| `memchr` | `5fdb40c` | 2026-07-07 | 35 | [https://github.com/BurntSushi/memchr](https://github.com/BurntSushi/memchr) | +| `SimSIMD` | `63a254f` | 2026-05-23 | 35 | [https://github.com/ashvardanian/SimSIMD](https://github.com/ashvardanian/SimSIMD) | +| `wgpu` | `f945c78` | 2026-07-10 | 34 | [https://github.com/gfx-rs/wgpu](https://github.com/gfx-rs/wgpu) | +| `sqlancer` | `af6ae85` | 2026-06-21 | 33 | [https://github.com/sqlancer/sqlancer](https://github.com/sqlancer/sqlancer) | +| `gapbs` | `b5e3e19` | 2024-05-11 | 32 | [https://github.com/sbeamer/gapbs](https://github.com/sbeamer/gapbs) | +| `raft.tla` | `6ecbdbc` | 2025-02-18 | 30 | [https://github.com/ongardie/raft.tla](https://github.com/ongardie/raft.tla) | +| `RediSearch` | `87276ca` | 2026-07-09 | 30 | [https://github.com/RediSearch/RediSearch](https://github.com/RediSearch/RediSearch) | +| `raphtory` | `5d0d286` | 2026-07-21 | 29 | [https://github.com/Pometry/Raphtory](https://github.com/Pometry/Raphtory) | +| `foundationdb` | `4c775a9` | 2026-07-10 | 28 | [https://github.com/apple/foundationdb](https://github.com/apple/foundationdb) | +| `simdjson` | `c783809` | 2026-07-10 | 28 | [https://github.com/simdjson/simdjson](https://github.com/simdjson/simdjson) | +| `tidb` | `b94006d` | 2026-07-10 | 28 | [https://github.com/pingcap/tidb](https://github.com/pingcap/tidb) | +| `splink` | `04189f5` | 2026-07-23 | 27 | [https://github.com/moj-analytical-services/splink](https://github.com/moj-analytical-services/splink) | +| `quickwit` | `a5ad540` | 2026-07-08 | 26 | [https://github.com/quickwit-oss/quickwit](https://github.com/quickwit-oss/quickwit) | +| `risingwave` | `119de0a` | 2026-07-10 | 25 | [https://github.com/risingwavelabs/risingwave](https://github.com/risingwavelabs/risingwave) | +| `surrealdb` | `9d9a5b0` | 2026-07-02 | 25 | [https://github.com/surrealdb/surrealdb](https://github.com/surrealdb/surrealdb) | +| `crossbeam` | `6b7458d` | 2026-07-10 | 23 | [https://github.com/crossbeam-rs/crossbeam](https://github.com/crossbeam-rs/crossbeam) | +| `cr-sqlite` | `891fe9e` | 2024-10-25 | 21 | [https://github.com/vlcn-io/cr-sqlite](https://github.com/vlcn-io/cr-sqlite) | +| `loro` | `b81abfc` | 2026-07-07 | 20 | [https://github.com/loro-dev/loro](https://github.com/loro-dev/loro) | +| `diamond-types` | `ad48b9c` | 2026-05-29 | 19 | [https://github.com/josephg/diamond-types](https://github.com/josephg/diamond-types) | +| `sqlparser-rs` | `aeb616f` | 2026-07-03 | 19 | [https://github.com/apache/datafusion-sqlparser-rs](https://github.com/apache/datafusion-sqlparser-rs) | +| `influxdb` | `d783411` | 2026-06-17 | 18 | [https://github.com/influxdata/influxdb](https://github.com/influxdata/influxdb) | +| `roaring-rs` | `83caaca` | 2026-04-24 | 18 | [https://github.com/RoaringBitmap/roaring-rs](https://github.com/RoaringBitmap/roaring-rs) | +| `spicedb` | `8422483` | 2026-07-24 | 16 | [https://github.com/authzed/spicedb](https://github.com/authzed/spicedb) | +| `cranelift-jit-demo` | `3e5e9b6` | 2025-11-07 | 15 | [https://github.com/bytecodealliance/cranelift-jit-demo](https://github.com/bytecodealliance/cranelift-jit-demo) | +| `VictoriaMetrics` | `c1e39b2` | 2026-07-10 | 15 | [https://github.com/VictoriaMetrics/VictoriaMetrics](https://github.com/VictoriaMetrics/VictoriaMetrics) | | `automerge` | `c39339d` | 2026-07-10 | 14 | [https://github.com/automerge/automerge](https://github.com/automerge/automerge) | -| `diamond-types` | `ad48b9c` | 2026-05-29 | 14 | [https://github.com/josephg/diamond-types](https://github.com/josephg/diamond-types) | -| `spicedb` | `8422483` | 2026-07-24 | 14 | [https://github.com/authzed/spicedb](https://github.com/authzed/spicedb) | +| `GraphRAG-SDK` | `f42ab3d` | 2026-04-12 | 14 | [https://github.com/FalkorDB/GraphRAG-SDK](https://github.com/FalkorDB/GraphRAG-SDK) | +| `arrow-rs` | `fed7862` | 2026-07-10 | 13 | [https://github.com/apache/arrow-rs](https://github.com/apache/arrow-rs) | | `bloodhound` | `1968388` | 2026-07-24 | 13 | [https://github.com/SpecterOps/BloodHound](https://github.com/SpecterOps/BloodHound) | -| `crossbeam` | `6b7458d` | 2026-07-10 | 13 | [https://github.com/crossbeam-rs/crossbeam](https://github.com/crossbeam-rs/crossbeam) | -| `GraphRAG-SDK` | `f42ab3d` | 2026-04-12 | 13 | [https://github.com/FalkorDB/GraphRAG-SDK](https://github.com/FalkorDB/GraphRAG-SDK) | -| `influxdb` | `d783411` | 2026-06-17 | 13 | [https://github.com/influxdata/influxdb](https://github.com/influxdata/influxdb) | -| `VictoriaMetrics` | `c1e39b2` | 2026-07-10 | 12 | [https://github.com/VictoriaMetrics/VictoriaMetrics](https://github.com/VictoriaMetrics/VictoriaMetrics) | -| `falkordb-rs-next-gen` | `67c71b81` | 2026-07-27 | 10 | [https://github.com/FalkorDB/falkordb-rs-next-gen](https://github.com/FalkorDB/falkordb-rs-next-gen) | -| `raft.tla` | `6ecbdbc` | 2025-02-18 | 9 | [https://github.com/ongardie/raft.tla](https://github.com/ongardie/raft.tla) | -| `surrealdb` | `9d9a5b0` | 2026-07-02 | 9 | [https://github.com/surrealdb/surrealdb](https://github.com/surrealdb/surrealdb) | -| `feldera` | `bb49055` | 2026-07-10 | 7 | [https://github.com/feldera/feldera](https://github.com/feldera/feldera) | -| `RedisBloom` | `ab734fa` | 2026-07-05 | 7 | [https://github.com/RedisBloom/RedisBloom](https://github.com/RedisBloom/RedisBloom) | -| `sqlparser-rs` | `aeb616f` | 2026-07-03 | 6 | [https://github.com/apache/datafusion-sqlparser-rs](https://github.com/apache/datafusion-sqlparser-rs) | -| `falkordb-py` | `ac68e59` | 2026-04-28 | 5 | [https://github.com/FalkorDB/falkordb-py](https://github.com/FalkorDB/falkordb-py) | +| `feldera` | `bb49055` | 2026-07-10 | 13 | [https://github.com/feldera/feldera](https://github.com/feldera/feldera) | +| `falkordb-rs-next-gen` | `9d28bdc6` | 2026-07-29 | 10 | [https://github.com/FalkorDB/falkordb-rs-next-gen](https://github.com/FalkorDB/falkordb-rs-next-gen) | +| `RedisBloom` | `ab734fa` | 2026-07-05 | 9 | [https://github.com/RedisBloom/RedisBloom](https://github.com/RedisBloom/RedisBloom) | +| `cuvs` | `8b97b61` | 2026-07-10 | 7 | [https://github.com/rapidsai/cuvs](https://github.com/rapidsai/cuvs) | +| `differential-dataflow` | `3f279da` | 2026-05-29 | 5 | [https://github.com/TimelyDataflow/differential-dataflow](https://github.com/TimelyDataflow/differential-dataflow) | +| `falkordb-py` | `122df79` | 2026-07-19 | 5 | [https://github.com/FalkorDB/falkordb-py](https://github.com/FalkorDB/falkordb-py) | +| `PGM-index` | `c6fcf3d` | 2024-11-28 | 5 | [https://github.com/gvinciguerra/PGM-index](https://github.com/gvinciguerra/PGM-index) | | `pytorch_geometric` | `1f0661c` | 2026-06-19 | 5 | [https://github.com/pyg-team/pytorch_geometric](https://github.com/pyg-team/pytorch_geometric) | -| `roaring-rs` | `83caaca` | 2026-04-24 | 5 | [https://github.com/RoaringBitmap/roaring-rs](https://github.com/RoaringBitmap/roaring-rs) | -| `arrow-rs` | `fed7862` | 2026-07-10 | 4 | [https://github.com/apache/arrow-rs](https://github.com/apache/arrow-rs) | -| `benchbase` | `33c0047` | 2025-12-13 | 4 | [https://github.com/cmu-db/benchbase](https://github.com/cmu-db/benchbase) | -| `differential-dataflow` | `3f279da` | 2026-05-29 | 4 | [https://github.com/TimelyDataflow/differential-dataflow](https://github.com/TimelyDataflow/differential-dataflow) | -| `RustyTaintChain` | `4e12fd0` | 2021-03-05 | 4 | [https://github.com/TaintChain/RustyTaintChain](https://github.com/TaintChain/RustyTaintChain) | -| `cuvs` | `8b97b61` | 2026-07-10 | 3 | [https://github.com/rapidsai/cuvs](https://github.com/rapidsai/cuvs) | -| `go-ycsb` | `f030f99` | 2025-12-31 | 3 | [https://github.com/pingcap/go-ycsb](https://github.com/pingcap/go-ycsb) | -| `cranelift-jit-demo` | `3e5e9b6` | 2025-11-07 | 2 | [https://github.com/bytecodealliance/cranelift-jit-demo](https://github.com/bytecodealliance/cranelift-jit-demo) | +| `RustyTaintChain` | `4e12fd0` | 2021-03-05 | 5 | [https://github.com/TaintChain/RustyTaintChain](https://github.com/TaintChain/RustyTaintChain) | +| `y-crdt` | `03e14a0` | 2026-06-12 | 3 | [https://github.com/y-crdt/y-crdt](https://github.com/y-crdt/y-crdt) | +| `antithesis-sdk-rust` | `78c9db5` | 2026-06-12 | 2 | [https://github.com/antithesishq/antithesis-sdk-rust](https://github.com/antithesishq/antithesis-sdk-rust) | | `helix-db` | `47191c6` | 2026-07-05 | 2 | [https://github.com/HelixDB/helix-db](https://github.com/HelixDB/helix-db) | -| `PGM-index` | `c6fcf3d` | 2024-11-28 | 2 | [https://github.com/gvinciguerra/PGM-index](https://github.com/gvinciguerra/PGM-index) | | `timely-dataflow` | `15fc7c9` | 2026-06-12 | 2 | [https://github.com/TimelyDataflow/timely-dataflow](https://github.com/TimelyDataflow/timely-dataflow) | diff --git a/topics/16-testing-correctness/README.md b/topics/16-testing-correctness/README.md index 3bd99e8..0baf27e 100644 --- a/topics/16-testing-correctness/README.md +++ b/topics/16-testing-correctness/README.md @@ -161,6 +161,8 @@ query plans for proofs). | [reading-pqs-tlp-papers.md](reading-pqs-tlp-papers.md) | PQS & TLP: solving the test-oracle problem twice | | [reading-jepsen.md](reading-jepsen.md) | Jepsen & elle: isolation anomalies are cycles | | [reading-z3.md](reading-z3.md) | Z3 & Cosette: testing every input at once | +| [reading-hypothesis.md](reading-hypothesis.md) | Hypothesis: shrinking a choice sequence, not a value | +| [reading-antithesis.md](reading-antithesis.md) | Antithesis: assertions as a search signal, and a simulation that branches | ## Capstone M16 diff --git a/topics/16-testing-correctness/reading-antithesis.md b/topics/16-testing-correctness/reading-antithesis.md new file mode 100644 index 0000000..8151ac9 --- /dev/null +++ b/topics/16-testing-correctness/reading-antithesis.md @@ -0,0 +1,558 @@ +# Antithesis: assertions as a search signal, and a simulation that branches + +Antithesis appears in this topic's opening paragraph and then never +again, which is unsatisfying, because it is the one system here whose +core is not readable: the deterministic hypervisor is a commercial +product and there is no source to open. This chapter is about what you +*can* read — the open-source SDK your program links against — and what +that interface proves about the platform behind it. + +The interface turns out to be the interesting part. It is not the +FoundationDB one. A seeded simulator (topic 16's +[FDB](reading-fdb-simulation.md) and [turso](reading-turso-simulator.md) +chapters) asks your program to be deterministic so that a failing run +can be *replayed*. The Antithesis SDK asks for something stronger and +stranger — that your program never remember a random value, and never +seed a PRNG from one — and the reason is that its simulation does not +replay a line, it **branches a tree**. Once you see why the SDK is +written the way it is, the design of the platform is legible from the +outside. + +The second idea worth stealing costs nothing and needs no vendor: an +assertion vocabulary in which `Sometimes` is a first-class kind. A +`Sometimes` assertion is not a safety property, it is a **coverage** +property — it fails when your test campaign never reached an +interesting state — and it is the direct answer to the failure mode +every fault-injection harness eventually has, where the faults quietly +stopped firing and the suite stayed green. + +Anchors are `antithesishq/antithesis-sdk-rust` at the commit +`resources/codebases.md` pins, quoted with the line numbers they occupy +there. Paths are relative to the repository root. Claims about the +platform itself are attributed to the SDK's own documentation, and +flagged where they cannot be checked from this side. + +## The problem in one sentence + +A fault-injecting test harness has two failure modes — it can miss a bug +your system has, and it can *stop exercising* the system while continuing +to pass — and the second one is invisible unless "this interesting thing +must actually happen" is something you can assert, and expensive to fix +unless the search knows which direction is interesting. + +## The concepts, step by step + +### Step 1 — replaying a line versus branching a tree + +> **In:** deterministic simulation as +> [reading-fdb-simulation.md](reading-fdb-simulation.md) built it — one +> seed, one history, replayable. **Out:** the different model the SDK's +> rules imply, and the evidence for it in the source. + +FoundationDB-style DST removes nondeterminism so that a run is a +function of a seed. The value delivered is *replay*: a failure is a +`u64` you can hand to a colleague. + +The Antithesis SDK asks for two things that replay does not require, and +states the reason for both: + +```rust +// lib/src/random.rs, lines 3-15 — the contract on get_random. +// The word to notice is on line 6: branch. + 3 /// Returns a u64 value chosen by Antithesis. + 4 /// + 5 /// You should use this value immediately rather than using it + 6 /// later. If you delay, then it is possible for the simulation + 7 /// to branch in between receiving the random data and using it. + 8 /// These branches will have the same random value, which + 9 /// defeats the purpose of branching. + 10 /// + 11 /// Similarly, do not use the value to seed a pseudo-random + 12 /// number generator. The PRNG will produce a deterministic + 13 /// sequence of pseudo-random values based on the seed, so if the + 14 /// simulation branches, the PRNG will use the same sequence of + 15 /// values in all branches. +``` + +Read that as evidence rather than as advice. Both rules only make sense +if the platform can **snapshot the entire system state and resume it +more than once**, taking different random values down each copy. Under +plain seeded replay, caching a random value or seeding a PRNG from it +would be harmless — the seed determines everything anyway. + +``` + seeded DST (FDB, turso) branching search (what the SDK implies) + + seed ──▶ ●──▶●──▶●──▶● ✗ ●──▶●──┬─▶●──▶● ✗ + one history, replayable │ └─▶●──▶● ✓ + by re-running the seed └─▶●──▶● ✓ + a snapshot resumed several times; + each resumption gets different + randomness FROM THE PLATFORM +``` + +This is why "use it immediately" is a hard rule. If your code draws a +value, stores it, and uses it ten milliseconds later, any branch point +inside those ten milliseconds produces two futures holding the *same* +value — the fork explored nothing. The randomness must be requested at +the moment the decision is made, so that the decision is what forks. + +The SDK's own words for the second half, at +`lib/src/lib.rs:34-35`: doing either of these things "makes it much +harder for the Antithesis platform to control the history of your +program's execution, and also makes it harder for Antithesis to learn +which inputs provided at which times are most fruitful." + +**"Learn"** is the other load-bearing word, and Step 5 is about it. + +### Step 2 — the assertion vocabulary + +> **In:** Step 1's platform. **Out:** the five macros the SDK exports +> and the two independent bits each one sets, which is a cleaner +> vocabulary than `assert!`. + +``` + macro condition must hold must be reached + ──────────────────────────── ────────────────────── ─────────────── + assert_always! every time it runs yes + assert_always_or_unreachable! every time it runs no + assert_sometimes! at least once yes + assert_reachable! — yes + assert_unreachable! — never +``` + +Two independent bits: *what must be true of the condition*, and *whether +the site has to be executed at all*. Ordinary `assert!` fixes the first +to "always" and the second to "don't care", which is why a test suite +can go green while never running the code. + +In the source the second bit is literally a flag called `must_hit`: + +```rust +// lib/src/assert/macros.rs, lines 115-125 — assert_always. The macro is a thin +// wrapper; line 123 is the whole difference from assert_always_or_unreachable. + 115 macro_rules! assert_always { + 116 ($condition:expr, $message:literal$(, $details:expr)?) => { + 117 $crate::assert_helper!( + 118 condition = $condition, + 119 $message, + 120 $(details = $details)?, + 121 $crate::assert::AssertType::Always, + 122 "Always", + 123 must_hit = true + 124 ) + 125 }; +``` + +`assert_always_or_unreachable!` (`macros.rs:151`) is the same macro with +`must_hit = false`, and the doc line above it says the property "will +pass even if the assertion is never encountered". + +Underneath there are only three assertion types — +`AssertType::{Always, Sometimes, Reachability}` (`lib/src/assert/mod.rs:93-96`) +— crossed with `must_hit` and, for reachability, the polarity. The +`message` string is not a comment: the SDK's docs say "Antithesis +generates one test property per unique `message`", so it is the +property's *identity* across the whole campaign (`lib/src/lib.rs:6-8`). + +### Step 3 — `Sometimes` is a coverage property, and it is the useful one + +> **In:** Step 2's table. **Out:** the assertion kind that has no +> equivalent in ordinary testing, and the failure mode it catches — with +> the version you can apply to this topic's own bench today. + +`assert_sometimes!(cond, "…")` passes if `cond` was true **at least +once** anywhere in the test campaign. Nothing in `assert!`-shaped +testing does this, because it is not a property of a run; it is a +property of the *search*. + +What it catches: the harness that stopped working. + +``` + what you wrote what you meant + ────────────── ────────────── + assert_always!(no_data_loss, …) durability holds + assert_sometimes!(crashed_mid_fsync, … AND we actually tried the case + "torn write hit") where it could fail +``` + +Without the second line, a fault injector whose probability drifted to +zero — a config typo, a refactor that stopped threading the fault +handle, a timeout that now fires before the interesting window — leaves +a permanently green suite that tests nothing. Anyone who has run a +crash-injection harness for a year has had this happen. + +This topic already has the measurement that makes the point. The +`crash_matrix` lane reports: + +``` + bug caught rate + None 0 0.0% ← the anti-vacuity check + TornWriteAccepted 2442 48.8% + NoSyncOnCommit 4980 99.6% +``` + +The `None` row is a hand-rolled `Sometimes` assertion: it asserts that +the oracle does *not* fire on a correct implementation. And +`TornWriteAccepted` at 48.8% is the flip side — the harness is reaching +the interesting state only half the time, which is exactly the quantity +a `Sometimes` assertion turns from invisible into reportable. Exercise: +add `sometimes_seen: HashSet<&str>` to `crash_matrix`, record which +fault classes actually fired per seed, and print the ones that never +did. That is the whole idea, and it costs twenty lines. + +### Step 4 — the catalog: assertions the platform knows about but has never seen + +> **In:** Step 3's `must_hit`. **Out:** the mechanism that makes "never +> reached" reportable at all, which is a neat piece of Rust. + +A `Sometimes` assertion that is never executed cannot report itself — +there is no code running to do it. So the SDK registers every assertion +site *at startup*, before any of them runs: + +```rust +// lib/src/assert/mod.rs, lines 20-24 and 32-35 — the catalog and its +// registration. Line 22's attribute is what makes it work. + 20 /// Catalog of all antithesis assertions provided + 21 #[doc(hidden)] + 22 #[distributed_slice] + 23 #[cfg(feature = "full")] + 24 pub static ANTITHESIS_CATALOG: [AssertionCatalogInfo]; + // ... 26-30: the same for the guidance catalog ... + 32 #[cfg(feature = "full")] + 33 pub(crate) static INIT_CATALOG: Lazy<()> = Lazy::new(|| { + 34 for info in ANTITHESIS_CATALOG.iter() { + 35 let f_name: &str = info.function.as_ref(); +``` + +A **distributed slice** (the `linkme` crate) is a static array assembled +by the *linker*: each macro expansion contributes an element from +wherever it appears in the crate graph, and the whole array exists +before `main` runs. Each element carries the assertion's identity and +source location (`mod.rs:112-124`): type, display type, message, class, +function, file, line, column, `must_hit`, id. + +So the platform is told "here are the 340 properties this binary can +report, with their source locations" at startup, and each execution then +reports which of them were *hit* and with what result. The emitted JSON +carries both bits — the doc comment at `mod.rs:341-343` shows three +records for one assertion, differing in `condition` and `hit`. + +That is the piece to steal even if you never use Antithesis: **a +property that was never evaluated must still be enumerable**, or your +coverage report is a report about the code that ran. + +### Step 5 — guidance: telling the search which way is interesting + +> **In:** the "learn which inputs are most fruitful" claim of Step 1. +> **Out:** the channel through which a program tells the search it is +> getting warmer, and its equivalent in the previous chapter. + +Beside the assertion catalog there is a guidance catalog +(`mod.rs:26-30`), and beside the boolean assertions there is a family of +comparison macros (`macros.rs:414-580`): + +``` + assert_always_greater_than! assert_sometimes_greater_than! + assert_always_greater_than_or_equal_to! … _or_equal_to! + assert_always_less_than! assert_sometimes_less_than! + assert_always_less_than_or_equal_to! … _or_equal_to! + assert_always_some! / assert_sometimes_all! (over a set of named clauses) +``` + +These do not just assert; they emit **guidance** — a record whose +`GuidanceType` is `Numeric`, `Boolean` or `Json` +(`lib/src/assert/guidance.rs:197-201`), carrying a `maximize` flag +(`:209`). Where a plain +`assert_always!(queue_len < 1000)` tells the platform only pass or fail, +`assert_always_less_than!(queue_len, 1000, …)` tells it the *margin*, so +a run that reached 998 is known to be more interesting than one that +reached 12, and the search can push in that direction. + +You have just read the same idea in +[reading-hypothesis.md](reading-hypothesis.md) Step 7: Hypothesis's +`target` phase, where a test calls `target(value)` and the engine +mutates toward larger values, with a Pareto front for multiple +objectives. Same mechanism — a scalar fitness signal from inside the +system under test — at two very different scales: one process versus a +fleet, seconds versus days. + +The database-shaped instances of this are worth naming: replication lag, +queue depth, open transaction count, WAL size, time since last +successful fsync, clock skew between nodes. Each is a number your system +already computes, and each is a direction a search would otherwise have +to find by luck. + +### Step 6 — the transport, and why the same binary runs anywhere + +> **In:** Steps 2–5, all of which emit records. **Out:** where those +> records go, and the three-way fallback that keeps instrumented code +> runnable on your laptop. + +```rust +// lib/src/internal/voidstar_handler.rs, lines 7-18 — the entire platform interface + 7 const LIB_NAME: &str = "/usr/lib/libvoidstar.so"; + // ... 8-9 ... + 10 pub struct VoidstarHandler { + 11 // Not used directly but exists to ensure the library is loaded + 12 // and all the following function pointers points to valid memory. + 13 _lib: Library, + 14 // SAFETY: The memory pointed by `s` must be valid up to `l` bytes. + 15 fuzz_json_data: unsafe fn(s: *const c_char, l: size_t), + 16 fuzz_get_random: fn() -> u64, + 17 fuzz_flush: fn(), + 18 } +``` + +Three C symbols, dynamically loaded from a fixed path: push a JSON +record, get a random `u64`, flush. That is the whole boundary between +your instrumented program and the platform. Everything in Steps 2–5 — +assertions, catalog, guidance, lifecycle — is JSON down `fuzz_json_data`, +and Step 1's branching is `fuzz_get_random`. + +And the fallback, which is the part that makes instrumenting worthwhile +even if you never buy anything: + +```rust +// lib/src/internal/mod.rs, lines 57-66 — three environments, one binary + 57 #[cfg(feature = "full")] + 58 fn get_handler() -> Box { + 59 match VoidstarHandler::try_load() { + 60 Ok(handler) => Box::new(handler), + 61 Err(_) => match LocalHandler::new() { + 62 Some(h) => Box::new(h), + 63 None => Box::new(NoOpHandler::new()), + 64 }, + 65 } + 66 } +``` + +Inside the platform, `libvoidstar.so` loads and records go to it. +Outside it, `LocalHandler` writes the same JSON to the file named by +`ANTITHESIS_SDK_LOCAL_OUTPUT` (`mod.rs:54`) — so you get a local +assertion log with the same schema. With neither, `NoOpHandler`, and the +assertions cost approximately nothing. + +`random::get_random` falls back to the Rust standard library outside the +platform (`lib.rs:38-39`), and `AntithesisRng` plugs the same source into +the `rand` ecosystem for whichever `rand` version you already depend on +(`lib.rs:41-51`). So an instrumented program is an ordinary program +everywhere else, which is the only way instrumentation of this kind ever +survives in a codebase. + +### Step 7 — lifecycle: telling the search when the interesting part starts + +> **In:** the branching search of Step 1. **Out:** the two calls that +> shape *where* it spends its budget. + +```rust +// lib/src/lifecycle.rs — two functions, at :37 and :63 + 37 pub fn setup_complete(details: &Value) { + 63 pub fn send_event(name: &str, details: &Value) { +``` + +`setup_complete` says the system is initialised and the workload is +about to begin: booting a five-node cluster is not the part worth +exploring a thousand times, and a branching search that does not know +where setup ends will waste its budget on it. `send_event` marks a named +milestone with a JSON payload during the run. + +The parallel in this repo is exact: topic 0's benchmarking chapter +insists on warmup being excluded from measurement, and this is warmup +being excluded from *search*. Both are the same instruction — do not +spend your budget on the part you already understand. + +### Step 8 — what this chapter can and cannot tell you + +> **In:** Steps 1–7, all sourced from the SDK. **Out:** an explicit line +> between what the source proves and what remains a vendor claim, so you +> can cite this chapter safely. + +What the open-source SDK establishes: + +- The platform supplies randomness on demand and the program is + forbidden from caching it, in language that only makes sense if + execution **branches** (Step 1). +- Assertions are enumerated at link time and reported by identity, so + properties that were never reached are still known (Step 4). +- The program can emit a scalar fitness signal to steer the search + (Step 5). +- The whole interface is three C symbols (Step 6). + +What it does not, and this chapter therefore does not assert: how the +determinism is achieved, what the snapshotting costs, how branches are +scheduled or prioritised, how much of a state space a campaign covers, +or any performance number whatsoever. Those are the closed part. This +repo's rule is that a number you cannot check does not go in a guide, +and none of Antithesis's published figures can be checked from here. + +Which leaves a fair summary: **the ideas are free and the +implementation is not.** `Sometimes` assertions, an enumerable catalog, +guidance signals and a lifecycle marker can all be built into a harness +you already own — Step 3's exercise is the smallest version — and the +deterministic hypervisor underneath cannot. + +## How to read the source (with the concepts in hand) + +The `antithesis-sdk-rust` crate is about 3,200 lines of Rust including +tests; an hour is enough. + +1. `lib/src/lib.rs` module docs first — Steps 1, 5 and 6 in the author's + own words. +2. `lib/src/assert/macros.rs`. Read `assert_always!` (`:115`) and + `assert_always_or_unreachable!` (`:151`) side by side, then + `assert_sometimes!` (`:188`), `assert_reachable!` (`:227`) and + `assert_unreachable!` (`:267`). The `assert_helper!` at `:35`/`:89` + is where the two `cfg` worlds split. +3. `lib/src/assert/mod.rs:20-124` — the catalog, `AssertType`, and + `AssertionCatalogInfo`. Then the doc comment at `:341-343`, which + shows the emitted JSON for one assertion in three states. +4. `lib/src/assert/guidance.rs:195-217` — `GuidanceType`, `maximize`, + and the record shape. +5. `lib/src/internal/mod.rs:57-89` — the handler fallback and the + `LibHandler` trait, then `voidstar_handler.rs` entire (60 lines). +6. `simple/src/main.rs` and `simple/src/rand.rs` — the worked example + program, which is short and shows the intended call sites. + +Then, to make it concrete, instrument this topic's own `dst_run` harness +with `assert_sometimes!`-equivalents and see which of your fault classes +have never fired. + +## Questions (answer in notes.md) + +1. Step 1 argues that "never seed a PRNG from `get_random`" implies + branching. Construct the concrete two-branch scenario in which a + seeded PRNG makes the fork useless, using a KV store's crash-point + choice as the decision. +2. Both `assert_always!` and `assert_always_or_unreachable!` demand the + condition hold whenever evaluated. Give a database example where you + genuinely want `must_hit = false`, and one where accepting it would + hide a real regression. +3. Take the `crash_matrix` lane's five bug rows. Write the `Sometimes` + assertions that would have caught a harness in which the crash + injector silently stopped firing, and say what each one's failure + message should contain to be actionable at 3am. +4. Guidance gives the search a scalar to maximise. Pick three for a + replicated KV store, and for each say what a *maximising* search + would do that a uniform random one would not — including the case + where maximising it is actively unhelpful. +5. The catalog is assembled by the linker (`linkme`). What breaks if an + assertion lives in a crate that is compiled but never linked into the + final binary, and how would you detect that in CI? +6. Compare the failure artefact of the three systems in this topic: a + `u64` seed (FDB/turso), a shrunk choice sequence (Hypothesis), and a + platform-side branch history (Antithesis). Which can you put in a + commit message, which can you replay in CI, and which needs the + vendor? + +## Done when + +Answer each before unfolding it. + +- [ ] You can say what the SDK's rules about randomness prove about the + platform. +
Answer + + `random.rs:3-15` forbids both storing a value for later use and + seeding a PRNG from it, and gives the same reason for both: the + simulation may **branch**, and both branches would then hold identical + values, "which defeats the purpose of branching". Neither rule would + be necessary under plain seeded replay, where the seed determines + everything anyway. So the platform snapshots system state and resumes + it more than once with different randomness — a tree, not a line. + Randomness must be requested at the moment of the decision so that the + decision is what forks. +
+ +- [ ] You can name the two independent bits an Antithesis assertion sets. +
Answer + + What must be true of the condition (`Always`, `Sometimes`, or nothing + for pure reachability — `AssertType` at `assert/mod.rs:93-96`), and + whether the site must be executed at all (`must_hit`, set to `true` at + `macros.rs:123` for `assert_always!` and `false` for + `assert_always_or_unreachable!` at `:151`). Ordinary `assert!` pins + the first to "always" and leaves the second unstated, which is how a + suite goes green while never executing the code. +
+ +- [ ] You can explain why `Sometimes` is a coverage property and give + the failure it catches. +
Answer + + It passes if the condition held at least once across the campaign, so + it is a claim about the *search*, not about any run. It catches the + harness that stopped working — a fault injector whose probability + drifted to zero, a fault handle a refactor stopped threading through — + which otherwise leaves a permanently green suite testing nothing. This + topic's `crash_matrix` already has a hand-rolled version: the `None` + row at 0.0%, which asserts the oracle does not fire on a correct + implementation, and the 48.8% `TornWriteAccepted` rate, which is + exactly the "did we reach the interesting state" quantity. +
+ +- [ ] You can say how a never-executed assertion gets reported. +
Answer + + Every assertion site contributes an `AssertionCatalogInfo` — type, + message, class, function, file, line, column, `must_hit`, id + (`assert/mod.rs:112-124`) — to a `#[distributed_slice]` assembled by + the linker (`:20-24`), which is walked at startup (`:32-35`). The + platform therefore knows every property the binary *can* report before + any of them runs, and each execution reports which were `hit` and with + what `condition`. Without that, a `Sometimes` assertion that never + executes has no code available to report itself. +
+ +- [ ] You can connect guidance to something you have already read. +
Answer + + Guidance is a scalar fitness signal from inside the system under test: + the comparison macros (`macros.rs:414-580`) emit a guidance record — + `Numeric`, `Boolean` or `Json` — with a `maximize` flag + (`guidance.rs:197-209`), so the search learns that a run reaching 998 + is more interesting than one reaching 12. It is Hypothesis's `target` + phase (`reading-hypothesis.md` Step 7) — same idea, one process versus + a fleet. For a database: replication lag, queue depth, open + transaction count, WAL size, clock skew. +
+ +- [ ] You can state the boundary between what the source shows and what + it does not. +
Answer + + The SDK proves the *interface*: on-demand randomness with a + no-caching contract, a link-time assertion catalog, guidance signals, + a lifecycle marker, and a three-symbol boundary + (`fuzz_json_data`, `fuzz_get_random`, `fuzz_flush` — + `voidstar_handler.rs:15-17`). It shows nothing about how determinism + is achieved, what a snapshot costs, how branches are scheduled, or how + much of a state space a campaign covers — and none of the published + figures can be checked from this side, so this chapter quotes none of + them. The ideas are reusable; the hypervisor is not. +
+ +## References + +- The `antithesis-sdk-rust` SDK (`antithesishq/antithesis-sdk-rust`) at the + pinned commit (see the pin table at the end of + [resources/codebases.md](../../resources/codebases.md)). Files read + here: `lib/src/lib.rs`, `lib/src/random.rs`, `lib/src/assert/macros.rs`, + `lib/src/assert/mod.rs`, `lib/src/assert/guidance.rs`, + `lib/src/lifecycle.rs`, `lib/src/internal/mod.rs`, + `lib/src/internal/voidstar_handler.rs`. +- Antithesis's own documentation (`antithesis.com/docs/`), cited by the + SDK's doc comments for the definitions of *test property*, + *workload*, and *triage report*. Treat it as vendor documentation: + useful for the vocabulary, not a source for numbers. +- Jingyu Zhou et al., **"FoundationDB: A Distributed Unbundled + Transactional Key Value Store"**, SIGMOD 2021 — the simulation + testing this platform's founders came from; read + [reading-fdb-simulation.md](reading-fdb-simulation.md) first. +- In this topic: [reading-hypothesis.md](reading-hypothesis.md) (Step + 5's guidance is its `target` phase; Step 3's coverage property is what + its swarm testing is trying to reach), + [reading-turso-simulator.md](reading-turso-simulator.md) (the + open-source system closest to this design). +- Alex Groce et al., **"Swarm Testing"**, ISSTA 2012 — the cheapest way + to make `Sometimes` assertions start passing. diff --git a/topics/16-testing-correctness/reading-hypothesis.md b/topics/16-testing-correctness/reading-hypothesis.md new file mode 100644 index 0000000..6f83e31 --- /dev/null +++ b/topics/16-testing-correctness/reading-hypothesis.md @@ -0,0 +1,664 @@ +# Hypothesis: shrinking a choice sequence, not a value + +This topic's table says property testing is "random ops" plus "an +in-memory model". That is the *idea*. The engineering that makes it +usable on a database is almost entirely about what happens **after** a +failure: a random 200-operation history that breaks your KV store is +not a bug report, it is a haystack. + +Hypothesis — the Python property-testing library, and the one whose +internals are documented rather than folklore — answers this with a +single structural decision: **it does not shrink your values, it shrinks +the sequence of choices your generators made.** Every consequence +follows from that, including the ones that look like unrelated features +(a failure database, a prefix trie over past executions, swarm testing, +targeted search). + +This chapter builds the vocabulary from zero — choice sequence, shortlex +order, complexity index, shrink pass, novel prefix — and works the +orderings on real numbers. Rust readers: `proptest`, which this topic's +exercises use, is a direct descendant of the same design (its integrated +shrinking comes from the same insight), so everything here transfers +except the file paths. + +Anchors are `HypothesisWorks/hypothesis` at the commit +`resources/codebases.md` pins, quoted with the line numbers they occupy +there. Paths are relative to `hypothesis/src/hypothesis/`. + +## The problem in one sentence + +If shrinking is a method on the *type* — a `shrink()` for lists, another +for integers, another for your `Op` enum — then it cannot see the +constraints that made a value valid, it composes badly under `flat_map`, +and every new generator needs a new shrinker; whereas if the thing being +shrunk is the *choice sequence the generators consumed*, one shrinker +works for every generator that will ever be written, and re-running the +test is what checks validity. + +## The concepts, step by step + +### Step 1 — what a property test is, and where the pain is + +> **In:** nothing. **Out:** the two halves of a property test, and the +> reason the second half is where the engineering went. + +A **property-based test** has two parts: a **generator**, which produces +inputs, and a **property**, which must hold for all of them. Running it +is a search for a counterexample. + +The classical (QuickCheck) design makes both type-directed: a +`Gen` produces a `T`, and a paired `Shrink` produces "smaller" +`T`s to try when one fails. Three things go wrong at database scale: + +1. **Composition.** Generate a list of length `n`, then generate `n` + indices into it. Shrinking the list to a shorter one invalidates + the indices, and the shrinker for the pair has no way to know. +2. **Constraints.** "A `put` whose key was previously written" is a + validity condition the type does not carry, so a type-directed + shrinker produces mostly invalid candidates. +3. **Cost.** Every generator you write needs a shrinker written and + maintained beside it, and the ones people skip are exactly the + domain types where shrinking would help most. + +**Integrated shrinking** is the fix: shrink the *input to generation* +rather than its output, and re-run generation to get a value that is +valid by construction. Hypothesis's realisation of it is Steps 2–5. + +### Step 2 — the choice sequence + +> **In:** Step 1's integrated shrinking. **Out:** the object Hypothesis +> actually manipulates, and the reason it is typed rather than a byte +> string. + +Every draw a strategy makes goes through one of five primitives, and +the record of those draws is the **choice sequence**: + +```python +# internal/conjecture/choice.py, lines 60-68 — the whole vocabulary of a test case + 60 ChoiceT: TypeAlias = int | str | bool | float | bytes + 61 ChoiceConstraintsT: TypeAlias = ( + // ... 62–67: the union of the five per-type constraint TypedDicts ... + 68 ChoiceTypeT: TypeAlias = Literal["integer", "string", "boolean", "float", "bytes"] +``` + +Five types, and each drawn value carries the **constraints** it was +drawn under — for an integer, `min_value`, `max_value`, `weights` and +`shrink_towards` (`choice.py:31-35`). A test case *is* a list of +`(type, value, constraints)` triples, and running the test is replaying +that list into the strategies. + +Two properties matter later: + +- **It is generic.** Nothing in the sequence knows about your `Op` enum; + your enum's generator turned into integer and boolean draws. +- **It is typed.** Earlier versions of Hypothesis shrank an underlying + *byte* stream, so a "small" change at the byte level could rewrite + every subsequent draw. Recording the choices themselves means a change + to one choice is a change to one decision. + +### Step 3 — "simpler" is shortlex, and it is exactly defined + +> **In:** the choice sequence of Step 2. **Out:** the total order the +> shrinker is minimising, with the arithmetic done on a real pair of +> candidates. + +**Shortlex order** compares two sequences by length first and, among +equal lengths, lexicographically. Hypothesis's key: + +```python +# internal/conjecture/shrinker.py, lines 73-94 — sort_key. The definition is +# lines 91-94; the docstring above it gives the three reasons. + 73 def sort_key(nodes: Sequence[ChoiceNode]) -> tuple[int, tuple[int, ...]]: + 74 """Returns a sort key such that "simpler" choice sequences are smaller than + 75 "more complicated" ones. + 76 + 77 We define sort_key so that x is simpler than y if x is shorter than y or if + 78 they have the same length and map(choice_to_index, x) < map(choice_to_index, y). + // ... 79–90: the three justifications, quoted in the prose below ... + 91 return ( + 92 len(nodes), + 93 tuple(choice_to_index(node.value, node.constraints) for node in nodes), + 94 ) +``` + +The docstring's three reasons are worth having in your head: a shorter +sequence means "we had to make fewer decisions"; a lower index at the +same position means a simpler value there; and earlier choices are +prioritised because they "potentially get used in more places" — a +choice made early can change how many later choices exist at all. + +`choice_to_index` is Step 4. Taking it on trust for one moment, work +three candidates with `shrink_towards = 0` and no bounds: + +``` + sequence length indices sort_key + [10] 1 (19,) (1, (19,)) + [0, 3] 2 (0, 5) (2, (0, 5)) + [3, 0] 2 (5, 0) (2, (5, 0)) + + shortlex: [10] < [0, 3] < [3, 0] +``` + +`[10]` wins despite containing the largest number in the table, because +it is one decision instead of two. And `[0, 3]` beats `[3, 0]` because +the *first* position is simpler — the third justification, made +concrete. A failing test that shrinks to `[10]` really is a simpler +story than one that shrinks to `[3, 0]`, even though "10" looks bigger +than "3". + +### Step 4 — the complexity index, and the zigzag + +> **In:** Step 3's use of `choice_to_index`. **Out:** what "simpler" +> means *within* one type, worked, and why it depends on the +> constraints. + +`choice_to_index` maps a value to its position in a per-type ordering, +0 being simplest, and **the ordering depends on the constraints the +value was drawn under**: + +```python +# internal/conjecture/choice.py, lines 325-337 — choice_to_index's contract. +# Line 330 is the one to hold on to: the index is relative to constraints. + 325 def choice_to_index(choice: ChoiceT, constraints: ChoiceConstraintsT) -> int: + 326 # This function takes a choice in the choice sequence and returns the + 327 # complexity index of that choice from among its possible values, where 0 + 328 # is the simplest. + 329 # + 330 # Note that the index of a choice depends on its constraints. The simplest value + 331 # (at index 0) for {"min_value": None, "max_value": None} is 0, while for + 332 # {"min_value": 1, "max_value": None} the simplest value is 1. + 333 # + 334 # choice_from_index inverts this function. An invariant on both functions is + 335 # that they must be injective. Unfortunately, floats do not currently respect + 336 // ... 336–337: floats do not satisfy the invariant; "nothing has blown up - yet" ... +``` + +Note the admission on 335–337 rather than glossing it: floats are not +injective under this mapping, and the comment says so. That is the +honest state of the code, and it is the kind of thing a guide that +described "what the technique usually does" would never surface. + +For unbounded integers the ordering is a **zigzag** outward from +`shrink_towards`: + +```python +# internal/conjecture/choice.py, lines 306-312 — the whole ordering, five lines + 306 def zigzag_index(value: int, *, shrink_towards: int) -> int: + 307 # value | 0 1 -1 2 -2 3 -3 4 + 308 # index | 0 1 2 3 4 5 6 7 + 309 index = 2 * abs(shrink_towards - value) + 310 if value > shrink_towards: + 311 index -= 1 + 312 return index +``` + +Work it, with `shrink_towards = 0`: + +``` + value 10 3 0 -3 + 2|a − v| 20 6 0 6 + v > a? yes yes no no + index 19 5 0 6 +``` + +which is where Step 3's table came from — 19 for `10`, 5 for `3`. And +positive-before-negative is not an accident of the formula, it is the +formula's *purpose*: `-3` and `3` are equally far away, and a reader +staring at a minimal failing example would rather see `3`. + +The constraint-dependence in the comment is the payoff of Step 2's +typed sequence. Drawn under `min_value=1`, the simplest integer is `1`, +not `0` — so shrinking never proposes a value the generator could not +have produced. Constraint satisfaction, for free, forever. + +### Step 5 — shrink passes, and the invariant that makes them terminate + +> **In:** the order of Steps 3–4. **Out:** the shrinker's loop, and the +> one rule every pass must obey. + +```python +# internal/conjecture/shrinker.py, lines 162-171 — the loop, from the class docstring + 162 The shrinker keeps track of a value shrink_target which represents the + 163 current best known ConjectureData object satisfying the predicate. + 164 It refines this value by repeatedly running *shrink passes*, which are + 165 methods that perform a series of transformations to the current shrink_target + 166 and evaluate the underlying test function to find new ConjectureData + 167 objects. If any of these satisfy the predicate, the shrink_target + 168 is updated automatically. Shrinking runs until no shrink pass can + 169 improve the shrink_target, at which point it stops. +``` + +A **shrink pass** is any function that proposes new choice sequences and +tests them; the target moves whenever a proposal is shortlex-smaller and +still fails. The end state is a **local minimum for every pass** — not a +global minimum, which nobody can promise. + +Then the rule that makes "run every pass until none makes progress" +terminate: + +```python +# internal/conjecture/shrinker.py, lines 187-199 — the determinism invariant + 187 In aid of this goal, the main invariant that a shrink pass much + 188 satisfy is that whether it makes progress must be deterministic. + 189 It is fine (encouraged even) for the specific progress it makes + 190 to be non-deterministic, but if you run a shrink pass, it makes + 191 no progress, and then you immediately run it again, it should + 192 never succeed on the second time. This allows us to stop as soon + 193 as we have run each shrink pass and seen no progress on any of + 194 them. + 195 + 196 This means that e.g. it's fine to try each of N deletions + 197 or replacements in a random order, but it's not OK to try N random + 198 deletions (unless you have already shrunk at least once, though we + 199 don't currently take advantage of this loophole). +``` + +Read the distinction on 196–199 twice, because it is subtle and it is +the reason the loop has a stopping condition at all: *which* of the N +deletions you try first may be random; *whether you tried all N* may +not. Randomising the order is a heuristic; randomising the coverage +turns "no pass made progress" into "no pass happened to make progress +this time", and the fixpoint disappears. + +### Step 6 — `find_integer`, the primitive underneath + +> **In:** Step 5's passes, which need to answer "how far can I go?". +> **Out:** the search Hypothesis uses for every such question, and its +> cost, worked. + +Most passes reduce to: find the largest `n` such that some predicate +holds — delete `n` choices, lower a value by `n`, and so on. + +```python +# internal/conjecture/junkdrawer.py, lines 435-470 — find_integer. The linear +# prefix on 445-447 is the part that is not textbook. + 435 def find_integer(f: Callable[[int], bool]) -> int: + 436 """Finds a (hopefully large) integer such that f(n) is True and f(n + 1) is + 437 False. + 438 + 439 f(0) is assumed to be True and will not be checked. + 440 """ + // ... 441–444: comment explaining the linear prefix ... + 445 for i in range(1, 5): + 446 if not f(i): + 447 return i - 1 + // ... 448–457: exponential probe upward, doubling hi ... + 458 while f(hi): + 459 lo = hi + 460 hi *= 2 + // ... 462–463: binary search between lo and hi ... + 464 while lo + 1 < hi: + 465 mid = (lo + hi) // 2 + 466 if f(mid): + 467 lo = mid + 468 else: + 469 hi = mid + 470 return lo +``` + +Every call to `f` is a **full test execution**, so the call count is the +cost. Work two cases: + +``` + answer n = 2: f(1) ✓ f(2) ✓ f(3) ✗ → 3 calls + answer n = 100: linear f(1) f(2) f(3) f(4) all ✓ → 4 + probe f(5) f(10) f(20) f(40) f(80) ✓, + f(160) ✗ → 6 (lo=80, hi=160) + bisect 120 ✗ 100 ✓ 110 ✗ 105 ✗ + 102 ✗ 101 ✗ → 6 (lo=100) + ───────────────────────────────────────────────── + 16 calls +``` + +The doubling gets logarithmic behaviour for large answers; the linear +prefix on 445–447 exists because, as the comment says, "it's very hard +to win big when the result is small. If the result is 0 and we try 2 +first then we've done twice as much work as we needed to!" A pure +binary search would be asymptotically identical and measurably worse, +because small answers are the common case. + +### Step 7 — the phases, and why a failure is sticky + +> **In:** generation and shrinking as separate activities. **Out:** the +> engine's actual state machine, and the feature that matters most in CI. + +```python +# _settings.py, lines 145-172 — the six phases, in the order they run + 145 explicit = "explicit" # run @example-decorated cases + 150 reuse = "reuse" # "previous test cases will be reused" + 155 generate = "generate" # generate new test cases + 160 target = "target" # "test cases will be mutated for targeting" + 165 shrink = "shrink" # shrink failing cases + 170 explain = "explain" # attempt to explain the failure +``` + +`reuse` is the one to notice. Hypothesis keeps a **database** of the +choice sequences that previously failed (by default `.hypothesis/`), and +replays them first. So a bug found once at 3am by seed luck is +re-checked on every subsequent run, and the fix is verified against the +exact case that broke — without anyone having to copy a counterexample +into the test file by hand. + +That is the same property this topic's `crash_matrix` lane gets by +printing `first seed`, and the same one FoundationDB-style DST gets from +a replayable seed: **a failure must survive the process that found it.** +Three different mechanisms, one requirement. + +`target` is Hypothesis's version of *targeted property-based testing*: a +test can call `target(value)` to say "bigger is more interesting", and +the engine mutates toward it (the optimiser is +`internal/conjecture/optimiser.py`, with a Pareto front in `pareto.py` +for the multi-objective case). Keep that in view for +[reading-antithesis.md](reading-antithesis.md), where the same idea +appears as *guidance* and drives a fleet instead of a loop. + +### Step 8 — the DataTree: don't re-run a prefix you have already seen + +> **In:** the generate phase of Step 7. **Out:** the structure that +> stops generation from repeating itself, which is a database structure. + +```python +# internal/conjecture/datatree.py, lines 546-556 — what it is for + 546 class DataTree: + 547 """ + 548 A DataTree tracks the structured history of draws in some test function, + 549 across multiple ConjectureData objects. + 550 + 551 This information is used by ConjectureRunner to generate novel prefixes of + 552 this tree (see generate_novel_prefix). A novel prefix is a sequence of draws + 553 which the tree has not seen before, and therefore the ConjectureRunner has + 554 not generated as an input to the test function before. +``` + +A trie over executions: each node a drawn choice, each leaf a conclusion +(`Status.VALID`, etc.) or a `Killed` marker meaning "there is more below +here but it is not worth exploring" (`datatree.py:567-571`). +`generate_novel_prefix` walks it to produce a prefix that has never been +run. + +Two things a database person should notice. First, this is a +**prefix index with pruning** — the same shape as a trie index in topic +2, used for deduplication instead of lookup. Second, it makes the search +*stateful across test cases*: a plain QuickCheck loop is memoryless and +will happily draw the same small case fifty times, which is why "10,000 +examples" in one system is not comparable to "10,000 examples" in +another. + +### Step 9 — swarm testing, and the deviation from the paper + +> **In:** the generator of Step 1. **Out:** a bias that finds bugs +> uniform generation cannot, and an honest reading of how Hypothesis +> actually implements it. + +```python +# strategies/_internal/featureflags.py, lines 21-35 — the technique, and the twist + 21 class FeatureFlags: + 22 """Object that can be used to control a number of feature flags for a + 23 given test run. + 24 + 25 This enables an approach to data generation called swarm testing ( + 26 see Groce, Alex, et al. "Swarm testing." Proceedings of the 2012 + 27 International Symposium on Software Testing and Analysis. ACM, 2012), in + 28 which generation is biased by selectively turning some features off for + 29 each test case generated. When there are many interacting features this can + 30 find bugs that a pure generation strategy would otherwise have missed. + 31 + 32 FeatureFlags are designed to "shrink open", so that during shrinking they + 33 become less restrictive. This allows us to potentially shrink to smaller + 34 test cases that were forbidden during the generation phase because they + 35 required disabled features. +``` + +**Swarm testing** (Groce et al., ISSTA 2012): instead of drawing every +operation from the same distribution every time, disable a random subset +of features for the whole test case. The reason it works is a fact about +distributions, not about bugs — if a bug needs 30 consecutive `delete`s +and `delete` has probability 1/5 per op, uniform generation will +effectively never produce it, whereas a test case in which `put` is +disabled entirely produces it immediately. + +Now the deviation, which the code states and the paper does not: + +```python +# strategies/_internal/featureflags.py, lines 54-58 — not the paper's model + 54 # In the original swarm testing paper they turn features on or off + 55 # uniformly at random. Instead we decide the probability with which to + 56 # enable features up front. This can allow for scenarios where all or + 57 # no features are enabled, which are vanishingly unlikely in the + 58 # original model. +``` + +With n features and independent fair coins, "all features on" has +probability 2^-n — at n = 10, about 1 in 1024, and at n = 20 about 1 in +a million. Hypothesis draws an enable-probability first, so the +all-on and all-off corners have real mass. That is a deliberate +distributional change, documented in a comment, and it is the sort of +thing to imitate when you write your own generator: say what +distribution you chose and why. + +"Shrink open" (lines 32–35) is the other half. During shrinking the +flags become *less* restrictive, so a minimal example may use features +that were disabled when the bug was found. Without it, swarm testing +would trade a better search for worse counterexamples. + +### Step 10 — stateful testing: where this meets a database + +> **In:** everything above, which is about generating *values*. +> **Out:** the generator shape you actually want for a storage engine, +> and its relationship to this topic's DST harness. + +```python +# stateful.py, lines 300-309 — the model-based interface + 300 class RuleBasedStateMachine(metaclass=StateMachineMeta): + 301 """A RuleBasedStateMachine gives you a structured way to define state machines. + 302 + 303 The idea is that a state machine carries the system under test and some supporting + 304 data. This data can be stored in instance variables or + 305 divided into Bundles. The state machine has a set of rules which may read data + 306 from bundles (or just from normal strategies), push data onto + 307 bundles, change the state of the machine, or verify properties. + 308 At any given point a random applicable rule will be executed. + 309 """ +``` + +A **rule** is a permitted operation; a **bundle** is a named pool of +values produced by earlier rules, so a rule can consume a key that some +earlier `put` created rather than a key drawn from nowhere. That single +mechanism is what makes generated histories *interesting* against a +storage engine: without it, almost every `get` misses. + +And now the important observation for this topic. A rule-based state +machine is the same object as the DST harness in +[reading-fdb-simulation.md](reading-fdb-simulation.md) and +[reading-turso-simulator.md](reading-turso-simulator.md), with two +differences: + +``` + rule-based state machine deterministic simulation + what is generated a sequence of operations ops + faults + schedules + what is controlled the operations only clock, disk, network, threads + the oracle a model in the same process model + invariants + minimisation shrink passes to a fixpoint replay the seed, then hand-cut +``` + +The column on the right controls more, and it is the reason a simulator +finds bugs a property test cannot. The column on the left *minimises*, +and it is the reason a property test's failures are cheap to act on. +Neither subsumes the other, which is why turso's simulator has a shrink +step and why this topic's exercise list asks you to build one. + +## How to read the source (with the concepts in hand) + +An afternoon, bottom-up, in this order: + +1. `internal/conjecture/choice.py` whole (637 lines) — Steps 2 and 4. + The `choice_to_index` / `choice_from_index` pair is the file. +2. `internal/conjecture/shrinker.py:73-94` (`sort_key`), then the + `Shrinker` class docstring `:150-282` — read it as documentation, it + is the best available explanation of the design. +3. `internal/conjecture/junkdrawer.py:435-470` (`find_integer`), then + pick any one pass in `shrinker.py` and follow it into + `internal/conjecture/shrinking/`. +4. `internal/conjecture/datatree.py:546-620` — the docstring includes + a drawn example of the tree growing. +5. `internal/conjecture/engine.py`, the phase driver, for how Step 7's + phases are sequenced. +6. `strategies/_internal/featureflags.py` (about 90 lines) and + `stateful.py:300-450`. + +If you write Rust: read `proptest`'s `strategy/traits.rs` and +`test_runner/` afterwards and match up the vocabulary. The design is the +same; the choice sequence is called something else. + +## Questions (answer in notes.md) + +1. Compute `sort_key` for the choice sequences `[0, 0, 5]` and `[7, 2]` + with `shrink_towards = 0`, and say which the shrinker prefers. + Then construct a pair where your intuition and shortlex disagree, and + decide which of you is wrong. +2. `choice_to_index` depends on the constraints the value was drawn + under. Give a concrete example — a bounded integer draw — where + ignoring the constraints would make the shrinker propose an invalid + test case, and say what the engine would do with it. +3. `find_integer` costs one test execution per call to `f`. For a + 200-operation failing history where the answer is "delete 150 of + them", how many executions does one pass cost? What does that imply + about shrinking a test whose single run takes 50 ms? +4. The determinism invariant (Step 5) forbids "try N random deletions". + Write a shrink pass that violates it, and describe the symptom a user + would see — not the theory, the symptom. +5. Take this topic's `crash_matrix` bug table. `TornWriteAccepted` is + caught by 48.8% of seeds. Design a swarm-testing bias over the + operation mix that should raise that number, predict the new rate, + then implement and measure it. +6. A `RuleBasedStateMachine` over your KV store versus the DST harness + of `dst_run`: name one bug class each finds that the other cannot, + and say what it would cost to close the gap in either direction. + +## Done when + +Answer each before unfolding it. + +- [ ] You can explain integrated shrinking without using the word + "integrated". +
Answer + + The shrinker manipulates the **choice sequence** — the record of every + primitive draw a generator made, with the constraints it was drawn + under — and then *re-runs generation* on the modified sequence. So a + shrunk value is valid by construction, no per-type shrinker is + written, and constraints such as `min_value=1` are respected + automatically because they are part of the recorded draw + (`choice.py:325-332`). The alternative — shrinking the output value — + needs one shrinker per type and cannot see the constraints that made + the value legal. +
+ +- [ ] You can compute `sort_key` and explain each of its two components. +
Answer + + `sort_key = (len(nodes), tuple(choice_to_index(v, constraints)))` + (`shrinker.py:91-94`): shortlex — length first, then per-choice + complexity indices lexicographically. With `shrink_towards = 0`, + `[10]` has key `(1, (19,))`, `[0, 3]` has `(2, (0, 5))` and `[3, 0]` + has `(2, (5, 0))`, so `[10] < [0,3] < [3,0]`. Length dominates because + a shorter sequence means fewer decisions were made; earlier positions + dominate within a length because early choices influence how many + later choices exist. +
+ +- [ ] You can compute the zigzag index of a value and say why the + ordering is not simply by magnitude. +
Answer + + `index = 2·|shrink_towards − value|`, minus one if `value > + shrink_towards` (`choice.py:306-312`). With `shrink_towards = 0`: + `0 → 0`, `3 → 5`, `−3 → 6`, `10 → 19`. It is not magnitude order + because `3` and `−3` are equidistant and the tie has to be broken — + and it is broken toward the positive value, because a minimal + counterexample reading `3` is easier to think about than one reading + `−3`. The centre is `shrink_towards`, not zero, which is how + "year 2000 is simpler than year 0" is expressed for datetimes. +
+ +- [ ] You can state the invariant every shrink pass must satisfy and why + it exists. +
Answer + + Whether a pass *makes progress* must be deterministic + (`shrinker.py:187-194`): if it runs, makes no progress, and is + immediately run again, it must not then succeed. Which progress it + makes may be random. Without this, "run every pass; stop when none + made progress" is not a termination condition, because a pass that + samples randomly might have succeeded had it sampled differently. The + code spells out the legal version: try N deletions *in a random + order*, never N *random* deletions (`:196-199`). +
+ +- [ ] You can say what the DataTree buys and name the data structure it + is. +
Answer + + It is a **trie over test executions** (`datatree.py:546-556`): nodes + are drawn choices, leaves are conclusions or `Killed` markers meaning + "do not explore below here". `generate_novel_prefix` uses it to emit a + prefix the runner has never executed, so generation does not + rediscover the same small cases, and exhausted subtrees are pruned. It + makes the search stateful across examples, which is why example counts + are not comparable between property-testing libraries. +
+ +- [ ] You can say how Hypothesis's swarm testing differs from the paper + it cites, and why. +
Answer + + Groce et al. (ISSTA 2012) turn each feature on or off by an + independent uniform coin. Hypothesis instead draws the *enable + probability* up front (`featureflags.py:54-58`), so runs where all or + no features are enabled — probability 2^-n each in the original model, + about one in a million at 20 features — have real mass. The flags also + "shrink open" (`:32-35`): during shrinking they become less + restrictive, so the minimal example may use features that were + disabled when the bug was found, which keeps the biased search from + degrading the counterexample. +
+ +- [ ] You can place property testing next to deterministic simulation + rather than choosing between them. +
Answer + + A `RuleBasedStateMachine` generates *operations* against a model + oracle and minimises the failure to a fixpoint. A DST harness + additionally controls the clock, disk, network and scheduler, so it + can generate *faults and interleavings* a property test cannot reach — + and it replays from a seed rather than shrinking. So DST finds a + strictly larger bug class, and property testing hands you a smaller + report. This is why turso's simulator grew a shrink step, and why this + topic asks for both. +
+ +## References + +- `HypothesisWorks/hypothesis` at the pinned commit (see the pin table + at the end of [resources/codebases.md](../../resources/codebases.md)). + Files read here, under `hypothesis/src/hypothesis/`: + `internal/conjecture/choice.py`, `shrinker.py`, `junkdrawer.py`, + `datatree.py`, `_settings.py`, `strategies/_internal/featureflags.py`, + `stateful.py`. +- David R. MacIver, Zac Hatfield-Dodds et al., **"Hypothesis: A new + approach to property-based testing"**, Journal of Open Source + Software 4(43), 2019 — the citable overview; the design rationale + lives in the source and on hypothesis.works. +- Alex Groce, Chaoqiang Zhang, Eric Eide, Yang Chen, John Regehr, + **"Swarm Testing"**, ISSTA 2012 — Step 9's technique, and the model + Hypothesis deliberately does not use. +- Andrea Löscher, Konstantinos Sagonas, **"Targeted Property-Based + Testing"**, ISSTA 2017 — the `target` phase of Step 7. +- Koen Claessen, John Hughes, **"QuickCheck: A Lightweight Tool for + Random Testing of Haskell Programs"**, ICFP 2000 — the type-directed + design Step 1 is arguing with. +- In this topic: [reading-antithesis.md](reading-antithesis.md) (the + same ideas at fleet scale), + [reading-turso-simulator.md](reading-turso-simulator.md) and + [reading-fdb-simulation.md](reading-fdb-simulation.md) (Step 10's + right-hand column). diff --git a/topics/44-egraphs-egglog/README.md b/topics/44-egraphs-egglog/README.md new file mode 100644 index 0000000..3b3870d --- /dev/null +++ b/topics/44-egraphs-egglog/README.md @@ -0,0 +1,353 @@ +# Topic 44 — E-graphs as a Database: Relational E-matching & egglog + +Topic 21 built the e-graph and measured the thing it repairs: a +hand-ordered rewriter that answers `(a*2)/2` with `(a << 1) / 2` and +stops. This topic is the sequel, and it belongs in a database course +rather than a compilers one — because the fix for the *next* bottleneck +turned out to be ours. E-matching, which the egg paper measured at +**60–90% of equality saturation's run time** (POPL'22 §1, citing +Willsey et al.), is a **conjunctive query**. The e-graph is a database. +The pattern is a query. The right algorithm was published in the +database literature and is called **generic join**. + +Then egglog (PLDI'23) took the last step: stop maintaining an e-graph +that gets copied into a database whenever you want to match, and make +the database the primary structure — with Datalog's semi-naive +evaluation on top, so an iteration only looks at what changed. + +```mermaid +graph LR + P["pattern
f(a, g(a))"] -->|"Fig 8: unnest"| Q["conjunctive query
Q(root,a) ← R_f(root,a,x), R_g(x,a)"] + E["e-graph
e-nodes + union-find"] -->|"§3.1: one tuple per e-node"| D["database
R_f, R_g, …"] + Q --> J["generic join
variable-at-a-time"] + D --> J + J --> S["substitutions"] + J -.->|"egglog: make the DB primary,
add semi-naive"| SN["only the new tuples"] +``` + +## The problem, measured (bench lane 1, provided — runs today) + +`cargo run --release --bin ematch_bench` — the e-graph of POPL'22 +Figure 2 (N constants, one e-class of `g(1)..g(N)`, one e-class of +`f(1,i_g)..f(N,i_g)`, so **3N e-nodes** standing for **N² + 2N terms**), +matched against `f(a, g(a))` two ways: egg's backtracking VM, and the +same pattern compiled to a conjunctive query and run with generic join. + +``` +-- lane 1: f(a, g(a)) — one equality constraint, N matches -- + Q(?0, a) <- R_f(?0, a, ?1), R_g(?1, a) + variable ordering: [a, ?1, ?0] + + N e-nodes matches bt visits bt µs gj probes index µs gj µs speedup + 100 300 100 10101 137.9 500 71.7 24.8 1.43x + 200 600 200 40201 398.9 1000 101.8 39.0 2.83x + 400 1200 400 160401 1119.8 2000 92.4 37.2 8.64x + 800 2400 800 640801 2586.1 4000 180.4 85.0 9.75x + 1600 4800 1600 2561601 10152.5 8000 322.4 145.0 21.72x +``` + +**There are N matches and the backtracking matcher does N² + N + 1 units +of work to find them** — 2,561,601 at N = 1600, against 1600 answers. +The join does 5N: 8,000. Both columns are exact, not approximate; the +generators are seeded and the counters count the same unit (one e-node +stepped over, or one key looked at in an intersection). + +The reason is the whole topic in one line. The pattern `f(a, g(a))` +carries two kinds of constraint, and backtracking can only use one of +them early: + +- a **structural constraint** — the root is an `f`, its second child is + a `g` — which is about the *shape* of the pattern; +- an **equality constraint** — both occurrences of `a` must land in the + same e-class — which backtracking cannot check until it has walked far + enough to bind both, i.e. after it has already built the candidate. + +So the walk enumerates every `f(i, g(j))` and throws away the N² − N +pairs where `i ≠ j`. The relational view has no such distinction: +after unnesting, `a` is simply a variable occurring in two atoms, which +is to say a **join key**, and a join algorithm's entire job is to not +enumerate the non-matching pairs. + +## When the join loses (same lane, second table) + +``` +-- lane 1: f(a, g(b)) — linear pattern, N^2 matches -- + Q(?0, a, b) <- R_f(?0, a, ?1), R_g(?1, b) + variable ordering: [?1, ?0, a, b] + + N e-nodes matches bt visits bt µs gj probes index µs gj µs speedup + 100 300 10000 10101 29.2 10103 12.8 48.4 0.48x + 400 1200 160000 160401 423.4 160403 41.9 714.7 0.56x + 1600 4800 2560000 2561601 6476.3 2561603 175.9 11290.4 0.56x +``` + +Rename the second `a` to `b` and the pattern becomes **linear** — no +variable occurs twice, so there is no equality constraint left to +exploit. Now every candidate the walk builds *is* a match: N² work for +N² answers, which is optimal, and the join has nothing to win. It does +the same N² + N + 3 probes, pays for a trie it did not need, and comes +out **1.8× slower**. + +This is not a defect in the implementation; it is the shape of the +result, and the paper reports it too. POPL'22 Table 1's "Worst" column +is **0.03** in the `+ math 8,205` row — that is, with index building +charged, there was a pattern on which their generic join came out +**33× slower** than egg's matcher. §5.2 says why in one sentence — "Speedup tends to be greater when the output +size is smaller". A dense output means backtracking wastes nothing. +The technique's win is *avoided* work, so where there is no waste there +is no win. + +Keep both tables in view. The interesting engineering question is never +"is generic join faster" but "how much of this query's candidate space +is thrown away", and that is a property of the pattern and the data. + +## Step 1 — the e-graph is already a database + +POPL'22 §3.1: every e-node with symbol `f` and arity k becomes one tuple +of a relation `R_f` of arity k+1 — the e-class id that contains it, +then its children, all canonicalised through the union-find. + +``` + e-graph (Figure 2) database + ───────────────── ──────── + R_f: | id | arg1 | arg2 | R_g: | id | arg1 | + i_f: { f(1,i_g) … f(N,i_g) } | i_f | 1 | i_g | | i_g | 1 | + i_g: { g(1) … g(N) } | i_f | 2 | i_g | | i_g | 2 | + 1..N: { 1 } … { N } | … | … | … | | … | … | + | i_f | N | i_g | | i_g | N | +``` + +Nothing is invented in the translation: the e-graph's own invariant +("no two e-nodes with the same symbol and children") is a **functional +dependency** from the children columns to the id column (§4.3), and +canonical ids are why nested patterns join directly on the auxiliary +variable instead of needing an extra join against the equivalence +relation (§3.2). + +## Step 2 — the pattern is a conjunctive query + +Figure 8's `Aux` gives every non-variable subpattern a fresh variable +and emits one atom for it: + +``` + Aux(f(p1..pk)) = v ~ R_f(v, v1..vk), A1..Ak where Aux(pi) = vi ~ Ai + Aux(x) = x ~ [] (a variable is itself) + + f(a, g(a)) ⇒ Q(root, a) ← R_f(root, a, x), R_g(x, a) +``` + +`x` is the structural constraint ("the second child is a `g`-class") and +`a` is the equality constraint ("both positions are the same class"). +In the query they are the same kind of thing — a variable shared by two +atoms — which is precisely why one algorithm can exploit both. This is +also why **multi-patterns are free** (§1): several patterns sharing +variables is just more atoms in one body, and lane 3's triangle is +exactly that. + +## Step 3 — generic join, and why it is variable-at-a-time + +A binary-join plan processes two relations at a time and materialises an +intermediate. Generic join (Algorithm 1, from Ngo et al.) processes one +*variable* at a time: intersect the values every atom allows for it, +then recurse. + +``` + for a ∈ R_f.arg1 ∩ R_g.arg1 ← the equality constraint, up front + for x ∈ R_f(_, a, x).x ∩ R_g(x, a).x + for root ∈ R_f(root, a, x).root + output (root, a) +``` + +Two requirements make the bound hold (§2.3): the intersection must cost +`O(min_j |R_j.x|)` — iterate the smallest set, probe the others — and a +residual relation like `R_f(v, y)` must be reachable in constant time, +which is what the **trie** index buys (Figure 5). Our +`relational.rs::gj` does both, and the 5N in the table is the receipt: +2N to intersect `a`, 2N for `x`, N for `root`. + +The payoff is a bound no backtracking algorithm has: run time linear in +the **AGM bound** of the query, the tight worst-case output size derived +from a fractional edge cover of the query hypergraph. For the triangle +query with |R| = |S| = |T| = M, the AGM bound is M^1.5 while a binary +plan's intermediate can reach M² — lane 3's exercise. + +## Step 4 — the loop, and the tuples it should not look at again + +Equality saturation runs the same queries against a database that only +grows. Naive evaluation re-derives every old match on every iteration; +**semi-naive** evaluation expands each rule into one *delta rule* per +body atom, ranging that atom over the new tuples and the rest over +everything (PLDI'23 §4.3, Algorithm 1): + +``` + A :- A₁, …, A_m ⇒ A :- A₁, …, ΔA_j, …, A_m for each j +``` + +Lane 2 prices the version we do not want: + +``` +-- lane 2: one more iteration of saturation — re-derive, or take the delta -- + e-graph 60000 tuples + delta of 24 tuples (8 new constants) + + evaluation matches probes µs + naive 20008 100040 11004.8 + semi-naive STUB - - +``` + +Twenty-four new tuples arrived and the naive iteration re-derived +**20,008 matches** at a cost of 100,040 probes. Eight of those matches +were new. That ratio is the PLDI'23 microbenchmark in miniature: §5.3 +measures egglog against egg on the `math` suite for 100 iterations and +reports **3.34×** for the non-incremental egglog (better joins alone) +and **9.27×** with semi-naive turned on. + +The mechanism in the real system is a column. Every row carries a +timestamp, and a delta rule is the same cached plan with one extra +constraint (`core-relations/src/query.rs:252`): + +> "an egglog rule is compiled once into a `CachedPlan` and then added to +> a fresh `RuleSet` each iteration with timestamp constraints (e.g. +> `GeConst` on the focus atom) that select only new tuples." + +If you have read topic 4, you have met this before: a monotonically +increasing sequence number per row, and readers that ask for "everything +since". `GeConst` is a range predicate over a sorted column. + +## Production shape — egglog's `core-relations` + +egglog is no longer "an e-graph library with a query engine bolted on". +Read the crate list and it is a database: tables with sorted writes, +hash indexes, a query planner, an execution engine, a union-find. +Anchors are `egraphs-good/egglog` at the commit pinned in +`resources/codebases.md`. + +| piece | where | what to notice | +|---|---|---| +| query planner | `core-relations/src/free_join/plan.rs:1-45` | two phases: **hypertree decomposition** (variable elimination with a min-fill heuristic, Yannakakis-style bags) then per-bag join planning | +| plan strategies | `plan.rs:32-38` | `PlanStrategy::Gj` is textbook generic join; `PureSize`/`MinCover` are **Free Join**, which "degenerates to a hash join" when a cover is a whole atom | +| the table | `core-relations/src/table/mod.rs:1-5` | "timestamp" and "merge function" are deliberately *outside* the table: it is a general sorted-write table, and the e-graph semantics live above it | +| semi-naive | `core-relations/src/query.rs:252-256` | one cached plan + a `GeConst` timestamp constraint per iteration | +| union-find | `union-find/src/lib.rs:1-12` | **union by min id**, not by rank — chosen to perturb fewer ids during congruence closure, and the crate says outright that it gives up the textbook asymptotics | + +That last row is the one to sit with. Two independent implementations +(egg's `unionfind.rs`, egglog's `union-find`) both decline the textbook +optimisation, for reasons that only exist because this union-find is +inside an e-graph. + +## Reading guides + +1. [reading-relational-ematching.md](reading-relational-ematching.md) — POPL'22: e-matching is a conjunctive query, and generic join answers it in worst-case optimal time. +2. [reading-egglog-pldi23.md](reading-egglog-pldi23.md) — PLDI'23: Datalog ∪ equality saturation, `:merge` as a lattice, and semi-naive evaluation over a congruence. +3. [reading-egglog-source.md](reading-egglog-source.md) — the implementation: tables, timestamps, the planner's two phases, and rebuilding as a query. +4. [reading-free-join.md](reading-free-join.md) — SIGMOD'23: why worst-case optimal joins lost to binary joins in practice, and the plan space that contains both. + +## Experiments + +``` +cd experiments +cargo test # 6 provided tests pass; 4 fix the contract for your stubs +cargo run --release --bin ematch_bench +``` + +- `egraph.rs` (PROVIDED) — union-find, hashcons, e-class map, rebuild to + fixpoint. Small enough to read in one sitting, which is the point: + both matchers work on the same visible structure. +- `pattern.rs` (PROVIDED) — Figure 8's unnesting, `Pat` → `Query`. +- `backtrack.rs` (PROVIDED) — egg's `Bind`/`Compare`/`Scan` VM, with + the op index, so the baseline is a real strategy and not a strawman. +- `relational.rs` (PROVIDED) — e-graph → tables, trie indexes, + most-constrained-first variable ordering, generic join. +- `semi_naive.rs` (stub, lane 2) — `delta_matches`: the m delta rules, + and the deduplication they require. +- `binary_join.rs` (stub, lane 3) — a left-deep hash-join plan for the + triangle multi-pattern, reporting its largest intermediate. + +Lane 3 today (generic join only; the binary-join column is your stub): + +``` + V E matches gj probes gj µs bj intermediate bj probes bj µs + 200 1000 129 10155 94.0 STUB - - + 400 2000 123 20163 198.3 STUB - - + 800 4000 123 39865 353.8 STUB - - + 1600 8000 138 79416 839.5 STUB - - +``` + +Note what the generator does: edges scale with vertices, so the answer +size does not move while the graph grows 8×. For a uniform random +directed graph on V vertices with E edges, the expected number of +3-cycles is `E³/3V³`, and each is reported three times (once per +rotation), so the expected match count is `(E/V)³` — **125** for every +row here, against a measured 123–138. Generic join's work grows +linearly in E and the answer does not grow at all. + +The column you are going to fill is the one that makes the point. A +binary plan must first join two edge relations on `y`, materialising +`Σ_v indeg(v)·outdeg(v)` tuples — about `E²/V` for this generator, so +roughly **40,000** at the last row, to return 138 answers. That is an +arithmetic estimate from the generator, not a measurement; lane 3 turns +it into one. + +## Exercises + +1. Implement both stubs until all 10 tests pass and lanes 2–3 print. +2. **Find the crossover.** Lane 1's two patterns are the extremes. Build + an e-graph where `f(a, g(a))` has a *tunable* match density (make + only a fraction p of the `f` e-nodes agree with a `g` child) and + sweep p. At what selectivity does generic join stop paying? Compare + your answer with POPL'22 §5.2's explanation. +3. **The ordering is the plan.** `relational::plan` is one heuristic. + Force the reverse ordering and re-run lane 1: any ordering is still + worst-case optimal, so what exactly got worse, and by how much? +4. **Index amortisation.** The `index µs` column is charged on every + call. In a saturation loop it would not be. Cache the tries across + iterations, invalidate only the relations that changed, and re-run + lane 2 — this is the difference between POPL'22's `+`/`−` rows in + Table 1, and the reason egglog stopped copying the e-graph into a + database at all. +5. **Congruence as a rule.** Rebuilding is congruence closure; in a + relational engine it is a query: `R_f(i, x), R_f(j, x) ⇒ i = j` for + a unary `f`. Write it as a rule over your database, run it to + fixpoint, and check it agrees with `EGraph::rebuild`. Then measure + which is faster on the Figure 2 graph, and say why. +6. **Free Join by hand.** For the triangle query, write the plan that + uses one atom as a *cover* and probes the other two (SIGMOD'23 §4), + and compare its probe count with both generic join and your binary + plan. Which of the three is worst-case optimal, and which is fastest + here? + +## Cross-topic threads + +- **Topic 21 → 44.** Topic 21's `eqsat_bench` shows *why* an e-graph; + this topic shows what it costs to search one. The `Bind`/`Compare` VM + measured here is the same `machine.rs` that guide reads. +- **Topic 10 / 11 ↔ 44.** Join ordering, cardinality-driven plan choice, + hash join build/probe, worst-case optimal joins: the entire content of + this topic is topic 10's optimizer and topic 11's operators, applied + to a workload that is not SQL. `plan.rs`'s min-fill variable + elimination is a join-order search with a different objective. +- **Topic 27 (streaming / IVM) ↔ 44.** Semi-naive evaluation *is* + incremental view maintenance for a monotone query, and the delta rules + are the same expansion DBSP derives for a join. Different literature, + identical algebra. +- **Topic 4 (LSM) ↔ 44.** Row timestamps + `GeConst` = sequence numbers + + "everything since". Deferred rebuilding = deferred compaction. +- **Topic 13 (graph engines) ↔ 44.** Lane 3's triangle query is the + triangle count from topic 24, run by the join engine instead of by a + graph kernel. The AGM bound is the reason a graph database and a + relational one converge on the same algorithm here. +- **Topic 16 (testing) ↔ 44.** An e-graph saturated over sound rewrite + rules is a generator of provably equivalent queries — which is an + oracle. See the metamorphic testing table in topic 16. + +## Capstone M44 — the rewrite stage, priced + +- [ ] Replace the capstone planner's hand-ordered rewrite pass with an + e-graph stage, and match its patterns relationally rather than by + walking. Report both: plan cost against the hand-ordered pass, and + match time against a backtracking matcher. +- [ ] Timestamp the e-node table and run the saturation loop + semi-naively. Measure iterations-to-saturation and total probes + against the naive loop, on the same rule set. +- [ ] One cyclic pattern in the rule set (a join-shaped rewrite over + three atoms), with the binary-join plan measured next to generic + join so the AGM bound is not a claim but a column. diff --git a/topics/44-egraphs-egglog/experiments/Cargo.lock b/topics/44-egraphs-egglog/experiments/Cargo.lock new file mode 100644 index 0000000..13df5b5 --- /dev/null +++ b/topics/44-egraphs-egglog/experiments/Cargo.lock @@ -0,0 +1,134 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "cfg-if" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" + +[[package]] +name = "egraph-db-experiments" +version = "0.1.0" +dependencies = [ + "rand", + "rand_chacha", +] + +[[package]] +name = "getrandom" +version = "0.2.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ff2abc00be7fca6ebc474524697ae276ad847ad0a6b3faa4bcb027e9a4614ad0" +dependencies = [ + "cfg-if", + "libc", + "wasi", +] + +[[package]] +name = "libc" +version = "0.2.189" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2" + +[[package]] +name = "ppv-lite86" +version = "0.2.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "85eae3c4ed2f50dcfe72643da4befc30deadb458a9b590d720cde2f2b1e97da9" +dependencies = [ + "zerocopy", +] + +[[package]] +name = "proc-macro2" +version = "1.0.107" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.47" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "rand" +version = "0.8.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e058c7de0b26af77780c769414d6257830bb240f3c38477dbc2c16e5f54d6d4c" +dependencies = [ + "libc", + "rand_chacha", + "rand_core", +] + +[[package]] +name = "rand_chacha" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88" +dependencies = [ + "ppv-lite86", + "rand_core", +] + +[[package]] +name = "rand_core" +version = "0.6.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" +dependencies = [ + "getrandom", +] + +[[package]] +name = "syn" +version = "2.0.119" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "872831b642d1a07999a962a351ed35b955ea2cfc8f3862091e2a240a84f17297" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + +[[package]] +name = "wasi" +version = "0.11.1+wasi-snapshot-preview1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b" + +[[package]] +name = "zerocopy" +version = "0.8.56" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "556764e583adb45a9f8d413c2a147fa7e8d821e48e12b14fd560b607998b75eb" +dependencies = [ + "zerocopy-derive", +] + +[[package]] +name = "zerocopy-derive" +version = "0.8.56" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f2ab42fc20575779bd240faa45f94a74256f755c0fa9e89f0ede20d91d0cdfc1" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] diff --git a/topics/44-egraphs-egglog/experiments/Cargo.toml b/topics/44-egraphs-egglog/experiments/Cargo.toml new file mode 100644 index 0000000..3f944a4 --- /dev/null +++ b/topics/44-egraphs-egglog/experiments/Cargo.toml @@ -0,0 +1,11 @@ +[package] +name = "egraph-db-experiments" +version = "0.1.0" +edition = "2021" + +[dependencies] +rand = "0.8" +rand_chacha = "0.3" + +[profile.release] +debug = true diff --git a/topics/44-egraphs-egglog/experiments/src/backtrack.rs b/topics/44-egraphs-egglog/experiments/src/backtrack.rs new file mode 100644 index 0000000..81b995a --- /dev/null +++ b/topics/44-egraphs-egglog/experiments/src/backtrack.rs @@ -0,0 +1,184 @@ +//! Backtracking e-matching: the algorithm every e-graph library shipped before +//! relational e-matching, reproduced faithfully enough to be worth timing. +//! +//! It is de Moura and Bjorner's declarative algorithm (POPL'22 Figure 3, +//! reproduced from their 2007 paper) compiled to egg's four-instruction virtual +//! machine so that the comparison in lane 1 is against a real implementation +//! strategy rather than against a set-of-substitutions strawman: +//! +//! egg src/machine.rs:24-29 enum Instruction { Bind, Compare, Lookup, Scan } +//! egg src/machine.rs:66-74 Scan iterates every e-class +//! egg src/pattern.rs:300-304 classes_for_op short-circuits the scan +//! +//! `Lookup` (a whole ground subterm resolved in one hashcons probe) is the one +//! instruction we leave out: none of this topic's patterns contain a ground +//! subterm, so it would never be emitted. +//! +//! The shape of the cost is the point. `Bind` walks *every* e-node of the right +//! symbol in an e-class and pushes its children into registers; `Compare` — the +//! equality constraint — can only run once both registers are filled. So a +//! pattern like `f(a, g(a))` binds all N g-e-nodes under each of the N f-e-nodes +//! before rejecting N^2 - N of the pairs it built. + +use crate::egraph::{EGraph, Id, Sym}; +use crate::pattern::{PatV, VarId}; +use std::cell::Cell; +use std::collections::HashMap; + +#[derive(Clone, Debug)] +pub enum Ins { + /// Enumerate candidate e-classes for a root register, through the op index. + Scan { out: usize, op: Option }, + /// For each `op` e-node in the e-class in register `class`, write its + /// children into registers `out..out+arity`. + Bind { + class: usize, + op: Sym, + out: usize, + arity: usize, + }, + /// The equality constraint, checked when the second occurrence is reached. + Compare { a: usize, b: usize }, +} + +pub struct Program { + pub ins: Vec, + pub n_regs: usize, + /// Register holding each query variable (usize::MAX if the variable is not + /// bound by these patterns). + pub var_reg: Vec, + pub root_regs: Vec, +} + +/// Compile numbered patterns into a straight-line program. Variables are bound +/// at their first occurrence and compared at every later one — the earliest a +/// backtracking matcher can check an equality constraint. +pub fn compile(pats: &[PatV], n_vars: usize, root_vars: &[VarId]) -> Program { + let mut p = Program { + ins: vec![], + n_regs: 0, + var_reg: vec![usize::MAX; n_vars], + root_regs: vec![], + }; + for (i, pat) in pats.iter().enumerate() { + let root = p.n_regs; + p.n_regs += 1; + p.root_regs.push(root); + // The root's auxiliary variable is answered by the root register. + p.var_reg[root_vars[i]] = root; + let op = match pat { + PatV::App(op, _) => Some(*op), + PatV::Var(_) => None, + }; + p.ins.push(Ins::Scan { out: root, op }); + emit(&mut p, pat, root); + } + p +} + +fn emit(p: &mut Program, pat: &PatV, reg: usize) { + match pat { + PatV::Var(v) => { + if p.var_reg[*v] == usize::MAX { + p.var_reg[*v] = reg; + } else { + p.ins.push(Ins::Compare { + a: p.var_reg[*v], + b: reg, + }); + } + } + PatV::App(op, args) => { + let base = p.n_regs; + p.n_regs += args.len(); + p.ins.push(Ins::Bind { + class: reg, + op: *op, + out: base, + arity: args.len(), + }); + for (i, a) in args.iter().enumerate() { + emit(p, a, base + i); + } + } + } +} + +/// Run the program. `visits` counts units of work: one per e-node a `Bind` +/// steps over and one per e-class a `Scan` steps over — the same accounting +/// [`crate::relational`] uses for generic join, so the two are comparable. +pub fn search( + g: &EGraph, + prog: &Program, + visits: &Cell, + out: &mut dyn FnMut(&[Id]), +) { + // The op index, built once — this is egg's `classes_by_op`, and both + // matchers are entitled to it. + let mut roots: HashMap, Vec> = HashMap::new(); + for ins in &prog.ins { + if let Ins::Scan { op, .. } = ins { + roots.entry(*op).or_insert_with(|| match op { + Some(s) => g.classes_with_op(*s), + None => g.class_ids().collect(), + }); + } + } + let mut regs = vec![0 as Id; prog.n_regs]; + exec(g, &prog.ins, &roots, &mut regs, visits, out); +} + +fn exec( + g: &EGraph, + ins: &[Ins], + roots: &HashMap, Vec>, + regs: &mut Vec, + visits: &Cell, + out: &mut dyn FnMut(&[Id]), +) { + let Some((head, rest)) = ins.split_first() else { + out(regs); + return; + }; + match head { + Ins::Scan { out: o, op } => { + for &c in &roots[op] { + visits.set(visits.get() + 1); + regs[*o] = c; + exec(g, rest, roots, regs, visits, out); + } + } + Ins::Bind { + class, + op, + out: base, + arity, + } => { + let c = regs[*class]; + for n in g.nodes(c) { + if n.op != *op || n.children.len() != *arity { + continue; + } + visits.set(visits.get() + 1); + for (i, &ch) in n.children.iter().enumerate() { + regs[base + i] = ch; + } + exec(g, rest, roots, regs, visits, out); + } + } + Ins::Compare { a, b } => { + if g.find(regs[*a]) == g.find(regs[*b]) { + exec(g, rest, roots, regs, visits, out); + } + } + } +} + +/// Substitutions for the query's head variables, in head order. +pub fn matches(g: &EGraph, prog: &Program, head: &[VarId], visits: &Cell) -> Vec> { + let mut found = vec![]; + search(g, prog, visits, &mut |regs| { + found.push(head.iter().map(|&v| regs[prog.var_reg[v]]).collect()); + }); + found +} diff --git a/topics/44-egraphs-egglog/experiments/src/bin/ematch_bench.rs b/topics/44-egraphs-egglog/experiments/src/bin/ematch_bench.rs new file mode 100644 index 0000000..f0ce192 --- /dev/null +++ b/topics/44-egraphs-egglog/experiments/src/bin/ematch_bench.rs @@ -0,0 +1,259 @@ +//! ematch_bench — the same pattern, matched as a graph walk and as a join. +//! +//! cargo run --release --bin ematch_bench + +use egraph_db_experiments::{ + backtrack, binary_join, + gen::{db_delta, edge_graph, Fig2}, + pattern::{compile, number, papp, pvar, Query}, + relational::{self, db_tuples, plan, to_database, Database}, + semi_naive, +}; +use std::cell::Cell; +use std::hint::black_box; +use std::panic::{catch_unwind, AssertUnwindSafe}; +use std::sync::atomic::{AtomicBool, Ordering}; +use std::time::Instant; + +static STUBBED: AtomicBool = AtomicBool::new(false); + +fn quiet_stubs() { + std::panic::set_hook(Box::new(|_| STUBBED.store(true, Ordering::Relaxed))); +} + +fn stub_summary(what: &str) { + if STUBBED.load(Ordering::Relaxed) { + println!("\n[stub — implement {what} to unlock the lanes marked STUB]"); + } +} + +/// Best of three, in microseconds. +fn best3(mut f: impl FnMut() -> u64) -> (f64, u64) { + let mut best = f64::MAX; + let mut work = 0; + for _ in 0..3 { + let t = Instant::now(); + let w = f(); + let us = t.elapsed().as_secs_f64() * 1e6; + if us < best { + best = us; + } + work = w; + } + (best, work) +} + +fn main() { + quiet_stubs(); + println!("=== ematch_bench ===\n"); + lane1(); + lane2(); + lane3(); + stub_summary("src/semi_naive.rs and src/binary_join.rs"); +} + +fn header(q: &Query, db: &Database, name_of: &dyn Fn(u32) -> String) { + let order = plan(q, db); + let vars: Vec = order.iter().map(|&v| q.names[v].clone()).collect(); + println!(" {}", q.render(name_of)); + println!(" variable ordering: [{}]", vars.join(", ")); +} + +fn lane1() { + for (title, linear) in [ + ("f(a, g(a)) — one equality constraint, N matches", false), + ("f(a, g(b)) — linear pattern, N^2 matches", true), + ] { + println!("-- lane 1: {title} --"); + let probe = Fig2::new(4); + let (f, gs) = (probe.f, probe.gs); + let pat = if linear { + papp(f, vec![pvar("a"), papp(gs, vec![pvar("b")])]) + } else { + papp(f, vec![pvar("a"), papp(gs, vec![pvar("a")])]) + }; + let q = compile(&[pat.clone()]); + let names: Vec = [f, gs].iter().map(|&s| probe.g.sym_name(s).to_string()).collect(); + header(&q, &to_database(&probe.g), &|s| { + names[if s == f { 0 } else { 1 }].clone() + }); + println!( + "\n{:>7} {:>9} {:>11} {:>13} {:>12} {:>13} {:>10} {:>10} {:>9}", + "N", "e-nodes", "matches", "bt visits", "bt µs", "gj probes", "index µs", "gj µs", "speedup" + ); + + for n in [100usize, 200, 400, 800, 1600] { + let fig = Fig2::new(n); + let g = &fig.g; + let pv = number(&pat, &q); + let prog = backtrack::compile(&[pv], q.n_vars, &q.roots); + + let (bt_us, bt_visits) = best3(|| { + let visits = Cell::new(0); + let mut hits = 0u64; + backtrack::search(g, &prog, &visits, &mut |regs| { + black_box(regs); + hits += 1; + }); + black_box(hits); + visits.get() + }); + let mut bt_matches = 0u64; + { + let visits = Cell::new(0); + backtrack::search(g, &prog, &visits, &mut |_| bt_matches += 1); + } + + let db = to_database(g); + let order = plan(&q, &db); + let (idx_us, _) = best3(|| { + let idx = relational::index_query(&q, &db, &order); + black_box(idx.len() as u64) + }); + let idx = relational::index_query(&q, &db, &order); + let (gj_us, gj_probes) = best3(|| { + let probes = Cell::new(0); + let mut hits = 0u64; + relational::generic_join(&order, &idx, q.n_vars, &probes, &mut |s| { + black_box(s); + hits += 1; + }); + black_box(hits); + probes.get() + }); + let mut gj_matches = 0u64; + { + let probes = Cell::new(0); + relational::generic_join(&order, &idx, q.n_vars, &probes, &mut |_| { + gj_matches += 1 + }); + } + assert_eq!(bt_matches, gj_matches, "the two matchers disagree at N={n}"); + + println!( + "{:>7} {:>9} {:>11} {:>13} {:>12.1} {:>13} {:>10.1} {:>10.1} {:>9}", + n, + g.total_nodes(), + bt_matches, + bt_visits, + bt_us, + gj_probes, + idx_us, + gj_us, + format!("{:.2}x", bt_us / (gj_us + idx_us)) + ); + } + println!(); + } +} + +fn lane2() { + println!("-- lane 2: one more iteration of saturation — re-derive, or take the delta --"); + let n = 20_000; + let k = 8; + let mut fig = Fig2::new(n); + let before = to_database(&fig.g); + let (f, gs) = (fig.f, fig.gs); + fig.grow(k); + let after = to_database(&fig.g); + let delta = db_delta(&after, &before); + let q = compile(&[papp(f, vec![pvar("a"), papp(gs, vec![pvar("a")])])]); + println!( + " e-graph {} tuples + delta of {} tuples ({} new constants)", + db_tuples(&before), + db_tuples(&delta), + k + ); + println!( + "\n{:>14} {:>11} {:>13} {:>10}", + "evaluation", "matches", "probes", "µs" + ); + + let (full_us, full_probes) = best3(|| { + let p = Cell::new(0); + black_box(relational::matches(&q, &after, &p).len()); + p.get() + }); + let full_n = { + let p = Cell::new(0); + relational::matches(&q, &after, &p).len() + }; + println!("{:>14} {:>11} {:>13} {:>10.1}", "naive", full_n, full_probes, full_us); + + match catch_unwind(AssertUnwindSafe(|| { + let (us, probes) = best3(|| { + let p = Cell::new(0); + black_box(semi_naive::delta_matches(&q, &after, &delta, &p).len()); + p.get() + }); + let n = { + let p = Cell::new(0); + semi_naive::delta_matches(&q, &after, &delta, &p).len() + }; + (n, probes, us) + })) { + Ok((n, probes, us)) => println!( + "{:>14} {:>11} {:>13} {:>10.1}", + "semi-naive", n, probes, us + ), + Err(_) => println!( + "{:>14} {:>11} {:>13} {:>10}", + "semi-naive", "STUB", "-", "-" + ), + } + println!(); +} + +fn lane3() { + println!("-- lane 3: the triangle multi-pattern {{e(x,y), e(y,z), e(z,x)}} --"); + println!(" (no backtracking column: with three roots to scan it is O(M^3), minutes at M=4000)"); + println!( + "\n{:>7} {:>7} {:>11} {:>13} {:>10} {:>15} {:>13} {:>10}", + "V", "E", "matches", "gj probes", "gj µs", "bj intermediate", "bj probes", "bj µs" + ); + for (v, e) in [(200usize, 1000usize), (400, 2000), (800, 4000), (1600, 8000)] { + let (g, esym) = edge_graph(v, e, 20 + v as u64); + let db = to_database(&g); + let q = compile(&[ + papp(esym, vec![pvar("x"), pvar("y")]), + papp(esym, vec![pvar("y"), pvar("z")]), + papp(esym, vec![pvar("z"), pvar("x")]), + ]); + let order = plan(&q, &db); + let idx = relational::index_query(&q, &db, &order); + let (gj_us, gj_probes) = best3(|| { + let p = Cell::new(0); + let mut hits = 0u64; + relational::generic_join(&order, &idx, q.n_vars, &p, &mut |s| { + black_box(s); + hits += 1; + }); + black_box(hits); + p.get() + }); + let mut n_matches = 0u64; + { + let p = Cell::new(0); + relational::generic_join(&order, &idx, q.n_vars, &p, &mut |_| n_matches += 1); + } + match catch_unwind(AssertUnwindSafe(|| { + let p = Cell::new(0); + let t = Instant::now(); + let r = binary_join::binary_join(&q, &db, &p); + let us = t.elapsed().as_secs_f64() * 1e6; + (r.max_intermediate, r.matches.len(), p.get(), us) + })) { + Ok((inter, m, probes, us)) => { + assert_eq!(m as u64, n_matches, "binary join disagrees with generic join"); + println!( + "{:>7} {:>7} {:>11} {:>13} {:>10.1} {:>15} {:>13} {:>10.1}", + v, e, n_matches, gj_probes, gj_us, inter, probes, us + ); + } + Err(_) => println!( + "{:>7} {:>7} {:>11} {:>13} {:>10.1} {:>15} {:>13} {:>10}", + v, e, n_matches, gj_probes, gj_us, "STUB", "-", "-" + ), + } + } +} diff --git a/topics/44-egraphs-egglog/experiments/src/binary_join.rs b/topics/44-egraphs-egglog/experiments/src/binary_join.rs new file mode 100644 index 0000000..658e5ce --- /dev/null +++ b/topics/44-egraphs-egglog/experiments/src/binary_join.rs @@ -0,0 +1,89 @@ +//! LANE 3 (exercise) — the binary-join baseline, on a cyclic pattern. +//! +//! Generic join is only interesting if the plan it replaces is worse. The +//! multi-pattern `{ e(x,y), e(y,z), e(z,x) }` compiles to the triangle query +//! +//! Q(x, y, z) <- R_e(r1, x, y), R_e(r2, y, z), R_e(r3, z, x) +//! +//! which is *cyclic*: no join tree covers it (POPL'22 §2.3). Any binary plan +//! must pick two atoms to join first, and that intermediate is the whole +//! problem — for M edges it is O(M^2) in the worst case even when the answer is +//! only O(M^1.5), the AGM bound of the triangle. +//! +//! Implement [`binary_join`] as a left-deep hash-join plan: +//! +//! 1. order the atoms (any order; a fixed one is fine, but say which); +//! 2. join atom 1 with atom 2 on their shared variables by building a hash +//! table on the smaller side and probing with the larger — the textbook +//! build/probe of topic 11; +//! 3. materialise the intermediate, then join it with atom 3, and so on; +//! 4. count every hash-table insert and every probe into `probes`, and record +//! the largest intermediate you materialised. +//! +//! The numbers to compare in `ematch_bench` lane 3 are `max_intermediate` +//! against the generic-join column's `probes`, as M grows. If the binary plan's +//! intermediate grows quadratically while the output grows as M^1.5, you have +//! reproduced the reason worst-case optimal joins exist — the same reason +//! topic 13's two-hop query is a join-order problem. + +use crate::egraph::Id; +use crate::pattern::Query; +use crate::relational::Database; +use std::cell::Cell; + +#[derive(Debug, Default)] +pub struct BinaryJoinReport { + pub matches: Vec>, + /// Tuples in the largest intermediate relation the plan materialised. + pub max_intermediate: usize, +} + +pub fn binary_join(q: &Query, db: &Database, probes: &Cell) -> BinaryJoinReport { + let _ = (q, db, probes); + todo!("left-deep hash-join plan (see module docs)") +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::gen::edge_graph; + use crate::pattern::{compile, papp, pvar}; + use crate::relational::{matches, to_database}; + use std::collections::HashSet; + + fn triangle_query(e: crate::egraph::Sym) -> Query { + compile(&[ + papp(e, vec![pvar("x"), pvar("y")]), + papp(e, vec![pvar("y"), pvar("z")]), + papp(e, vec![pvar("z"), pvar("x")]), + ]) + } + + #[test] + fn binary_join_agrees_with_generic_join() { + let (g, e) = edge_graph(120, 900, 7); + let db = to_database(&g); + let q = triangle_query(e); + let p = Cell::new(0); + let want: HashSet> = matches(&q, &db, &p).into_iter().collect(); + assert!(!want.is_empty(), "the generator should produce triangles"); + let got: HashSet> = binary_join(&q, &db, &p).matches.into_iter().collect(); + assert_eq!(got, want); + } + + #[test] + fn the_intermediate_is_the_problem() { + let (g, e) = edge_graph(400, 4000, 11); + let db = to_database(&g); + let q = triangle_query(e); + let p = Cell::new(0); + let r = binary_join(&q, &db, &p); + assert!( + r.max_intermediate > 4 * r.matches.len(), + "intermediate {} vs output {} — a binary plan on a cyclic query is \ + supposed to materialise far more than it returns", + r.max_intermediate, + r.matches.len() + ); + } +} diff --git a/topics/44-egraphs-egglog/experiments/src/egraph.rs b/topics/44-egraphs-egglog/experiments/src/egraph.rs new file mode 100644 index 0000000..9c9d0f4 --- /dev/null +++ b/topics/44-egraphs-egglog/experiments/src/egraph.rs @@ -0,0 +1,214 @@ +//! A minimal e-graph — union-find, hashcons, e-class map, deferred rebuild. +//! +//! Small on purpose: topic 21 reads egg's real one (`~/repos/egg/src/egraph.rs`) +//! and this crate is not trying to replace it. What we need here is an e-graph +//! whose *internal representation is visible*, so the same structure can be +//! walked as a graph (`backtrack.rs`) and read as a set of tables +//! (`relational.rs`) with nothing hidden between the two. +//! +//! egg anchors for the same three pieces, at the pinned commit: +//! unionfind.rs:30 UnionFind::find — no path compression on the & path +//! egraph.rs:970 EGraph::add — hashcons lookup-or-insert +//! egraph.rs:1147 EGraph::union — merge now, repair later +//! egraph.rs:1416 EGraph::rebuild — the deferred congruence repair + +use std::collections::HashMap; + +/// An e-class id. Not necessarily canonical — call [`EGraph::find`]. +pub type Id = u32; +/// An interned function symbol. +pub type Sym = u32; + +/// `(f, [child ids])`. In the relational view this is one tuple of `R_f`, with +/// the containing e-class id prepended. +#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)] +pub struct ENode { + pub op: Sym, + pub children: Vec, +} + +#[derive(Default)] +pub struct EGraph { + parents: Vec, + classes: HashMap>, + memo: HashMap, + names: Vec, + syms: HashMap, +} + +impl EGraph { + pub fn new() -> Self { + Self::default() + } + + /// Intern a function symbol. `sym("f") == sym("f")`, always. + pub fn sym(&mut self, name: &str) -> Sym { + if let Some(&s) = self.syms.get(name) { + return s; + } + let s = self.names.len() as Sym; + self.names.push(name.to_string()); + self.syms.insert(name.to_string(), s); + s + } + + pub fn sym_name(&self, s: Sym) -> &str { + &self.names[s as usize] + } + + pub fn lookup_sym(&self, name: &str) -> Option { + self.syms.get(name).copied() + } + + /// Canonical id. Like egg's `find(&self)`, this walks without compressing. + pub fn find(&self, mut id: Id) -> Id { + while self.parents[id as usize] != id { + id = self.parents[id as usize]; + } + id + } + + fn canon(&self, n: &ENode) -> ENode { + ENode { + op: n.op, + children: n.children.iter().map(|&c| self.find(c)).collect(), + } + } + + /// Hashcons: an e-node with the same symbol and canonical children is the + /// same e-node, and lands in the same e-class. + pub fn add(&mut self, op: Sym, children: &[Id]) -> Id { + let node = self.canon(&ENode { + op, + children: children.to_vec(), + }); + if let Some(&id) = self.memo.get(&node) { + return self.find(id); + } + let id = self.parents.len() as Id; + self.parents.push(id); + self.classes.insert(id, vec![node.clone()]); + self.memo.insert(node, id); + id + } + + /// Merge two e-classes. Congruence is left broken until [`Self::rebuild`]. + pub fn union(&mut self, a: Id, b: Id) -> bool { + let (a, b) = (self.find(a), self.find(b)); + if a == b { + return false; + } + self.parents[b as usize] = a; + if let Some(nodes) = self.classes.remove(&b) { + self.classes.entry(a).or_default().extend(nodes); + } + true + } + + /// Restore both invariants: every e-node's children are canonical ids, and + /// no two e-classes contain the same e-node (congruence). Runs to fixpoint, + /// because merging two classes can make two more e-nodes congruent. + pub fn rebuild(&mut self) { + loop { + let old: Vec<(Id, Vec)> = self.classes.drain().collect(); + let mut fresh: HashMap> = HashMap::new(); + for (id, nodes) in old { + let c = self.find(id); + let slot = fresh.entry(c).or_default(); + for n in nodes { + slot.push(self.canon(&n)); + } + } + for v in fresh.values_mut() { + v.sort(); + v.dedup(); + } + self.classes = fresh; + + let mut memo: HashMap = HashMap::new(); + let mut merges: Vec<(Id, Id)> = Vec::new(); + for (&c, nodes) in &self.classes { + for n in nodes { + match memo.get(n) { + Some(&prev) if prev != c => merges.push((prev, c)), + Some(_) => {} + None => { + memo.insert(n.clone(), c); + } + } + } + } + if merges.is_empty() { + self.memo = memo; + return; + } + for (a, b) in merges { + self.union(a, b); + } + } + } + + pub fn class_ids(&self) -> impl Iterator + '_ { + self.classes.keys().copied() + } + + pub fn nodes(&self, class: Id) -> &[ENode] { + static EMPTY: &[ENode] = &[]; + self.classes.get(&self.find(class)).map_or(EMPTY, |v| v) + } + + pub fn total_nodes(&self) -> usize { + self.classes.values().map(|v| v.len()).sum() + } + + pub fn n_classes(&self) -> usize { + self.classes.len() + } + + /// Every e-class holding at least one `op` e-node — egg's `classes_by_op` + /// index (`egraph.rs:81`), which keeps a pattern's root from scanning the + /// whole e-graph. Both matchers get it, so the comparison is about the + /// inner loop rather than about the root scan. + pub fn classes_with_op(&self, op: Sym) -> Vec { + let mut v: Vec = self + .classes + .iter() + .filter(|(_, ns)| ns.iter().any(|n| n.op == op)) + .map(|(&c, _)| c) + .collect(); + v.sort(); + v + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn hashcons_returns_the_same_class() { + let mut g = EGraph::new(); + let f = g.sym("f"); + let a = g.sym("a"); + let x = g.add(a, &[]); + let n1 = g.add(f, &[x]); + let n2 = g.add(f, &[x]); + assert_eq!(n1, n2); + assert_eq!(g.total_nodes(), 2); + } + + #[test] + fn rebuild_closes_congruence() { + // f(a) and f(b) are distinct until a and b are merged; then congruence + // says they are the same e-node, so their classes must merge too. + let mut g = EGraph::new(); + let (f, a, b) = (g.sym("f"), g.sym("a"), g.sym("b")); + let (ia, ib) = (g.add(a, &[]), g.add(b, &[])); + let (fa, fb) = (g.add(f, &[ia]), g.add(f, &[ib])); + assert_ne!(g.find(fa), g.find(fb)); + g.union(ia, ib); + g.rebuild(); + assert_eq!(g.find(fa), g.find(fb), "congruence not restored"); + assert_eq!(g.nodes(fa).len(), 1, "duplicate e-node survived rebuild"); + } +} diff --git a/topics/44-egraphs-egglog/experiments/src/gen.rs b/topics/44-egraphs-egglog/experiments/src/gen.rs new file mode 100644 index 0000000..177bda4 --- /dev/null +++ b/topics/44-egraphs-egglog/experiments/src/gen.rs @@ -0,0 +1,133 @@ +//! Seeded e-graph generators. Every figure in this topic reproduces exactly. + +use crate::egraph::{EGraph, Id, Sym}; +use crate::relational::{Database, Relation}; +use rand::{Rng, SeedableRng}; +use rand_chacha::ChaCha8Rng; +use std::collections::HashSet; + +/// The e-graph of POPL'22 Figure 2: N constants, one e-class holding +/// `g(1)..g(N)`, one e-class holding `f(1, i_g)..f(N, i_g)`. +/// +/// 3N e-nodes, N+2 e-classes — and it represents N + N + N^2 terms, which is +/// the whole point: the e-graph is polynomial and the term set it stands for is +/// quadratic, so an algorithm that enumerates terms has already lost. +pub struct Fig2 { + pub g: EGraph, + pub f: Sym, + pub gs: Sym, + pub ig: Id, + pub iff: Id, + pub n: usize, +} + +impl Fig2 { + pub fn new(n: usize) -> Self { + let mut g = EGraph::new(); + let f = g.sym("f"); + let gs = g.sym("g"); + let mut me = Fig2 { + g, + f, + gs, + ig: 0, + iff: 0, + n: 0, + }; + me.extend(n, true); + me + } + + /// Add `k` more constants, with their `g` and `f` e-nodes, into the same + /// two e-classes. Used by the semi-naive lane: the e-graph after the delta + /// keeps every id it had before it. + pub fn grow(&mut self, k: usize) { + self.extend(k, false); + } + + fn extend(&mut self, k: usize, first: bool) { + let (f, gs) = (self.f, self.gs); + let base = self.n; + let leaves: Vec = (base..base + k) + .map(|i| { + let s = self.g.sym(&format!("c{i}")); + self.g.add(s, &[]) + }) + .collect(); + + for (j, &l) in leaves.iter().enumerate() { + let x = self.g.add(gs, &[l]); + if first && j == 0 { + self.ig = x; + } else { + self.g.union(self.ig, x); + } + } + self.g.rebuild(); + self.ig = self.g.find(self.ig); + + for (j, &l) in leaves.iter().enumerate() { + let x = self.g.add(f, &[l, self.ig]); + if first && j == 0 { + self.iff = x; + } else { + self.g.union(self.iff, x); + } + } + self.g.rebuild(); + self.iff = self.g.find(self.iff); + self.n += k; + } +} + +/// A seeded directed graph as an e-graph: one nullary e-node per vertex, one +/// binary `e(x, y)` e-node per edge, no unions. `R_e` is then an edge list, and +/// the triangle multi-pattern is the database triangle query on the nose. +pub fn edge_graph(vertices: usize, edges: usize, seed: u64) -> (EGraph, Sym) { + let mut g = EGraph::new(); + let e = g.sym("e"); + let vs: Vec = (0..vertices) + .map(|i| { + let s = g.sym(&format!("v{i}")); + g.add(s, &[]) + }) + .collect(); + let mut rng = ChaCha8Rng::seed_from_u64(seed); + let mut seen = HashSet::new(); + let mut made = 0; + while made < edges { + let (a, b) = (rng.gen_range(0..vertices), rng.gen_range(0..vertices)); + if a == b || !seen.insert((a, b)) { + continue; + } + g.add(e, &[vs[a], vs[b]]); + made += 1; + } + g.rebuild(); + (g, e) +} + +/// Tuples present in `new` and not in `old` — the delta database a semi-naive +/// iteration is allowed to look at. +pub fn db_delta(new: &Database, old: &Database) -> Database { + let mut d: Database = Database::new(); + for (&rel, r) in new { + let before: HashSet<&Vec> = old.get(&rel).map(|o| o.tuples.iter().collect()).unwrap_or_default(); + let tuples: Vec> = r + .tuples + .iter() + .filter(|t| !before.contains(*t)) + .cloned() + .collect(); + if !tuples.is_empty() { + d.insert( + rel, + Relation { + arity: r.arity, + tuples, + }, + ); + } + } + d +} diff --git a/topics/44-egraphs-egglog/experiments/src/lib.rs b/topics/44-egraphs-egglog/experiments/src/lib.rs new file mode 100644 index 0000000..fb95d83 --- /dev/null +++ b/topics/44-egraphs-egglog/experiments/src/lib.rs @@ -0,0 +1,17 @@ +//! Topic 44 — the e-graph as a relational database. +//! +//! Lane 1 (provided): the same pattern matched two ways — the backtracking +//! search every e-matcher shipped before 2022, and the relational one that +//! compiles the pattern to a conjunctive query and runs generic join over the +//! e-graph's tables. +//! +//! Lanes 2 and 3 are the exercises: semi-naive evaluation (`semi_naive`) and a +//! binary-join baseline for the cyclic multi-pattern (`binary_join`). + +pub mod backtrack; +pub mod binary_join; +pub mod egraph; +pub mod gen; +pub mod pattern; +pub mod relational; +pub mod semi_naive; diff --git a/topics/44-egraphs-egglog/experiments/src/pattern.rs b/topics/44-egraphs-egglog/experiments/src/pattern.rs new file mode 100644 index 0000000..0353e25 --- /dev/null +++ b/topics/44-egraphs-egglog/experiments/src/pattern.rs @@ -0,0 +1,178 @@ +//! Patterns, and the compilation of a pattern into a conjunctive query. +//! +//! This is Figure 8 of "Relational E-matching" (POPL'22), which unnests a +//! pattern by giving every non-variable subpattern a fresh auxiliary variable: +//! +//! Aux(f(p1..pk)) = v ~ R_f(v, v1..vk), A1..Ak where Aux(pi) = vi ~ Ai +//! Aux(x) = x ~ [] +//! +//! So `f(a, g(a))` becomes `Q(root, a) <- R_f(root, a, x), R_g(x, a)`, and the +//! repeated `a` — the *equality constraint* backtracking checks last — is now +//! just a join variable, indistinguishable from the structural one (`x`). + +use crate::egraph::Sym; +use std::collections::HashMap; + +pub type VarId = usize; + +#[derive(Clone, Debug)] +pub enum Pat { + Var(String), + App(Sym, Vec), +} + +pub fn pvar(name: &str) -> Pat { + Pat::Var(name.to_string()) +} + +pub fn papp(op: Sym, args: Vec) -> Pat { + Pat::App(op, args) +} + +/// `R_rel(vars[0], vars[1..])` — `vars[0]` is always the e-class id column. +#[derive(Clone, Debug)] +pub struct Atom { + pub rel: Sym, + pub vars: Vec, +} + +#[derive(Clone, Debug)] +pub struct Query { + pub atoms: Vec, + pub n_vars: usize, + /// Display name per variable; auxiliaries are named `?0`, `?1`, … + pub names: Vec, + /// The variables the caller wants back: the roots, then the pattern vars. + pub head: Vec, + /// One root per input pattern, in order. + pub roots: Vec, +} + +struct Builder { + atoms: Vec, + names: Vec, + by_name: HashMap, + aux: usize, +} + +impl Builder { + fn named(&mut self, name: &str) -> VarId { + if let Some(&v) = self.by_name.get(name) { + return v; + } + let v = self.names.len(); + self.names.push(name.to_string()); + self.by_name.insert(name.to_string(), v); + v + } + + fn fresh(&mut self) -> VarId { + let v = self.names.len(); + self.names.push(format!("?{}", self.aux)); + self.aux += 1; + v + } + + /// Aux from Figure 8: returns the variable standing for this subpattern. + fn aux_of(&mut self, p: &Pat) -> VarId { + match p { + Pat::Var(name) => self.named(name), + Pat::App(op, args) => { + let v = self.fresh(); + // Reserve this atom's slot before recursing, so the body reads + // outside-in the way the paper writes it. + let slot = self.atoms.len(); + self.atoms.push(Atom { rel: *op, vars: vec![v] }); + let child_vars: Vec = args.iter().map(|a| self.aux_of(a)).collect(); + self.atoms[slot].vars.extend(child_vars); + v + } + } + } +} + +/// Compile one or more patterns into a single conjunctive query. Several +/// patterns sharing variables is a *multi-pattern*; the relational view gets it +/// for free, since it is just more atoms in the same query body (POPL'22 §1). +pub fn compile(pats: &[Pat]) -> Query { + let mut b = Builder { + atoms: vec![], + names: vec![], + by_name: HashMap::new(), + aux: 0, + }; + let roots: Vec = pats.iter().map(|p| b.aux_of(p)).collect(); + let mut head = roots.clone(); + // The pattern's own variables, in first-appearance order. + let mut named: Vec = b.by_name.values().copied().collect(); + named.sort(); + head.extend(named); + Query { + n_vars: b.names.len(), + atoms: b.atoms, + names: b.names, + head, + roots, + } +} + +impl Query { + /// Human-readable, in the paper's notation. + pub fn render(&self, name_of: &dyn Fn(Sym) -> String) -> String { + let head: Vec = self.head.iter().map(|&v| self.names[v].clone()).collect(); + let body: Vec = self + .atoms + .iter() + .map(|a| { + let vs: Vec = a.vars.iter().map(|&v| self.names[v].clone()).collect(); + format!("R_{}({})", name_of(a.rel), vs.join(", ")) + }) + .collect(); + format!("Q({}) <- {}", head.join(", "), body.join(", ")) + } + + pub fn atoms_with(&self, v: VarId) -> Vec { + (0..self.atoms.len()) + .filter(|&i| self.atoms[i].vars.contains(&v)) + .collect() + } +} + +/// A pattern whose variables have been numbered against a [`Query`], so both +/// matchers report substitutions in the same variable space. +#[derive(Clone, Debug)] +pub enum PatV { + Var(VarId), + App(Sym, Vec), +} + +pub fn number(p: &Pat, q: &Query) -> PatV { + match p { + Pat::Var(name) => PatV::Var( + q.names + .iter() + .position(|n| n == name) + .expect("pattern variable not in the compiled query"), + ), + Pat::App(op, args) => PatV::App(*op, args.iter().map(|a| number(a, q)).collect()), + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::egraph::EGraph; + + #[test] + fn unnesting_matches_figure_8() { + let mut g = EGraph::new(); + let (f, gg) = (g.sym("f"), g.sym("g")); + // f(a, g(a)) + let q = compile(&[papp(f, vec![pvar("a"), papp(gg, vec![pvar("a")])])]); + assert_eq!(q.atoms.len(), 2, "one atom per non-variable subpattern"); + let rendered = q.render(&|s| g.sym_name(s).to_string()); + assert_eq!(rendered, "Q(?0, a) <- R_f(?0, a, ?1), R_g(?1, a)"); + // `a` occurs in both atoms: the equality constraint became a join. + assert_eq!(q.atoms_with(q.head[1]).len(), 2); + } +} diff --git a/topics/44-egraphs-egglog/experiments/src/relational.rs b/topics/44-egraphs-egglog/experiments/src/relational.rs new file mode 100644 index 0000000..c251649 --- /dev/null +++ b/topics/44-egraphs-egglog/experiments/src/relational.rs @@ -0,0 +1,319 @@ +//! The e-graph read as a relational database, and generic join over it. +//! +//! POPL'22 §3.1: every e-node with symbol `f` and arity k is one tuple of a +//! relation `R_f` of arity k+1 — the containing e-class id, then the children, +//! all canonical. Nothing is copied out of the e-graph that was not already in +//! it; this is a *view*, and egglog's answer (topic 44's second half) is to +//! stop maintaining the other view at all. +//! +//! Generic join (POPL'22 Algorithm 1, from Ngo et al.) is variable-at-a-time +//! rather than relation-at-a-time: pick a variable, intersect the sets of +//! values every atom allows for it, recurse on each survivor. Its cost is +//! bounded by the AGM bound of the query, which is why it cannot blow up on a +//! cyclic query the way a binary-join plan can. + +use crate::egraph::{EGraph, Id, Sym}; +use crate::pattern::{Atom, Query, VarId}; +use std::cell::Cell; +use std::collections::HashMap; + +#[derive(Default, Clone, Debug)] +pub struct Relation { + pub arity: usize, + pub tuples: Vec>, +} + +pub type Database = HashMap; + +/// One pass over the e-graph, one tuple per e-node. +pub fn to_database(g: &EGraph) -> Database { + let mut db: Database = HashMap::new(); + for c in g.class_ids() { + for n in g.nodes(c) { + let r = db.entry(n.op).or_insert_with(|| Relation { + arity: n.children.len() + 1, + tuples: vec![], + }); + let mut t = Vec::with_capacity(n.children.len() + 1); + t.push(c); + t.extend(n.children.iter().map(|&x| g.find(x))); + r.tuples.push(t); + } + } + db +} + +pub fn db_tuples(db: &Database) -> usize { + db.values().map(|r| r.tuples.len()).sum() +} + +/// A trie is a tree of maps; a path from the root spells one tuple, with the +/// columns ordered to agree with the query's variable ordering (POPL'22 Fig 5). +/// This is what makes "the residual relation R(v, y)" a pointer chase rather +/// than a filter. +#[derive(Default, Debug)] +pub struct Trie { + pub kids: HashMap, +} + +impl Trie { + fn insert(&mut self, path: &[Id]) { + let Some((h, rest)) = path.split_first() else { + return; + }; + self.kids.entry(*h).or_default().insert(rest); + } +} + +/// An atom indexed for one variable ordering. +pub struct AtomIndex { + /// The atom's distinct variables, in the global ordering. + pub vars: Vec, + pub trie: Trie, + pub tuples_indexed: usize, +} + +/// Build the trie for one atom. A variable occurring twice in the same atom +/// (`f(x, x)`) indexes on its first column and filters on the rest. +pub fn index_atom(rel: &Relation, atom: &Atom, order: &[VarId]) -> AtomIndex { + let pos = |v: VarId| order.iter().position(|&o| o == v).expect("var not in ordering"); + let mut first: Vec<(VarId, usize)> = vec![]; + let mut filters: Vec<(usize, usize)> = vec![]; + for (col, &v) in atom.vars.iter().enumerate() { + match first.iter().find(|(fv, _)| *fv == v) { + Some(&(_, c0)) => filters.push((c0, col)), + None => first.push((v, col)), + } + } + first.sort_by_key(|&(v, _)| pos(v)); + let cols: Vec = first.iter().map(|&(_, c)| c).collect(); + let vars: Vec = first.iter().map(|&(v, _)| v).collect(); + + let mut trie = Trie::default(); + let mut indexed = 0; + let mut path = vec![0 as Id; cols.len()]; + for t in &rel.tuples { + if filters.iter().any(|&(a, b)| t[a] != t[b]) { + continue; + } + for (i, &c) in cols.iter().enumerate() { + path[i] = t[c]; + } + trie.insert(&path); + indexed += 1; + } + AtomIndex { + vars, + trie, + tuples_indexed: indexed, + } +} + +/// Variable ordering: most-constrained-first — the variable in the most atoms, +/// breaking ties toward the one whose smallest relation is smallest. Any order +/// is worst-case optimal; the order is what decides the constant (POPL'22 §2.3, +/// "different orderings can lead to dramatically different run time"). +pub fn plan(q: &Query, db: &Database) -> Vec { + let mut vars: Vec = (0..q.n_vars).collect(); + let key = |v: &VarId| { + let atoms = q.atoms_with(*v); + let smallest = atoms + .iter() + .map(|&i| db.get(&q.atoms[i].rel).map_or(usize::MAX, |r| r.tuples.len())) + .min() + .unwrap_or(usize::MAX); + (usize::MAX - atoms.len(), smallest, *v) + }; + vars.sort_by_key(key); + vars +} + +pub fn index_query(q: &Query, db: &Database, order: &[VarId]) -> Vec { + static EMPTY: &[Vec] = &[]; + q.atoms + .iter() + .map(|a| match db.get(&a.rel) { + Some(r) => index_atom(r, a, order), + None => index_atom( + &Relation { + arity: a.vars.len(), + tuples: EMPTY.to_vec(), + }, + a, + order, + ), + }) + .collect() +} + +/// Generic join. `probes` counts the same unit backtracking counts: one per +/// key looked at during an intersection. +pub fn generic_join( + order: &[VarId], + idx: &[AtomIndex], + n_vars: usize, + probes: &Cell, + out: &mut dyn FnMut(&[Id]), +) { + let mut cur: Vec<&Trie> = idx.iter().map(|a| &a.trie).collect(); + let mut depth_of: Vec = vec![0; idx.len()]; + let mut subst = vec![0 as Id; n_vars]; + gj(0, order, idx, &mut cur, &mut depth_of, &mut subst, probes, out); +} + +/// Atoms participating in one intersection. Patterns in this topic have at +/// most three atoms; the fixed array keeps the inner loop allocation-free, so +/// the numbers compare algorithms rather than allocators. +const MAX_ATOMS: usize = 8; + +#[allow(clippy::too_many_arguments)] +fn gj<'a>( + depth: usize, + order: &[VarId], + idx: &'a [AtomIndex], + cur: &mut [&'a Trie], + at: &mut [usize], + subst: &mut [Id], + probes: &Cell, + out: &mut dyn FnMut(&[Id]), +) { + if depth == order.len() { + out(subst); + return; + } + let x = order[depth]; + let mut part = [0usize; MAX_ATOMS]; + let mut n_part = 0; + for i in 0..idx.len() { + if idx[i].vars.get(at[i]) == Some(&x) { + assert!(n_part < MAX_ATOMS, "raise MAX_ATOMS for this query"); + part[n_part] = i; + n_part += 1; + } + } + if n_part == 0 { + // A variable no atom constrains: nothing to intersect, nothing to bind. + gj(depth + 1, order, idx, cur, at, subst, probes, out); + return; + } + // Intersect smallest-first, which is what buys the O(min |R_j.x|) bound. + let lead = *part[..n_part] + .iter() + .min_by_key(|&&i| cur[i].kids.len()) + .expect("non-empty"); + let lead_trie: &'a Trie = cur[lead]; + let mut others = [(0usize, lead_trie); MAX_ATOMS]; + let mut n_others = 0; + for &i in &part[..n_part] { + if i != lead { + others[n_others] = (i, cur[i]); + n_others += 1; + } + } + let mut next = [(0usize, lead_trie); MAX_ATOMS]; + + for (&v, sub) in &lead_trie.kids { + probes.set(probes.get() + 1); + let mut ok = true; + for k in 0..n_others { + probes.set(probes.get() + 1); + match others[k].1.kids.get(&v) { + Some(child) => next[k] = (others[k].0, child), + None => { + ok = false; + break; + } + } + } + if !ok { + continue; + } + cur[lead] = sub; + at[lead] += 1; + for &(i, t) in &next[..n_others] { + cur[i] = t; + at[i] += 1; + } + subst[x] = v; + gj(depth + 1, order, idx, cur, at, subst, probes, out); + cur[lead] = lead_trie; + at[lead] -= 1; + for &(i, t) in &others[..n_others] { + cur[i] = t; + at[i] -= 1; + } + } +} + +/// Substitutions for the head variables, in head order. +pub fn matches(q: &Query, db: &Database, probes: &Cell) -> Vec> { + let order = plan(q, db); + let idx = index_query(q, db, &order); + let mut found = vec![]; + generic_join(&order, &idx, q.n_vars, probes, &mut |s| { + found.push(q.head.iter().map(|&v| s[v]).collect()); + }); + found +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::backtrack; + use crate::gen::{edge_graph, Fig2}; + use crate::pattern::{compile, number, papp, pvar, Pat}; + use std::collections::HashSet; + + /// The load-bearing test for lane 1: a graph walk and a join must return + /// the same set of substitutions, or the timing table compares nothing. + fn agree(g: &EGraph, pats: &[Pat], expect: usize) { + let q = compile(pats); + let pv: Vec<_> = pats.iter().map(|p| number(p, &q)).collect(); + let prog = backtrack::compile(&pv, q.n_vars, &q.roots); + let bt = Cell::new(0); + let walked: HashSet> = backtrack::matches(g, &prog, &q.head, &bt) + .into_iter() + .collect(); + let gj = Cell::new(0); + let joined: HashSet> = matches(&q, &to_database(g), &gj).into_iter().collect(); + assert_eq!(walked.len(), expect, "unexpected match count"); + assert_eq!(walked, joined, "the two matchers disagree"); + } + + #[test] + fn nonlinear_pattern_agrees() { + let fig = Fig2::new(60); + // f(a, g(a)) — N matches out of N^2 candidate terms. + agree( + &fig.g, + &[papp(fig.f, vec![pvar("a"), papp(fig.gs, vec![pvar("a")])])], + 60, + ); + } + + #[test] + fn linear_pattern_agrees() { + let fig = Fig2::new(40); + // f(a, g(b)) — every candidate is a match: N^2 of them. + agree( + &fig.g, + &[papp(fig.f, vec![pvar("a"), papp(fig.gs, vec![pvar("b")])])], + 1600, + ); + } + + #[test] + fn triangle_multipattern_agrees() { + let (g, e) = edge_graph(60, 300, 3); + let pats = vec![ + papp(e, vec![pvar("x"), pvar("y")]), + papp(e, vec![pvar("y"), pvar("z")]), + papp(e, vec![pvar("z"), pvar("x")]), + ]; + let q = compile(&pats); + let gj = Cell::new(0); + let n = matches(&q, &to_database(&g), &gj).len(); + assert!(n > 0, "generator produced no triangles"); + agree(&g, &pats, n); + } +} diff --git a/topics/44-egraphs-egglog/experiments/src/semi_naive.rs b/topics/44-egraphs-egglog/experiments/src/semi_naive.rs new file mode 100644 index 0000000..e04c09b --- /dev/null +++ b/topics/44-egraphs-egglog/experiments/src/semi_naive.rs @@ -0,0 +1,101 @@ +//! LANE 2 (exercise) — semi-naive evaluation. +//! +//! An equality-saturation loop runs the same queries against an e-graph that +//! only ever grows. Naive evaluation re-derives, on iteration i+1, every match +//! it already derived on iteration i. Semi-naive evaluation derives only the +//! matches that *use at least one new tuple*, which is the difference between +//! egglog and egglogNI in the PLDI'23 paper — the two curves of Figure 7, and +//! the 9.27x vs 3.34x speedups in §5.3. +//! +//! The rule (PLDI'23 §4.3): a rule with m body atoms +//! +//! A :- A_1, ..., A_m +//! +//! expands into m *delta rules*, the j-th of which ranges atom j over the new +//! tuples only and every other atom over the whole database: +//! +//! A :- A_1, ..., A_{j-1}, dA_j, A_{j+1}, ..., A_m +//! +//! Their union is exactly the set of derivations that touch something new. +//! Note the word union: a substitution using two new tuples is produced twice, +//! by two different delta rules, so the results must be deduplicated. That +//! duplication is the price of the incrementalisation and it is worth +//! measuring, not just avoiding. +//! +//! Implement [`delta_matches`]: +//! +//! 1. for each atom index j, build a database that is `db` everywhere except +//! relation `q.atoms[j].rel`, which is `delta`'s tuples for that relation +//! (careful: two atoms may name the same relation, as the triangle query +//! does — the substitution must be for atom j, not for every atom over +//! that relation); +//! 2. run [`crate::relational::matches`] on each, sharing `probes`; +//! 3. concatenate, then dedup. +//! +//! The test below is the specification: the result must equal +//! `matches(after) - matches(before)`, as sets. + +use crate::egraph::Id; +use crate::pattern::Query; +use crate::relational::Database; +use std::cell::Cell; + +pub fn delta_matches( + q: &Query, + db: &Database, + delta: &Database, + probes: &Cell, +) -> Vec> { + let _ = (q, db, delta, probes); + todo!("semi-naive evaluation (see module docs)") +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::gen::{db_delta, Fig2}; + use crate::pattern::{compile, papp, pvar}; + use crate::relational::{matches, to_database}; + use std::collections::HashSet; + + fn setup(n: usize, k: usize) -> (Query, Database, Database, Database) { + let mut fig = Fig2::new(n); + let before = to_database(&fig.g); + let (f, gs) = (fig.f, fig.gs); + fig.grow(k); + let after = to_database(&fig.g); + let delta = db_delta(&after, &before); + let q = compile(&[papp(f, vec![pvar("a"), papp(gs, vec![pvar("a")])])]); + (q, before, after, delta) + } + + #[test] + fn semi_naive_derives_exactly_the_new_matches() { + let (q, before, after, delta) = setup(200, 8); + let p = Cell::new(0); + let old: HashSet> = matches(&q, &before, &p).into_iter().collect(); + let new: HashSet> = matches(&q, &after, &p).into_iter().collect(); + let expected: HashSet> = new.difference(&old).cloned().collect(); + assert_eq!(expected.len(), 8, "the delta should be exactly the 8 new f-terms"); + + let got: HashSet> = delta_matches(&q, &after, &delta, &p).into_iter().collect(); + assert_eq!(got, expected); + } + + #[test] + fn semi_naive_is_cheaper_than_re_deriving_everything() { + let (q, _before, after, delta) = setup(2000, 8); + let full = Cell::new(0); + let n_full = matches(&q, &after, &full).len(); + let inc = Cell::new(0); + let n_inc = delta_matches(&q, &after, &delta, &inc).len(); + assert_eq!(n_full, 2008); + assert_eq!(n_inc, 8); + assert!( + inc.get() * 10 < full.get(), + "semi-naive did {} probes against naive's {} — that is not incremental", + inc.get(), + full.get() + ); + } +} diff --git a/topics/44-egraphs-egglog/notes.md b/topics/44-egraphs-egglog/notes.md new file mode 100644 index 0000000..e0848be --- /dev/null +++ b/topics/44-egraphs-egglog/notes.md @@ -0,0 +1,161 @@ +# Topic 44 notes — e-graphs as a database + +## Baseline (provided lane, Apple M3 Pro, measured 2026-08-26) + +`cargo run --release --bin ematch_bench`. Counters (`bt visits`, +`gj probes`) are exact and reproduce on any machine; µs columns are +best-of-three on this one. + +### Lane 1a — `f(a, g(a))`, the non-linear pattern + +| N | e-nodes | matches | bt visits | bt µs | gj probes | index µs | gj µs | speedup | +|---|---|---|---|---|---|---|---|---| +| 100 | 300 | 100 | 10,101 | 137.9 | 500 | 71.7 | 24.8 | 1.43x | +| 200 | 600 | 200 | 40,201 | 398.9 | 1,000 | 101.8 | 39.0 | 2.83x | +| 400 | 1200 | 400 | 160,401 | 1119.8 | 2,000 | 92.4 | 37.2 | 8.64x | +| 800 | 2400 | 800 | 640,801 | 2586.1 | 4,000 | 180.4 | 85.0 | 9.75x | +| 1600 | 4800 | 1600 | 2,561,601 | 10152.5 | 8,000 | 322.4 | 145.0 | 21.72x | + +Both counters are closed forms, and checking them is how you know the +harness is honest: + +- `bt visits = N² + N + 1` — one `Scan` of the single `f`-class, N + `Bind`s of `f` e-nodes, and N `Bind`s of `g` e-nodes under each. + At N = 100: 10,000 + 100 + 1 = 10,101. ✓ +- `gj probes = 5N` — 2N to intersect `a` (N keys in the lead trie, N + probes into the other), 2N for `x` (one key each side, N times), N for + `root`. At N = 100: 500. ✓ + +Speedup doubles as N doubles, which is what a quadratic-over-linear +ratio has to do. It lags the counter ratio badly: +2,561,601/8,000 = **320×** in units of work against **21.7×** measured. +The gap is the cost of a unit. At N = 1600 a `bt` visit is +10152.5 µs / 2,561,601 = **4.0 ns** (a pointer walk down a +`Vec`), while a `gj` probe is 145.0 µs / 8,000 = **18.1 ns** (a +hash lookup) — and the trie build charges another 322.4 µs, so per +probe the join really costs (145.0 + 322.4) µs / 8,000 = **58.4 ns**. +58.4 / 4.0 = 14.7×, and 320 / 14.7 = 21.8, which is the speedup column. +Asymptotics win anyway, but only from about N = 200 on this machine. + +### Lane 1b — `f(a, g(b))`, the linear pattern (the negative result) + +| N | matches | bt visits | bt µs | gj probes | index µs | gj µs | speedup | +|---|---|---|---|---|---|---|---| +| 100 | 10,000 | 10,101 | 29.2 | 10,103 | 12.8 | 48.4 | 0.48x | +| 400 | 160,000 | 160,401 | 423.4 | 160,403 | 41.9 | 714.7 | 0.56x | +| 1600 | 2,560,000 | 2,561,601 | 6476.3 | 2,561,603 | 175.9 | 11290.4 | 0.56x | + +`gj probes = N² + N + 3`. No equality constraint, so every candidate is +an answer and there is nothing to prune: the join does the same work +through a more expensive instruction. Generic join is **1.8× slower** +and that is the correct outcome. POPL'22 measures the same thing (Table +1, "Worst" 0.03; §5.2: "Speedup tends to be greater when the output size +is smaller"). + +### Lane 2 — one iteration, naive + +60,000 tuples, then a delta of 24 tuples (8 new constants): +**20,008 matches re-derived, 100,040 probes, 11.0 ms** — for 8 new +answers. The whole cost of naive evaluation in one row. + +The probe count is exact and reproduces everywhere; the µs is the noisiest +figure in this topic — repeat runs on the same machine span **6.5–11.0 ms**, +because this lane materialises 20,008 substitution vectors and is therefore +partly an allocator benchmark. Compare probes, not milliseconds, when you +implement the stub. + +### Lane 3 — triangle multi-pattern, generic join only + +| V | E | matches | gj probes | gj µs | +|---|---|---|---|---| +| 200 | 1000 | 129 | 10,155 | 94.0 | +| 400 | 2000 | 123 | 20,163 | 198.3 | +| 800 | 4000 | 123 | 39,865 | 353.8 | +| 1600 | 8000 | 138 | 79,416 | 839.5 | + +Expected matches `(E/V)³ = 125` (each 3-cycle found three times, once +per rotation) — the answer size is flat while the graph grows 8×, and +generic join's probes grow linearly in E. + +## Predictions (fill BEFORE implementing the stubs) + +| question | prediction | actual | +|---|---|---| +| semi-naive probes for a 24-tuple delta (naive: 100,040) | | | +| semi-naive µs vs naive's 11.0 ms — ratio? | | | +| how many of the 8 answers does *each* of the m delta rules produce? | | | +| duplicates across delta rules on this query — how many? | | | +| binary join's largest intermediate at V=1600, E=8000 (est. E²/V) | | | +| binary join µs vs generic join's 839.5 µs at the last row | | | +| does binary join's intermediate grow linearly or quadratically here? | | | +| at what N does lane 1a's speedup cross 1.0 if you cache the tries? | | | + +## Implementation log + +- [ ] `semi_naive::delta_matches` — both tests green +- [ ] `binary_join::binary_join` — both tests green +- [ ] prediction table reconciled +- [ ] stretch: cache tries across iterations (exercise 4) and re-measure + lane 2 — the `+idx` / `−idx` distinction of POPL'22 Table 1 +- [ ] stretch: congruence closure as a rule over the database + (exercise 5), checked against `EGraph::rebuild` + +Surprises / dead ends: + +- The first version of `gj` allocated a `Vec` per intersection key. It + did not change any counter and it halved the wall clock — a reminder + that when the counters and the clock disagree, the clock is measuring + your allocator, not the algorithm. + +## Paper numbers worth keeping + +- E-matching is **60–90%** of equality saturation's run time (POPL'22 + §1, citing egg's POPL'21 measurements). That is the size of the prize. +- POPL'22 Table 1, `math` at 217,396 e-nodes, index building excluded: + best ratio **8,575,830×**, median **80.84×**, worst **0.76×**. Six + orders of magnitude of upside and a real downside, in one row. +- POPL'22 §5: relational e-matching is ~80 lines inside egg plus a + generic-join library under 500 lines; egg's own e-matcher is ~500 + lines "interconnected to various other parts of egg". +- PLDI'23 §5.3: at iteration 100 on the `math` suite, egglog without + semi-naive is **3.34×** faster than egg (same e-graph); with + semi-naive, **9.27×** (and a slightly larger e-graph). Measured on an + M2 with 16 GB (footnote 8). +- PLDI'23 §5: egglog is ~4,200 lines of Rust. (It has since grown a + `core-relations` crate that is a database in its own right.) + +## Questions from the reading guides + +- [reading-relational-ematching.md](reading-relational-ematching.md) — answers: +- [reading-egglog-pldi23.md](reading-egglog-pldi23.md) — answers: +- [reading-egglog-source.md](reading-egglog-source.md) — answers: +- [reading-free-join.md](reading-free-join.md) — answers: + +## Cross-topic threads + +- Semi-naive evaluation = incremental view maintenance (27) for a + monotone query. Delta rules are DBSP's join expansion. +- Row timestamps + `GeConst` = LSM sequence numbers + "everything since" + (4). Deferred rebuild = deferred compaction. +- Generic join / AGM = topic 10's join ordering with a worst-case bound + instead of a cost model; `plan.rs`'s min-fill elimination is a + join-order search. +- The triangle query is topic 24's triangle counting, executed by a join + engine rather than a graph kernel. +- An e-graph over sound rewrites is a generator of equivalent queries — + topic 16's metamorphic oracle, with a proof attached. + +## M44 log (capstone) + +- [ ] relational rewrite stage in the planner, both numbers reported + (plan cost vs hand pass; match time vs backtracking) +- [ ] timestamped e-node table, semi-naive saturation loop +- [ ] one cyclic rewrite pattern, binary plan measured next to GJ + +## Done when + +- both stubs green and the prediction table reconciled; +- you can say, without looking, which of lane 1a and lane 1b generic + join loses and why — and predict it from the pattern alone; +- lane 3's intermediate measured rather than estimated; +- guide questions answered; M44 outline drafted. diff --git a/topics/44-egraphs-egglog/reading-egglog-pldi23.md b/topics/44-egraphs-egglog/reading-egglog-pldi23.md new file mode 100644 index 0000000..baa8720 --- /dev/null +++ b/topics/44-egraphs-egglog/reading-egglog-pldi23.md @@ -0,0 +1,507 @@ +# egglog: a Datalog engine that happens to be an e-graph + +The previous chapter ends on an unfinished sentence. Relational +e-matching turns the e-graph into a database *whenever you want to +match*, and POPL'22 §6.4 flags the obvious cost: the translation is +rebuilt from scratch, which is only affordable because matching happens +in big batches between rebuilds. **"Better Together: Unifying Datalog +and Equality Saturation"** — Zhang, Wang, Flatt, Cao, Zucker, Rosenthal, +Tatlock and Willsey, PLDI 2023 (arXiv:2304.04332) — is what happens when +you stop translating and make the database primary. + +The claim is bigger than a performance one. egglog is a **Datalog +engine with two extensions** — user-extensible equality, and functions +with a `:merge` expression — and those two extensions are enough to make +equality saturation a special case. Congruence closure stops being a +built-in algorithm and becomes what a particular `:merge` does. Once +that is true, everything Datalog knows — semi-naive evaluation, +lattices, stratification, query optimisation — applies to e-graphs for +free. + +This chapter builds the Datalog vocabulary from scratch, works +`:merge` and semi-naive evaluation on concrete numbers, and closes on +what the paper measured and what it gave up. Read +[reading-relational-ematching.md](reading-relational-ematching.md) +first; this one assumes its Steps 5–7 (atoms, bodies, join variables). + +## The problem in one sentence + +Equality saturation needed the things Datalog has (incremental +evaluation, lattice-valued analyses, a query optimiser) and Datalog +needed the thing equality saturation has (a fast, built-in equivalence +relation) — and each community had been building bad versions of the +other's feature until someone noticed that a **function whose merge +operation is `union` is exactly congruence closure**. + +## The concepts, step by step + +### Step 1 — Datalog, in the amount this chapter needs + +> **In:** nothing. **Out:** the six words — fact, rule, body, head, +> immediate consequence, fixpoint — that Steps 4 and 7 restate for +> egglog. + +A **Datalog program** is a set of relations and a set of rules. A +**fact** is a tuple asserted directly; a **rule** has a head and a body, + +``` + TC(x, y) :- TC(x, z), E(z, y). +``` + +read as: *whenever* the body's atoms can all be matched by one +assignment of the variables, add the head to the database. Body +matching is exactly the conjunctive query of the previous chapter. + +Evaluation applies the **immediate consequence operator** `T_P` — fire +every rule once against the current database, collect all the heads — +and repeats until nothing new appears. That is the **fixpoint**, and it +exists because ordinary Datalog is **monotone**: rules only ever add +tuples, so the database grows and, being finite, must stop. + +The paper's Figure 1 runs the classic example, and the trace is worth +copying because Step 7 measures against it: + +``` + E(1,2). E(2,3). E(3,4). iter E TC + TC(x,y) :- E(x,y). 0 ∅ ∅ + TC(x,y) :- TC(x,z), E(z,y). 1 {(1,2),(2,3),(3,4)} ∅ + 2 … {(1,2),(2,3),(3,4)} + 3 … … (1,3),(2,4) + 4 … … (1,4) +``` + +Note iteration 3. It re-derives (1,2), (2,3) and (3,4) — every tuple +found in iteration 2 — because the rule body is checked against the +whole database again. That waste is Step 7's subject. + +### Step 2 — what each side was missing + +> **In:** Step 1's Datalog, and equality saturation from topic 21. +> **Out:** the two concrete failures the paper opens with, which are the +> reason the unification is not just elegant. + +Paper §1 names one on each side, and both are real systems: + +- **Herbie** (a floating-point accuracy optimiser) uses equality + saturation with rules that are *unsound*: `x/x → 1` is only valid for + `x ≠ 0`, and equality saturation has no good way to express the + condition. So Herbie runs with the unsound rules and then validates + and discards results afterwards — and cannot run saturation for + longer, because more iterations means more unsoundness. +- **cclyzer++** (an LLVM points-to analysis in Datalog) needed + Steensgaard-style unification — a union-find — and found Datalog's + built-in equivalence relations too slow, so it wrote "an ad-hoc + implementation of union-find", whose complexity "led to bugs in the + pointer analysis". + +One system wants Datalog's analyses inside its e-graph; the other wants +an e-graph's union-find inside its Datalog. §1: "EqSat struggles to +support rich analyses, and equational reasoning in Datalog is complex +and slow." + +### Step 3 — functions, not relations + +> **In:** Step 1's notion of a relation. **Out:** egglog's storage +> model, and the constraint that makes `:merge` necessary. + +egglog stores data as **partial functions**, not relations (§3.2). +Every user-defined function is backed by a **map** rather than a set, +and a relation is sugar: an n-ary relation `R` is a function to the +built-in `unit` type, defined exactly where the tuple is present. + +The map enforces something a set cannot: a **functional dependency** +from the argument columns to the output column. `f(v₁ … v_k)` has at +most one output value, always. In relational terms, egglog's tables all +have a declared key — which is also what an e-graph's hashcons +guarantees (previous chapter, Step 6), now stated as a schema property +rather than an implementation trick. + +The paper uses "table" for both the map behind a function and the set +behind a relation, and so will this chapter. + +### Step 4 — `:merge`, worked on shortest paths + +> **In:** the functional dependency of Step 3. **Out:** what happens +> when a rule tries to violate it, and why the answer is a lattice. + +If `path(1,3) ↦ 30` is already in the table and a rule fires with +`(set (path 1 3) 20)`, the functional dependency is about to break. A +`:merge` expression says how to resolve it. Paper Figure 3b: + +```lisp +;; paper Figure 3b, lines 1-2 and 6-7 — reachability with path length + 1 (function edge (i64 i64) i64) + 2 (function path (i64 i64) i64 :merge (min old new)) + 6 (rule ((= (path x y) xy) (= (edge y z) yz)) + 7 ((set (path x z) (+ xy yz)))) +``` + +With `(set (edge 1 2) 10)`, `(set (edge 2 3) 10)`, `(set (edge 1 3) 30)`: + +``` + the direct edge is found first path(1,3) ↦ 30 + the two-hop rule fires set(path(1,3), 10 + 10) = 20 + conflict, so evaluate :merge (min old new) = (min 30 20) = 20 + result path(1,3) ↦ 20 ✓ paper prints 20 +``` + +Some vocabulary, because the paper's next sentence uses it. A +**partial order** `⊑` is a reflexive, antisymmetric, transitive +relation. A **lattice** over a domain adds a **join** `⊔`: the least +element that is above both arguments (their *supremum*). `min` looks +like the wrong direction until you read the paper's own definition +(§3.2): it is the join of the **min lattice**, where `x ⊑ y ⟺ x ≥ y`. +Order the values by *worseness* and taking the minimum is climbing. + +This is the same construction as Flix's lattice semantics and as egg's +e-class analyses (topic 21, Step 9), but egglog does not require the +`:merge` expression to be a lattice join at all — it can be any egglog +expression. That freedom is what Step 6 needs. + +### Step 5 — sorts, ids, and get-or-make-set + +> **In:** Step 3's functions. **Out:** egglog's equality, and the one +> operation that turns a function call into an e-node. + +A **sort** declared by the user is "a set of opaque integer values +called ids and an equivalence relation over those ids" (§3.3), +implemented by a union-find. Two ids are equal iff they canonicalise to +the same id, and **egglog keeps every id in the database canonical**. +Those ids are e-class ids; the paper says so. + +`union` is an action that merges two ids of a user-defined sort. Values +of *base* types (`i64`, `String`) cannot be unioned — they are only +equal to themselves — which is what keeps the constant `2` from +accidentally becoming the constant `3`. + +Then the small mechanism that carries the most weight. A function may +declare a `:default`, and calling `(f x)` is a lookup that falls back to +it: "Calling a function `(f x)` will first see if the map for function +`f` defines an output for `x`. If so, it returns that output. Otherwise, +egglog evaluates the `:default` expression, stores the result in the +map, and returns it" (§3.3). For a function returning a user-defined +sort the default default is **make-set**: mint a fresh union-find id. + +So calling a constructor is a **get-or-make-set**. Read that next to +topic 21's `EGraph::add`, which is a hashcons lookup that inserts a new +e-class on a miss. They are the same operation, arrived at from +opposite directions. + +### Step 6 — congruence, as a consequence rather than an algorithm + +> **In:** Steps 3–5: the functional dependency, `:merge`, and unionable +> ids. **Out:** the paper's central identification, worked on a +> two-entry table. + +Constructors of a `datatype` get `:merge` = `union` (§3.4). Watch what +that alone produces. Take `Add`'s table with two entries: + +``` + Add: (a, b) ↦ c + (a, d) ↦ e with b ≠ d, c ≠ e +``` + +Now a rule unions `b` and `d`, and `b` becomes canonical. egglog +canonicalises the database, so the second row is rewritten: + +``` + Add: (a, b) ↦ c + (a, b) ↦ e ← the functional dependency is violated +``` + +The conflict invokes `Add`'s `:merge`, which is `union`, so `c` and `e` +are unioned — and that is precisely the congruence axiom: +`b ≡ d ⟹ Add(a,b) ≡ Add(a,d)`. Unioning `c` and `e` may in turn break +another table's dependency, so the process repeats to fixpoint. + +**Congruence closure is not implemented in egglog. It is what +maintaining a functional dependency under a union-find does.** Compare +topic 21: egg's `rebuild` is a hand-written worklist algorithm with the +congruence invariant baked in. Here it is a schema constraint plus a +merge policy, and `min` in the same slot gives you shortest paths +instead. + +The paper's formal version (§4.2) is two operators applied +alternately: the inflationary immediate consequence operator `T_P↑`, +which fires the rules and may produce a **pre-instance** (a database +whose functional dependencies are broken), and the **rebuilding +operator** `R`, whose `≡_R` is the equivalence closure of the current +equality plus every pair `(n₁, n₂)` such that some `f(v₁…v_k)` maps to +both. `R^∞` is that run to fixpoint. + +One footnote worth stopping on (§4.2, footnote 4): egglog's consequence +operator has to union with the old database explicitly because, unlike +standard Datalog, **egglog rules are not always monotone**. The example +given is a rule reading a lower-bound analysis, `Q(e) :- lo(e) ↦ 5` — +`lo(e)` can *increase* over time, so a fact derivable now may not be +derivable later. Monotonicity was the reason Datalog terminates; egglog +keeps termination by making the database inflationary by construction +instead. + +### Step 7 — semi-naive evaluation, and the duplicates it creates + +> **In:** Step 1's re-derivation waste and Step 6's two operators. +> **Out:** the delta-rule expansion, worked on this topic's lane 2 — +> including the exact number of duplicate derivations it produces. + +Naive evaluation re-derives everything every iteration (Step 1's trace, +iteration 3). **Semi-naive** evaluation (§4.3) keeps a differential +database `ΔDB_i` of the tuples that are new or updated this iteration, +and expands each rule into one **delta rule** per body atom: + +``` + A :- A₁ … A_m ⇒ A :- A₁ … A_{j-1}, ΔA_j, A_{j+1} … A_m + for each j ∈ 1…m +``` + +The j-th delta rule ranges atom j over the new tuples and every other +atom over the whole database. Their union is exactly the derivations +that use at least one new tuple — and Theorem 4.1 says the semi-naive +evaluation of an egglog program produces the same database as the naive +one, which is the property you actually need. + +Work it on lane 2 of this topic's bench. The query has m = 2 atoms: + +``` + Q(root, a) ← R_f(root, a, x), R_g(x, a) +``` + +The e-graph has 20,000 constants (60,000 tuples); then 8 constants +arrive, contributing 8 new `R_f` tuples, 8 new `R_g` tuples and 8 new +constant tuples — 24, which is what the lane prints. The two delta +rules: + +``` + j = 1: ΔR_f(root, a, x), R_g(x, a) 8 new f-tuples ⋈ full R_g → 8 matches + j = 2: R_f(root, a, x), ΔR_g(x, a) full R_f ⋈ 8 new g-tuples → 8 matches + union → 16 + dedup → 8 +``` + +**Every one of the 8 answers is derived twice**, because each involves +one new `f` tuple *and* one new `g` tuple, so both delta rules find it. +That is not a bug in the expansion; it is inherent to "at least one +atom is new", and it is why `semi_naive::delta_matches` must +deduplicate. Set that against the naive column the lane prints today — +**20,008 matches, 100,040 probes, 11.0 ms** — and you have the whole +argument in two rows. + +The general shape: semi-naive replaces one query over the full database +with m queries, each with one small atom. It wins when the delta is +small relative to the database, which in a saturation loop is true from +about iteration three onwards, and it loses when the delta is most of +the database, which is true on iteration one. + +### Step 8 — what it measured + +> **In:** Steps 6–7. **Out:** the paper's numbers, and which of them is +> attributable to which idea. + +§5.3, the microbenchmark, is designed to separate the two contributions. +Three systems on egg's `math` suite, populated with the same initial +terms, run with egg's default BackOff scheduler for 100 iterations, +median of seven runs, on an M2 with 16 GB (footnote 8): + +| system | what it isolates | result at iteration 100 | +|---|---|---| +| `egg` | the baseline | — | +| `egglogNI` | relational matching + query optimiser, **no** semi-naive | grows *the same e-graph* **3.34×** faster | +| `egglog` | plus semi-naive | **9.27×** faster, and a slightly larger e-graph | + +The `egglogNI` row is the one that matters for attribution: it produces +the identical e-graph, so 3.34× is purely better joins — the previous +chapter's contribution, engineered. The extra step to 9.27× is +semi-naive evaluation, and egglog explores *more* in that time, which is +why the paper is careful to say "slightly larger e-graph" rather than +claiming a clean speedup. + +The case studies (§6): + +- **Points-to analysis** (§6.1): a Steensgaard-style unification-based + analysis, where Datalog's weakness was equality. egglog is **4.96×** + faster than `patched` (the fastest *sound* Soufflé encoding + available), **1.94×** faster than cclyzer++, and **1.59×** faster than + egglogNI. +- **Herbie** (§6.2): egglog's analyses let the unsound rewrites be + guarded, so Herbie can saturate longer. The honest summary is in the + paper's own count: in **104** benchmarks the sound analysis finds a + *more* accurate program than the unsound ruleset, and in **135** the + unsound ruleset still wins. Soundness bought the ability to run + longer, not uniformly better answers. + +### Step 9 — what egglog gives up + +> **In:** everything above. **Out:** the honest boundary, so the choice +> between egg and egglog is a choice rather than a fashion. + +- **It is a language, not a library.** §5.2 argues this is a feature — + the compiler sees the guards, rules are typechecked, and a program can + declare many sorts and functions instead of egg's "single, ad-hoc + datatype". The cost is that a host-language escape hatch (an arbitrary + Rust closure in a conditional rewrite) is no longer free. +- **The core semantics is a subset.** §4 is defined over *core egglog*, + which has one atom in the head, no `union` action, and `:merge` + restricted to union-on-ids and lattice-join-on-constants. Full egglog + allows any expression there, and the theorems are not stated for it. +- **Non-monotone rules are allowed** (Step 6's footnote), which means + the reassuring Datalog story — "monotone, therefore a least fixpoint, + therefore order does not matter" — does not transfer wholesale. +- **The paper's own scale.** §5: "approximately 4,200 lines of Rust". + The implementation guide in this topic reads a codebase that has since + grown a separate `core-relations` crate with its own query planner; + the 2023 numbers were measured on the smaller thing. + +## How to read the paper (with the concepts in hand) + +1. **§1** — the two failing systems. It is the motivation and it is + concrete; do not skip it for the abstract. +2. **§2** is background; if Step 1 landed, skim it. +3. **§3** is the language tour and is best read at a terminal with + egglog installed, one figure at a time. Figures 3a → 3b → 4a → 4b is + a deliberate escalation: Datalog, then lattices, then unification, + then equality saturation, each one figure apart. +4. **§4.2** — read the definition of `R`, the rebuilding operator, next + to Step 6's worked table, and read footnote 4 rather than skipping it. +5. **§4.3** is one page and is Step 7. +6. **§5.1** for the implementation's shape, **§5.3** for the numbers + with Step 8's attribution table in view. +7. **§6.1** if you care about program analysis, **§6.2** if you care + about what "sound" costs in practice. + +## Where each step lives in the code + +Anchors are `egraphs-good/egglog` at the pinned commit; the next chapter +reads them properly. + +| step | where | +|---|---| +| 3, functions as maps | `core-relations/src/table/mod.rs:1-5` — a general table; "timestamp" and "merge function" live above it | +| 5, ids and canonicalisation | `union-find/src/lib.rs:1-12` — and note it is union **by min id**, not by rank | +| 6, rebuilding | `egglog-bridge/src/lib.rs:722` `fn rebuild` | +| 7, semi-naive | `core-relations/src/query.rs:252-256` — one cached plan, re-added each iteration with a `GeConst` timestamp constraint | +| 7, in this crate | `semi_naive.rs` (the stub), lane 2 of `bin/ematch_bench.rs` | + +## Questions (answer in notes.md) + +1. Write the `:merge` expression that makes a function behave like egg's + *interval* e-class analysis (each e-class carries `[lo, hi]`), and + say what lattice it is the join of. What goes wrong if you use `min` + on the lower bound and `min` on the upper? +2. Step 6 shows congruence emerging from `:merge = union`. Write the + converse: an egglog function whose `:merge` is *not* a lattice join + and not `union`, and describe a database on which the result depends + on the order the conflicts are resolved in. +3. Lane 2's delta produces 16 raw derivations for 8 answers. For a rule + with m atoms where the delta touches all of them, how many times is a + single answer derived, and what does that imply about semi-naive's + overhead as rules get wider? +4. §5.3 attributes 3.34× to better joins and the rest of 9.27× to + semi-naive. Design the experiment that would separate the query + *optimiser*'s contribution from the *generic join algorithm*'s. What + would you have to hold fixed? +5. Footnote 4 says egglog rules can be non-monotone. Construct a + two-rule egglog program whose final database depends on the order the + rules fire in, and say which of Datalog's guarantees you have lost. +6. egg needs a separate e-class *analysis* mechanism for facts like + constant folding; egglog uses ordinary rules. Name one thing an + analysis can express that a rule cannot, and one the other way round. + +## Done when + +Answer each before unfolding it. + +- [ ] You can explain why an egglog function needs a `:merge` and a + Datalog relation does not. +
Answer + + A relation is backed by a set: adding a tuple that is already there is + a no-op, and there is nothing to reconcile. An egglog function is + backed by a **map**, which enforces a functional dependency from the + argument columns to the output (§3.2), so two derivations that agree + on the arguments and disagree on the output are a violation, not a + duplicate. `:merge` is the policy for that case — `(min old new)` for + shortest paths, `union` for a constructor. +
+ +- [ ] You can walk the shortest-path example and say why `min` is a + *join* and not a meet. +
Answer + + `path(1,3)` gets 30 from the direct edge, then the two-hop rule fires + with 10 + 10 = 20; `(min 30 20) = 20` and the program prints 20. It is + a join because the lattice is ordered by worseness: §3.2 defines + `x ⊑ y ⟺ x ≥ y`, so the *supremum* of {30, 20} under that order is + the numerically smaller 20. Same operator, inverted order — the sign + error to watch for whenever a paper calls `min` a join. +
+ +- [ ] You can derive congruence closure from `:merge = union` on a + two-row table. +
Answer + + `Add: (a,b) ↦ c, (a,d) ↦ e`. Union `b` and `d`, with `b` canonical. + egglog canonicalises the database, so both rows become `(a,b)`, which + breaks `Add`'s functional dependency. The conflict invokes `:merge`, + which for a constructor is `union`, so `c ≡ e` — the congruence axiom + `b ≡ d ⟹ Add(a,b) ≡ Add(a,d)`. Unioning `c` and `e` may break another + table, so it repeats to fixpoint (§3.4, §4.2's `R`). Congruence is not + a subroutine here; it is what dependency maintenance does. +
+ +- [ ] You can expand a two-atom rule into its delta rules and predict + how many duplicates lane 2 produces. +
Answer + + `Q(root,a) ← R_f(root,a,x), R_g(x,a)` expands to + `ΔR_f, R_g` and `R_f, ΔR_g`. Each of the 8 new answers involves one + new `f` tuple and one new `g` tuple, so both delta rules find all 8: + 16 raw derivations, deduplicated to 8. Against naive's 20,008 matches + and 100,040 probes for the same 8 answers. The duplication is inherent + to "at least one atom is new" and is why `delta_matches` must dedup. +
+ +- [ ] You can state the 3.34× and 9.27× correctly, including what each + is measured against. +
Answer + + §5.3, `math` suite, 100 iterations, median of seven, M2/16 GB. + `egglogNI` — egglog with semi-naive **disabled** — grows *the same + e-graph* as egg and is **3.34×** faster at iteration 100, so that + number is attributable to relational matching and query planning + alone. Full `egglog` is **9.27×** faster and explores a *slightly + larger* e-graph, so the increment is semi-naive evaluation and is not + a like-for-like ratio. Both are against egg, not against a naive + matcher. +
+ +- [ ] You can say what egglog gives up relative to egg. +
Answer + + Host-language escape hatches (guards are egglog expressions, not Rust + closures — §5.2 argues this is worth it); the formal semantics covers + only *core* egglog, with a single head atom, no `union` action and + `:merge` restricted to union-on-ids or a lattice join (§4); and + Datalog's monotonicity guarantee, since egglog rules can be + non-monotone (§4.2 footnote 4), which is why the consequence operator + is inflationary by construction. +
+ +## References + +- Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, + Eli Rosenthal, Zachary Tatlock, Max Willsey, **"Better Together: + Unifying Datalog and Equality Saturation"**, PLDI 2023, + arXiv:2304.04332. §1 (Herbie and cclyzer++), §3.2 (`:merge`, the min + lattice), §3.3 (sorts, `:default`, get-or-make-set), §3.4 (congruence + from `:merge = union`), §4.2 (`T_P↑`, `R`, footnote 4 on + monotonicity), §4.3 + Algorithm 1 + Theorem 4.1 (semi-naive), §5.1–5.3 + (implementation and microbenchmark), §6.1–6.2 (case studies). +- Isaac Balbin, Kotagiri Ramamohanarao, **"A generalization of the + differential approach to recursive query evaluation"**, J. Logic + Programming 1987 — the semi-naive evaluation the paper cites. +- Previous chapter: + [reading-relational-ematching.md](reading-relational-ematching.md). + Next: [reading-egglog-source.md](reading-egglog-source.md), which + reads the engine these ideas turned into. +- Topic 21's [egg chapter](../21-formal/reading-egg-popl21.md) for the + e-class analysis and `rebuild` that Step 6 replaces. diff --git a/topics/44-egraphs-egglog/reading-egglog-source.md b/topics/44-egraphs-egglog/reading-egglog-source.md new file mode 100644 index 0000000..48fb315 --- /dev/null +++ b/topics/44-egraphs-egglog/reading-egglog-source.md @@ -0,0 +1,597 @@ +# Reading egglog: the e-graph that is a database engine + +The two previous chapters are papers. This one is a codebase, and the +reason to read it is that the papers understate what happened. PLDI'23 +describes "approximately 4,200 lines of Rust"; the repository today is a +workspace whose largest crate is called **`core-relations`** and which +contains a table with a clustered sort column, a hash index, a query +planner with hypertree decomposition, a join executor with two +strategies, and a union-find. If you had been handed those files with +the names changed you would call it a small analytical database. + +That is the point worth taking from this chapter. **Congruence closure, +e-matching and rebuilding are not implemented as e-graph algorithms in +egglog. They are a schema constraint, a query, and a rule.** The +engineering underneath is ordinary database engineering, and it is +ordinary database engineering that made it fast. + +Anchors are `egraphs-good/egglog` at the commit `resources/codebases.md` +pins (`e264c37a`), quoted with the line numbers they occupy there. +Read the [POPL'22](reading-relational-ematching.md) and +[PLDI'23](reading-egglog-pldi23.md) chapters first: this one assumes +generic join, delta rules and `:merge`. + +## The problem in one sentence + +Everything the two papers propose has to survive contact with a +representation — where do the tuples live, how do you find the ones a +variable is bound to, how do you say "only the new ones", and what +happens to all of it when a union invalidates half the ids — and +egglog's answers to those four questions are, respectively, a sorted row +buffer, a hash index over columns, a binary search on a timestamp +column, and a rule. + +## The concepts, step by step + +### Step 1 — the map of the workspace + +> **In:** the two papers. **Out:** which crate answers which question, +> so the rest of the chapter has somewhere to put each file. + +``` + egglog/ + src/ the language: parser, typechecker, sorts, + extraction, proofs. This is "egglog" as a user + meets it. + egglog-bridge/ the glue that turns egglog's semantics — + functions, :merge, rebuilding — into rules and + tables for the engine below. + core-relations/ the engine. tables, indexes, query, free_join + (plan + execute), offsets, actions. + union-find/ two union-finds, single-threaded and concurrent. + egglog-ast/, concurrency/, numeric-id/ supporting crates. +``` + +The split is the thesis in directory form. `core-relations` knows +nothing about e-graphs — its table module says so out loud (Step 2) — +and `egglog-bridge` is where "this is an e-graph" is expressed, in terms +the engine already had. + +### Step 2 — the table, field by field + +> **In:** Step 1's map. **Out:** the physical representation every later +> step manipulates, and the deliberate omission at the top of the file. + +```rust +// core-relations/src/table/mod.rs, lines 1-5 — the module's opening claim + 1 //! A generic table implementation supporting sorted writes. + 2 //! + 3 //! The primary difference between this table and the `Function` implementation + 4 //! in egglog is that high level concepts like "timestamp" and "merge function" + 5 //! are abstracted away from the core functionality of the table. +``` + +Read that twice. The engine's table does not know what a timestamp +means; it knows it may be asked to keep rows sorted by some column. It +does not know what congruence is; it knows it may be handed a merge +function. Every e-graph concept enters as a *parameter*. + +```rust +// core-relations/src/table/mod.rs, lines 136-152 — the whole table. +// The line to look at is 143: one nominated column decides the physical order. + 136 pub struct SortedWritesTable { + 137 generation: Generation, + 138 data: Rows, + 139 hash: ShardedHashTable, + 140 + 141 n_keys: usize, + 142 n_columns: usize, + 143 sort_by: Option, + 144 offsets: Vec<(Value, RowId)>, + 145 + 146 pending_state: Arc, + 147 merge: Arc, + 148 to_rebuild: Vec, + 149 rebuild_index: Index, + 150 // Used to manage incremental rebuilds. + 151 subset_tracker: SubsetTracker, + 152 } +``` + +Field by field, in database vocabulary: + +- `data: Rows` — a row buffer. Tuples, contiguously. +- `hash` — a hash index from key columns to row id, **sharded** for + parallel insert. `n_keys` says how many leading columns are the key: + this is the functional dependency of PLDI'23 §3.2, declared. +- `sort_by` + `offsets` — the rows are kept in order of one nominated + column, and `offsets` records where each distinct value of it starts. + A **clustered index**, in other words, and Step 3 is what it is for. +- `merge` — the `:merge` expression, as a function pointer. Congruence + is a value in this field. +- `to_rebuild`, `rebuild_index`, `subset_tracker` — which columns hold + ids that a union can displace, and enough state to repair only the + affected rows. +- `generation` — bumped when the table changes shape enough to + invalidate cached indexes and subsets. Cache invalidation, given a + name. + +### Step 3 — "only the new tuples" is a range scan + +> **In:** Step 2's `sort_by` column. **Out:** the mechanism behind +> PLDI'23's semi-naive evaluation, which turns out to be an index seek. + +The previous chapter left semi-naive evaluation as an expansion into +delta rules. Here is what a delta rule *is*: + +```rust +// core-relations/src/query.rs, lines 252-256 — doc comment on +// add_rule_from_cached_plan (the fn itself is at :257) + 252 /// The primary use-case is seminaive evaluation: an egglog rule is compiled + 253 /// once into a [`CachedPlan`] and then added to a fresh [`RuleSet`] each + 254 /// iteration with timestamp constraints (e.g. `GeConst` on the focus atom) + 255 /// that select only new tuples. If no new tuples exist for an atom, the + 256 /// `None` return allows the caller to skip that variant entirely. +``` + +Three separate ideas in five lines. The plan is compiled **once** and +reused every iteration, so delta rules cost no planning. The delta is +expressed as a **constraint on a column** rather than as a separate +relation. And when an atom has no new tuples, the whole rule variant is +dropped before it runs — the `None` return. + +And the constraint itself is not a filter. Because the timestamp is the +`sort_by` column, `GeConst` becomes a binary search returning a +contiguous range of rows: + +```rust +// core-relations/src/table/mod.rs, lines 497-510 — inside fast_subset (:445). +// Line 499 is the argument: a delta is found, not scanned for. + 497 Constraint::GeConst { col, val } => { + 498 if col == &sort_by { + 499 match self.binary_search_sort_val(*val) { + 500 Ok((found, _)) => { + 501 Some(Subset::Dense(OffsetRange::new(found, self.data.next_row()))) + 502 } + 503 Err(next) => { + 504 Some(Subset::Dense(OffsetRange::new(next, self.data.next_row()))) + 505 } + 506 } + 507 } else { + 508 None + 509 } + 510 } +``` + +`else { None }` is the honest part: on any other column, `fast_subset` +declines and the caller falls back to filtering. This is exactly the +difference between a clustered and an unclustered index, and egglog gets +the clustered one for the only column where it is worth having. + +Work the cost. Lane 2 of this topic's bench has 60,000 tuples and a +delta of 24. A filter costs 60,000 comparisons; a binary search over +~20,000 distinct timestamps costs about `log₂(20,000) ≈ 14` probes and +returns an offset range. The saving is not the constant factor on the +scan — it is that the delta rule never touches the old rows at all. + +### Step 4 — a `Subset` is how "which rows" is represented + +> **In:** the `Subset::Dense` returned in Step 3. **Out:** the one type +> that carries intermediate results through the join, and why it has two +> shapes. + +```rust +// core-relations/src/offsets/mod.rs, lines 333-338 + 333 /// Either or an offset range or a sorted offset vector. + 334 #[derive(Debug, Hash, PartialEq, Eq)] + 335 pub enum Subset { + 336 Dense(OffsetRange), + 337 Sparse(Pooled), + 338 } +``` + +Every intermediate in the executor is a set of row ids, and it is stored +either as a **range** — two integers, when the rows happen to be +contiguous, which is exactly what a timestamp seek produces — or as a +**sorted vector** of row ids. + +Both halves of that choice are cashed in by `Subset::intersect` +(`offsets/mod.rs:402`), which is four cases and no hashing anywhere: + +``` + dense ∩ dense max of the starts, min of the ends — two comparisons :404-411 + dense ∩ sparse two binary searches, then a subslice :413-426 + sparse ∩ dense the same, compacted in place :432-441 + sparse ∩ sparse two-pointer MERGE when the sides are within 4x :447-467 + of each other … + … and GALLOPING into the longer side when they are :468-516 + not — the comment at :470 gives the reason, + "O(other_len * log(cur_len / other_len)) vs + O(cur_len) for retain" +``` + +That is topic 23's postings-list intersection menu — merge for similar +lengths, galloping for skewed ones — chosen by the same size ratio, in a +join engine instead of a search engine. Topic 26's readers will +recognise the storage half as roaring's array-vs-bitmap container +decision, taken per intermediate rather than per block. And `Pooled<…>` +means the sorted vector comes from a pool: allocation on the join path +is treated as a cost worth eliminating, which is the same lesson this +topic's own `gj` learned in `notes.md`. + +### Step 5 — a query, and the plan it is compiled to once + +> **In:** Steps 2–4. **Out:** where the conjunctive query of POPL'22 +> lives in this codebase, and the two-phase compilation it goes through. + +`core-relations/src/query.rs` builds a `Query` from **atoms** — a table +plus a list of variables or constants — and hands it to +`plan_query` (`free_join/plan.rs:1183`), which returns a `Plan`. The +module comment is the best short description of a modern join planner +you will find in a source file, so read it whole; here is its skeleton: + +```rust +// core-relations/src/free_join/plan.rs, lines 3-23 — the two phases. +// Line 13 names the algorithm the first phase is: variable elimination. + 3 //! At a high level, the query planner has two phases: **(hyper)tree decomposition** and **join planning for each bag**. + 4 //! Both phases are very subtle, and heuristics are heavily used for good performance. + 5 //! + 6 //! # (Hyper)tree Decomposition + 7 //! + 8 //! A conjunctive query can be viewed as a hypergraph where variables are vertices and atoms (relations) are hyperedges. + 9 //! The idea of tree decomposition is to break this hypergraph into a tree of overlapping subqueries called *bags*, + 10 //! each of which is cheaper to evaluate independently. This is the classical idea behind tree decomposition and the + 11 //! Yannakakis algorithm. + 12 //! + 13 //! The decomposition proceeds via *variable elimination*: we iteratively pick a variable `v` and eliminate the neighborhood + 14 //! `N(v)` (which also includes `v`) from the hypergraph, and add back a hyperedge consisting of `N(v) - {v}`, until + 15 //! there are no variables left. Each elimination step gives us a bag. A min-fill heuristic + 16 //! (`next_var_to_eliminate`) guides the order of elimination to keep bags small. After all variables are eliminated, + 17 //! redundant bags are pruned: bags subsumed by another (all their variables are covered) are merged, and "ears" + 18 //! are merged into their parent. + // ... 19–20: topologically sort the bags, split message vs private vars ... + 21 //! The materialized result of each bag has its output keyed on the *message variables* it shares with + 22 //! its parent, and the parent uses that materialization to prune its own search space. + 23 //! +``` + +Vocabulary, defined here because the comment assumes it: + +- The **query hypergraph** is the one from the POPL'22 chapter, Step 8: + a vertex per variable, a hyperedge per atom. +- A **tree decomposition** covers that hypergraph with **bags** — sets + of variables — arranged in a tree, such that every atom fits inside + some bag and every variable's bags form a connected subtree. An + **acyclic** query is one with a decomposition whose bags are single + atoms. +- **Yannakakis' algorithm** evaluates an acyclic query in time linear in + input plus output by passing *semijoin messages* up and down that + tree, so that no bag ever materialises a tuple that cannot survive. +- **Variable elimination** builds a decomposition greedily: repeatedly + remove a variable and connect its neighbours. The **min-fill** + heuristic picks the variable that adds the fewest new connections — + the standard heuristic from probabilistic graphical models, here + scoring on atom occurrences and column cardinality estimates + (`plan.rs:420` `next_var_to_eliminate`, whose body at `:441-452` + counts occurrences and consults a size estimate). +- **Message variables** are the ones a bag shares with its parent — the + join keys of the semijoin, and the columns the bag's materialised + result is keyed on. + +That is topic 10's optimizer, in a system with no SQL in it. And note +what the comment says about the fallback: "When the query hypergraph is +a single connected component with no beneficial decomposition, the +planner falls back to a `SinglePlan` with no materialization steps." +A planner that knows when not to plan. + +### Step 6 — two join strategies, and the space between them + +> **In:** the bags of Step 5. **Out:** what actually runs inside one +> bag, and where generic join sits relative to a hash join. + +```rust +// core-relations/src/free_join/plan.rs, lines 32-41 — the strategies. +// Line 38 is the sentence to keep: one plan space, two familiar corners. + 32 //! - **Generic Join** (`PlanStrategy::Gj`): The classic worst-case optimal join algorithm. Each stage picks one variable + 33 //! and intersects the columns of atoms that correspond to this variable (`JoinStage::Intersect`). + 34 //! + 35 //! - **Free Join** (`PlanStrategy::PureSize` / `PlanStrategy::MinCover`): From Remy's paper. The planning algorithm + 36 //! does the following: Each stage it selects a *cover* — a (sub)atom whose columns span the variables being bound in that step — and + 37 //! uses it to probe all other atoms that share those variables (`JoinStage::FusedIntersect`). When the cover is an + 38 //! entire atom and there is only one relation to probe, this degenerates to a hash join; when covers are single-column + 39 //! scans it ~ recovers generic join*. + 40 //! + 41 //! *: although this is not worst-case optimal because it does not necessarily picks the smallest side to scan. +``` + +`Gj` is the algorithm this topic's `relational.rs` implements. +`MinCover` is the [Free Join](reading-free-join.md) plan space, and the +footnote at line 41 is the honest caveat: the production default is not +worst-case optimal, because picking a cover is not the same as always +scanning the smallest side. Worst-case optimality is a property the +engine will trade for speed, deliberately, and says so in a comment. + +### Step 7 — the executor, doing the thing the bound requires + +> **In:** a `JoinStage::Intersect` from Step 6. **Out:** the production +> version of `relational.rs`'s "iterate the smallest, probe the rest". + +```rust +// core-relations/src/free_join/execute.rs, lines 1460-1469 — the two-scan +// intersection. Line 1465 is the whole O(min |R_j.x|) requirement. + 1460 [a, b] => { + 1461 let a_prober = self.get_column_index(atoms, binding_info, a.atom, a.column); + 1462 let b_prober = self.get_column_index(atoms, binding_info, b.atom, b.column); + 1463 + 1464 let ((smaller, smaller_scan), (larger, larger_scan)) = + 1465 if a_prober.len() < b_prober.len() { + 1466 ((&a_prober, a), (&b_prober, b)) + 1467 } else { + 1468 ((&b_prober, b), (&a_prober, a)) + 1469 }; +``` + +Compare our own, which is the same decision written for two to eight +atoms instead of specialised at two: + +```rust +// relational.rs, lines 199-203 (this topic's crate) + 199 // Intersect smallest-first, which is what buys the O(min |R_j.x|) bound. + 200 let lead = *part[..n_part] + 201 .iter() + 202 .min_by_key(|&&i| cur[i].kids.len()) + 203 .expect("non-empty"); +``` + +Two details in the surrounding production code that our version does not +have, and that are worth knowing exist. First, a size threshold: at +`execute.rs:1431` a subset of 16 rows or fewer is refined directly, +while a larger one goes through `get_cached_trie_node` (`:1439`) — the +trie node is *built lazily and cached*, so the index is materialised +only where it pays. Second, results are accumulated into `FrameUpdates` +and drained in **chunks** (`:1453`), which is what lets the join run in +parallel — vectorised execution, in topic 11's sense, arriving for the +same reason it arrived there. + +### Step 8 — rebuilding is a rule + +> **In:** everything above. **Out:** the answer to "where is congruence +> closure implemented", which is: nowhere, on purpose. + +Topic 21 read egg's `rebuild` — a hand-written worklist that repairs the +congruence invariant. Look for its equivalent here and you find a +*rule builder*: + +```rust +// egglog-bridge/src/lib.rs, lines 951-957 — inside incremental_rebuild_rule (:945). +// The comment on 954 is the whole design. + 951 let subsume = self.funcs[table].can_subsume; + 952 let table_id = self.funcs[table].table; + 953 let uf_table = self.uf_table; + 954 // Two atoms, one binding a whole tuple, one binding a displaced column + 955 let mut rb = self.new_rule(&format!("incremental rebuild {table:?}, {col:?}"), true); + 956 rb.set_plan_strategy(PlanStrategy::MinCover); + 957 let mut vars = Vec::::with_capacity(schema.len()); +``` + +Rebuilding is compiled, per table and per id-typed column +(`incremental_rebuild_rules`, `:932`), into a two-atom query: find a +tuple, join it against the union-find table on a column whose id has +been displaced, and write the canonical version back. It is planned by +the same planner (`MinCover` is chosen for it explicitly) and executed +by the same executor. There is a `nonincremental_rebuild` (`:994`) +alongside it for the case where scanning everything is cheaper, and +`EGraph::rebuild` (`:722`) picks between them — including a short-circuit +at `:703` that skips the full rebuild when no unions happened. + +This is what "unifying Datalog and equality saturation" cashes out to. +Every optimisation the query engine gains — a better plan, a lazily +built index, chunked parallel execution — is inherited by congruence +closure, because congruence closure is a query. + +### Step 9 — the union-find that declines the textbook + +> **In:** the union-find referenced by Step 8's rule. **Out:** a +> deliberate asymptotic sacrifice, and the reason for it. + +```rust +// union-find/src/lib.rs, lines 6-12 — the crate's own justification + 6 //! Both structures are fairly rudimentary and are customized to be used in an + 7 //! egraph-related setting. In particular, they do "union by min id", which is a + 8 //! strategy that _does not_ guarantee the same asymptotic complexity as the + 9 //! main techniques in the literature (e.g. union by rank). Union by min is a + 10 //! heuristic introduced to reduce the number of ids perturbed during congruence + 11 //! closure. There's likely more to do in this area but for now it seems to work + 12 //! well enough. It doesn't hurt that it's also simpler to implement. +``` + +**Union by rank** attaches the shorter tree under the taller one, which +with path compression gives the near-constant `O(α(n))` amortised bound +every textbook quotes. **Union by min id** instead always keeps the +numerically smaller id as the representative — giving up that bound on +purpose. + +Why is it worth giving up? Because in this system a union's real cost is +not the union-find operation, it is everything downstream: every row +whose id stops being canonical has to be rewritten by Step 8's rebuild +rule. Keeping the smaller id stable means an id that has been canonical +for a long time — and therefore appears in many rows — tends to stay +canonical. **The union-find is optimised for the rebuild it triggers, +not for itself.** + +Topic 21 found egg making the same kind of choice for the same kind of +reason (its `find(&self)` does not path-compress, because the read path +takes `&self`). Two independent implementations, two textbook +optimisations declined, both because the union-find is embedded in +something bigger. + +## How to read the source (with the concepts in hand) + +A two-hour path, top-down, that stays on the database side: + +1. `core-relations/src/free_join/plan.rs`, **lines 1-46**. The module + comment. Everything else is easier afterwards. +2. `core-relations/src/table/mod.rs`, **lines 1-5 and 136-172**. The + doc, the struct, and the `Clone` impl right after it — which is a + good check on your reading, because what it chooses *not* to clone + (the indexes) tells you what is derived state. +3. `fast_subset` (`table/mod.rs:445-512`) in full: five constraint kinds, + one of which is fast and only on the sorted column. +4. `core-relations/src/offsets/mod.rs:333` and the `Offsets` trait above + it — 20 lines, and every intermediate in the engine is one of these. + Then `intersect` at `:402-519`, which is a compact tour of set + intersection strategies. +5. `core-relations/src/query.rs`, the `RuleSetBuilder` API, ending at + `add_rule_from_cached_plan` (`:257`). +6. `free_join/execute.rs:1418-1560`, the `Intersect` stage at one, two + and many scans. Skim the parallel machinery; read the size threshold + at `:1431`. +7. `egglog-bridge/src/lib.rs:932-1050`, the rebuild rules, then `:722` + for how they are driven. +8. `union-find/src/lib.rs` entire — 104 lines. + +Then, for contrast, re-read this topic's `relational.rs` (250 lines) and +list what it is missing. That list is the difference between an +algorithm and an engine. + +## Where each step lives in the code + +| step | file:line | +|---|---| +| 2, the table | `core-relations/src/table/mod.rs:1-5`, `:136-152` | +| 3, delta as a seek | `core-relations/src/query.rs:252-256`, `table/mod.rs:445` `fast_subset`, `:497-510` `GeConst`, `:983` binary search | +| 4, intermediates | `core-relations/src/offsets/mod.rs:333-338`, `:402-519` `intersect` | +| 5, the planner | `free_join/plan.rs:1-46` (doc), `:1183` `plan_query`, `:420` `next_var_to_eliminate` | +| 6, strategies | `free_join/plan.rs:32-41`, `:134-158` `JoinStage` | +| 7, the executor | `free_join/execute.rs:1418` `Intersect`, `:1431` size threshold, `:1460-1469` smaller-first, `:1453` chunking | +| 8, rebuilding | `egglog-bridge/src/lib.rs:932`, `:945`, `:994`, `:722`, `:703` | +| 9, union-find | `union-find/src/lib.rs:1-12`, `:55` `union` | +| this topic's toy | `relational.rs:78` `index_atom`, `:116` `plan`, `:170` `gj` | + +## Questions (answer in notes.md) + +1. `SortedWritesTable` has one `sort_by` column. If you wanted a second + sort order — say, to make a different atom's delta a range scan too — + what would you have to add, and what would it cost on the write path? + Compare with a second clustered index in postgres (topic 3). +2. `fast_subset` returns `None` for a `GeConst` on any column other than + `sort_by`. Trace what the caller does with that `None` + (`free_join/mod.rs:805` `split_fast_slow`) and describe the fallback + in database terms. +3. The min-fill heuristic (`plan.rs:420`) scores variables by occurrence + count and column cardinality. Our `relational.rs::plan` scores by + atom count then relation size. Construct a query where the two + orderings differ and say which is better and why. +4. Step 6's footnote says the Free Join strategies are not worst-case + optimal. Write the query and database where `MinCover` does + asymptotically more work than `Gj`, and then argue why the default is + still the right default. +5. Rebuilding as a rule (Step 8) means congruence closure is planned. + What would a *bad* plan for the incremental rebuild rule look like, + and what in the schema stops the planner from choosing it? (Hint: + `n_keys`, and PLDI'23 §3.2.) +6. Union by min id trades the `O(α(n))` bound for fewer perturbed ids. + Design the measurement that would decide whether the trade pays on + the Figure 2 e-graph, and predict the result before running it. + +## Done when + +Answer each before unfolding it. + +- [ ] You can say what `core-relations` deliberately does not know, and + why that matters. +
Answer + + It does not know what a timestamp is or what a merge function means — + `table/mod.rs:1-5` says both are "abstracted away from the core + functionality of the table". A timestamp is just the column named in + `sort_by`; congruence is just a value in the `merge` field. That + separation is what lets the same engine run Datalog, lattice analyses + and equality saturation, and it is why `egglog-bridge` exists: it is + the only crate that knows the parameters mean "e-graph". +
+ +- [ ] You can explain how a delta rule finds its tuples without scanning. +
Answer + + The rule's plan is compiled once and re-added each iteration with a + `GeConst` constraint on the focus atom's timestamp column + (`query.rs:252-256`). Because that column is the table's `sort_by` + column, `fast_subset` answers the constraint with a binary search + (`table/mod.rs:497-510`, `:983`) and returns a `Subset::Dense` — a + contiguous offset range. It is an index seek on a clustered index. On + any other column `fast_subset` returns `None` and the caller filters + instead. +
+ +- [ ] You can name the planner's two phases and what each produces. +
Answer + + Phase one is **hypertree decomposition** by variable elimination with + a min-fill heuristic (`plan.rs:3-18`, `:420`): it breaks the query + hypergraph into a tree of *bags*, prunes subsumed bags and ears, and + chooses each bag's *message variables* — the ones shared with its + parent, which its materialised result is keyed on. That is Yannakakis' + semijoin idea. Phase two plans the join *inside* each bag as a list of + `JoinStage`s, using either `Gj` (generic join, one variable per stage) + or Free Join (`PureSize`/`MinCover`, a cover per stage). A `JoinHeader` + applies constant constraints before the loop starts. +
+ +- [ ] You can point at the line in production code that implements + generic join's `O(min |R_j.x|)` requirement. +
Answer + + `execute.rs:1464-1469`: with two scans, the executor compares + `a_prober.len()` and `b_prober.len()` and iterates the smaller, + probing the larger. That is the same decision as `relational.rs:200`'s + `min_by_key`, specialised to the two-atom case. Around it are two + things the toy lacks: a 16-row threshold below which a subset is + refined directly instead of indexed (`:1431`, `:1439`), and chunked + draining of results so the stage can run in parallel (`:1453`). +
+ +- [ ] You can say where congruence closure is implemented in egglog. +
Answer + + It is not, as an algorithm. `egglog-bridge/src/lib.rs:945` + `incremental_rebuild_rule` *compiles a rule*: two atoms, one binding a + whole tuple and one binding a displaced column + (comment at `:954`), planned with `PlanStrategy::MinCover` and + executed by the ordinary join executor. `:932` builds one such rule + per id-typed column, `:994` provides a non-incremental variant, and + `:722`/`:703` choose between them and skip entirely when no unions + happened. Congruence inherits every improvement the query engine gets. +
+ +- [ ] You can explain why egglog's union-find gives up the textbook + bound. +
Answer + + It unions **by min id** rather than by rank (`union-find/src/lib.rs:6-12`), + which the crate admits "does not guarantee the same asymptotic + complexity". The reason is that the expensive consequence of a union + is not the union — it is the rebuild it triggers, which must rewrite + every row whose id stopped being canonical. Keeping the smaller id + canonical keeps long-lived ids stable and so perturbs fewer rows. The + union-find is tuned for its caller. egg declines a different textbook + optimisation (path compression on the `&self` path) for a + structurally similar reason. +
+ +## References + +- `egraphs-good/egglog` at the pinned commit (see the pin table at the + end of [resources/codebases.md](../../resources/codebases.md)). + The crates read here: `core-relations` (table, offsets, query, + free_join), `egglog-bridge`, `union-find`. +- Zhang et al., **"Better Together: Unifying Datalog and Equality + Saturation"**, PLDI 2023, arXiv:2304.04332 — §5.1 describes the + components this chapter reads, at the size they were in 2023. +- Wang, Willsey, Suciu, **"Free Join: Unifying Worst-Case Optimal and + Traditional Joins"**, SIGMOD 2023 — the `PureSize`/`MinCover` + strategies. Next chapter: [reading-free-join.md](reading-free-join.md). +- Mihalis Yannakakis, **"Algorithms for Acyclic Database Schemes"**, + VLDB 1981 — the semijoin program the decomposition phase is aiming at. +- Topic 21's [egg chapter](../21-formal/reading-egg-popl21.md) for the + hand-written `rebuild` this engine replaces with a rule. diff --git a/topics/44-egraphs-egglog/reading-free-join.md b/topics/44-egraphs-egglog/reading-free-join.md new file mode 100644 index 0000000..e760a10 --- /dev/null +++ b/topics/44-egraphs-egglog/reading-free-join.md @@ -0,0 +1,452 @@ +# Free Join: the plan space that contains both hash join and generic join + +The previous three chapters make a clean argument: e-matching is a +conjunctive query, generic join answers it with a worst-case optimal +bound, and egglog is built on that. This chapter is where the argument +gets complicated, and it is the reason egglog's *default* plan strategy +is not generic join. + +**"Free Join: Unifying Worst-Case Optimal and Traditional Joins"** — +Yisu Remy Wang, Max Willsey and Dan Suciu, SIGMOD 2023 +(arXiv:2301.10841) — starts from an uncomfortable observation. Ten +years after worst-case optimal joins were published, systems that adopt +them use them *only* for the cyclic part of a query and fall back to +binary joins for everything else, because binary joins have decades of +constant-factor engineering behind them. The paper's response is not to +pick a side. It shows the two algorithms are corners of one design +space, gives a plan language that covers all of it, and then does the +engineering — a data structure and a vectorized executor — that the +worst-case optimal side was missing. + +It is the most conventionally *database* paper in this topic, and it is +where the e-graph literature pays its debt back: the ideas were +developed for query processing, and this is the query-processing paper +that came out of the e-graph group. + +## The problem in one sentence + +Generic join has the better asymptotic bound and binary hash join has +the better constant, and treating them as rival algorithms means every +system that wants both has to implement both and a rule for choosing — +whereas they are the same nested loop with two different settings of +"how many relations and how many attributes does one join step touch". + +## The concepts, step by step + +### Step 1 — why the dichotomy survived + +> **In:** the AGM bound and generic join from +> [reading-relational-ematching.md](reading-relational-ematching.md) +> Steps 8–9. **Out:** the reason a provably better algorithm did not +> displace the one it beats. + +The folklore the paper opens with (§1): *"WCOJ is designed for cyclic +queries"*. It has real support. On a cyclic query, generic join beats +any binary plan asymptotically. On an **acyclic** query — one whose +hypergraph admits a join tree — Yannakakis' algorithm is already +asymptotically optimal, so there is nothing left to win, and binary +joins arrive with "column-oriented layout, vectorization, and query +optimization … compounding constant-factor speedups". + +So systems went hybrid: Umbra, EmptyHeaded, Graphflow all use WCOJ for +the cyclic subparts and binary joins elsewhere. The paper's complaint +about that is an engineering one, not a theoretical one: "Having two +different algorithms in the same system requires changing and +potentially duplicating existing infrastructure like the query +optimizer. This introduces complexity, and hinders the adoption of +WCOJ." + +Two planners, two executors, and a rule for switching. Anyone who has +maintained a query engine knows what that costs. + +### Step 2 — the two algorithms are the same loop + +> **In:** Step 1's dichotomy. **Out:** the structural identity the whole +> paper is built on, stated in one sentence per algorithm. + +§1, and it is worth memorising: + +- **Binary join** "processes two relations at a time, and joins on all + attributes in the join condition between these two relations." +- **Generic join** "processes one attribute at a time, and joins all + relations that share that attribute." + +Both are nested loops. A binary hash join iterates the tuples of one +relation and probes the hash table of another; a generic join level +iterates the keys of one trie and probes the others. The difference is +only in *what a single step is quantified over*: + +``` + relations per step attributes per step + binary hash join 2 all shared ones + generic join all sharing the attribute 1 + Free Join any number any number +``` + +Which immediately suggests filling in the rest of the table. Figure 1 +of the paper draws that design space and points out that the classic +multiway algorithms already live in it — Hash Teams, Generalized Hash +Teams, Eddies are all points between the two corners. + +### Step 3 — one data structure for both: the GHT + +> **In:** Step 2's design space. **Out:** the structure a plan in that +> space indexes over, and the two special cases it collapses to. + +Before unifying the algorithms you must unify what they read. Binary +join reads a **hash table**; generic join reads a **trie**. + +> **Definition 3.1 (Generalized Hash Trie).** "A GHT is a tree where +> each leaf is a vector of tuples, and each internal node is a hash map +> whose keys are tuples, and each key maps to a child node." + +The **schema** of a GHT is the list `[y₀, y₁ … y_ℓ]` of the attribute +names keyed at each level. Now read off the two corners (§3.1): + +- The trie used by generic join is a GHT **where each key is a tuple of + size one**, and the last level stores empty vectors. +- The hash table used by binary join is a GHT with **only two levels**: + level 0 the keys, level 1 vectors of tuples. + +One structure, two configurations, and everything in between is legal. +Note how far this is from the previous chapters' `Trie`: our +`relational.rs::Trie` is the size-one-key case, hard-coded, because that +is all generic join needs. + +### Step 4 — subatoms, and what a Free Join plan is + +> **In:** the GHT of Step 3. **Out:** the plan language, its validity +> condition, and the word egglog's source uses — *cover*. + +Three definitions (§3.2), each small: + +- A **subatom** of an atom `R(x)` is `R(y)` for some subsequence `y` of + `x` — the atom restricted to some of its columns. +- The subatoms of `R` used across a plan must form a **partitioning** of + `R(x)`: every column appears in exactly one of them. +- A **Free Join plan** for a query is a list of *nodes* + `[φ₁ … φ_m]`, each node a list of subatoms. + +Each node is one loop level. Write `vs(φ_k)` for the variables of node +k, and `avs(φ_k) = ⋃_{j **In:** Step 4's plan language. **Out:** how the system gets a good +> plan without a new optimizer, which is the practical crux. + +The paper does not build a new query optimizer. It takes an *existing* +binary join plan — from a real optimizer, with its cardinality +estimates and decades of tuning — and converts it into a Free Join plan +that "runs as fast or faster" (§1, §4.1). A left-deep binary plan maps +directly onto a list of two-subatom nodes. + +Then it **factors**: split a node whose cover carries several new +variables into two nodes, so that the more selective intersection +happens first and the remaining attributes are expanded later. Factoring +is the move that turns the binary-join-like plan of Step 4 into the +generic-join-like one, and it is applied only where the estimates say it +pays. + +This is why egglog's default strategy is `MinCover` rather than `Gj` +(`core-relations/src/free_join/plan.rs:35-41`), and why the source +comment can say a Free Join plan "degenerates to a hash join" at one end +and "~ recovers generic join" at the other. Read that comment again +after this step; it is a two-line summary of this paper. + +### Step 6 — COLT: pay for the index only where you probe + +> **In:** the GHT of Step 3 and the plans of Steps 4–5. **Out:** the +> data structure, and the specific waste it removes from generic join. + +Generic join's cost is not only the loops. Before it runs, the tries +have to be built — a cost this topic's own bench prints in its +`index µs` column, and which POPL'22 Table 1 splits its rows on. + +**COLT** — Column-Oriented Lazy Trie (§4.2) — attacks it from two sides. + +*Lazy*: a trie level is built only when something actually looks it up. +A COLT starts as a single leaf holding the offsets of every tuple in the +base table; on the first `get` at a level, that level is materialised. +If a subtrie is never probed, it is never built. The paper's improvement +over the earlier lazy trie of Umbra is that COLT "completely eliminates +the cost" of building at least one level per table — with the neat +special case that if a relation is only ever *iterated* (it is a cover +and nothing gets it), no auxiliary structure is built for it at all. + +*Column-oriented*: the leaves are vectors of **offsets into the base +table** rather than copies of the tuples, so the trie stores integers +and the payload columns stay where they were. Topic 12's readers will +recognise the pattern and the reason: you touch only the columns the +join actually uses. + +Set this against the honest number in our own lane 1: at N = 1600 the +tries cost 322.4 µs and the join itself 145.0 µs — **the index build is +69% of generic join's total time**, and it is charged in full on every +call because our matcher rebuilds it every time. COLT is the answer to +that column, and exercise 4 of this topic is a small version of it. + +### Step 7 — vectorized execution + +> **In:** the Free Join execution of Step 4. **Out:** the second +> constant-factor recovery, and where you have met it before. + +Generic join as published is tuple-at-a-time recursion. Free Join +batches: at each node, collect a batch of bindings and probe the other +subatoms for the whole batch, "so these probes issue the same set of +relations for each tuple". This is exactly topic 11's tuple-at-a-time +versus batch-at-a-time result, arriving in a join algorithm for the same +reasons — fewer indirect branches, better cache and TLB behaviour, and +memory-level parallelism from independent probes in flight. + +You can see the shape in egglog's executor, which accumulates into +`FrameUpdates` and drains in chunks (`free_join/execute.rs:1453`). + +### Step 8 — the numbers, including the ones that are below 1 + +> **In:** Steps 5–7. **Out:** what the combination actually bought, on +> real benchmarks, with the losses stated. + +Setup (§5): implemented in Rust, evaluated on the **Join Order +Benchmark** (JOB — real IMDb data, the benchmark topic 22 and topic 10 +both use) and **LSQB**, against the in-memory column store DuckDB as the +binary-join baseline, its own Generic Join implementation, and Kùzu. + +``` + Free Join vs. geometric mean maximum minimum + binary join (DuckDB) 2.94x 19.36x 0.85x (a 17% slowdown) + Generic Join 9.61x 31.6x 2.63x +``` + +Two things to take from that table. First, the geometric means are the +honest summary and they are much smaller than the maxima — 2.94× is a +good result, not a revolution. Second, **the minimum against binary join +is below one**: on some queries Free Join loses, and §5 says why — +those plans are bushy and materialise a large intermediate, and "we have +not spent much effort optimizing for materialization". + +The instructive single query is JOB's **Q13a** (§5.2). DuckDB takes over +10 seconds, Generic Join 7 seconds, Free Join just over 1. The plan +explains it: the first three binary joins are over four very large +tables, two of them many-to-many, "exploding the intermediate result to +contain over 100 million tuples" — and all three joins are on the *same +attribute*, which makes it the clover query of Step 4. Generic Join and +Free Join intersect on that attribute and "expand the remaining +attributes only after other more selective joins". + +The paper draws the right conclusion rather than the flattering one: the +binary plan *could* have been fast had the optimizer ordered the +selective joins first. What the WCOJ-style plan bought here was +**robustness to a bad plan**, not raw speed — a claim §5.4 then tests +directly. And §5.2 notes elsewhere that performance "is not solely +determined by the cyclicity of the query; the presence of skew in the +data is another important factor", which is the folklore of Step 1 +finally being stated properly. + +### Step 9 — what this means back in the e-graph + +> **In:** everything above, plus +> [reading-egglog-source.md](reading-egglog-source.md) Step 6. +> **Out:** why the engine that started this topic ships with generic +> join as the *option* rather than the default. + +egglog's planner offers `PlanStrategy::Gj` and the Free Join strategies +`PureSize`/`MinCover`, and the rebuild rules explicitly ask for +`MinCover` (`egglog-bridge/src/lib.rs:956`). The source comment's +footnote is the trade stated plainly: Free Join "is not worst-case +optimal because it does not necessarily pick the smallest side to scan". + +So the arc of this topic ends where a database course should want it to. +POPL'22: your matcher is a query, here is the optimal algorithm. +PLDI'23: then make the database primary and get incrementality free. +SIGMOD'23: and then, having won the asymptotics, spend the next paper +winning back the constants — with lazy indexes, column layout and +vectorized execution, the same three things every analytical engine in +topics 11 and 12 is made of. + +## How to read the paper (with the concepts in hand) + +1. **§1** whole. It is the clearest statement of the dichotomy anywhere, + and Figure 1 is the paper's thesis in one picture. +2. **§2** if you want generic join re-derived; skip if the POPL'22 + chapter's Step 9 is fresh. +3. **§3.1** for the GHT (Step 3) and **§3.2** for the plan language + (Step 4). Do the exercise of writing both plans for `Q♣` yourself + before reading Example 3.6. +4. **§4.1** (conversion and factoring), then **§4.2** (COLT) — Figures + 11 and 12 together are the data structure. +5. **§5** with Step 8's table beside you; read §5.2's Q13a discussion + and §5.4's robustness experiments, which are the paper's most useful + pages for a practitioner. +6. **§6**, limitations, is short and worth it. + +## Where each step lives in the code + +Nothing in this topic's crate implements Free Join — that is exercise 6. +The production reference is egglog: + +| step | file:line | +|---|---| +| 4, plan language | `core-relations/src/free_join/plan.rs:134-158` `JoinStage`, `:145` `FusedIntersect` (a cover plus the subatoms it probes) | +| 5, strategies | `plan.rs:32-41`; `PlanStrategy::MinCover` chosen at `egglog-bridge/src/lib.rs:956` | +| 5, fusion | `plan.rs:159-163` `fuse_single_scans` — merging single-scan stages onto one cover atom (the module doc at `:43` calls it `JoinStage::fuse`; the function on disk has the longer name) | +| 6, lazy index | `free_join/execute.rs:1431` (small subsets are refined, not indexed), `:1439` `get_cached_trie_node` | +| 7, vectorization | `free_join/execute.rs:1428` `FrameUpdates`, `:1453` chunked drain | +| this topic's toy | `relational.rs:78` `index_atom` builds every level eagerly — the thing COLT does not do | + +## Questions (answer in notes.md) + +1. Write both Free Join plans of Step 4 for lane 3's triangle + multi-pattern, and give the cover of every node. Which is generic + join, which is a binary plan, and what is the intermediate size of + each on the V = 1600, E = 8000 graph? +2. Our `index µs` at N = 1600 is 69% of generic join's total. Which + levels of the two tries does lane 1a's plan actually probe, and how + much of that build would COLT's laziness skip? Estimate before + measuring, then measure (exercise 4). +3. The minimum speedup against binary join is 0.85×. Construct the + shape of a query where you would *expect* Free Join to lose, using + §5's explanation, and say what you would change in the executor to + fix it. +4. §5.2 claims WCOJ-style plans are more robust to bad plans. State + that claim as a measurable property (not "more robust"), and design + the experiment for lane 3. +5. A GHT with two levels is a hash table; with size-one keys it is a + trie. What is a GHT with size-two keys, and which classic algorithm + from Figure 1's design space does a plan over it correspond to? +6. egglog picks `MinCover` for its rebuild rules. Given what the rebuild + rule's query looks like (two atoms, one of them the union-find + table), argue whether worst-case optimality could ever matter there. + +## Done when + +Answer each before unfolding it. + +- [ ] You can state the difference between binary join and generic join + in one sentence each, without mentioning cyclicity. +
Answer + + Binary join processes **two relations at a time and joins on all the + attributes shared between them**; generic join processes **one + attribute at a time and joins all the relations that share it** + (§1). They are the same nested loop with different quantifiers, which + is why a design space parameterised by (relations per step, + attributes per step) contains both — and contains Hash Teams and + Eddies in between. +
+ +- [ ] You can say what a GHT is and give its two degenerate cases. +
Answer + + A tree whose leaves are vectors of tuples and whose internal nodes are + hash maps from *tuples* to child nodes (Definition 3.1); its schema + names the attributes keyed at each level. Generic join's trie is the + case where every key is a one-tuple and the last level holds empty + vectors; binary join's hash table is the two-level case, keys at level + 0 and tuple vectors at level 1. +
+ +- [ ] You can define a valid Free Join plan and identify a node's cover. +
Answer + + A plan is a list of nodes, each a list of subatoms (an atom restricted + to a subsequence of its columns), such that each atom's subatoms + partition it. With `vs(φ_k)` the node's variables and + `avs(φ_k) = ⋃_{j + +- [ ] You can explain what COLT is lazy about and why it matters to this + topic's own numbers. +
Answer + + A COLT starts as one leaf of offsets into the base table and + materialises a trie level only on the first `get` at that level, so + subtries that are never probed are never built — and a relation that + is only ever iterated (always a cover, never probed) gets no auxiliary + structure at all. Leaves hold offsets, not copied tuples, so the + payload columns stay in the base table. It matters here because lane + 1a spends 322.4 µs building tries against 145.0 µs joining — 69% of + the cost is index construction that is thrown away after one query. +
+ +- [ ] You can quote the evaluation without overstating it. +
Answer + + Geometric means on JOB and LSQB: **2.94×** faster than binary join + (DuckDB) and **9.61×** faster than its own Generic Join. Maxima + 19.36× and 31.6×; minima **0.85×** — a 17% slowdown against binary + join on some queries — and 2.63×. The losing queries have bushy plans + that materialise large intermediates, which the authors say they did + not optimise. Q13a is the showcase: >10 s (DuckDB), 7 s (Generic + Join), just over 1 s (Free Join), because the binary plan built an + intermediate of over 100 million tuples across three joins on the same + attribute. +
+ +- [ ] You can say why egglog's default is not generic join. +
Answer + + Because worst-case optimality is a bound on the worst case, and the + average case is decided by constants: index building, memory layout, + batching. Free Join's `MinCover` strategy reaches a plan close to a + binary plan where that is better and close to generic join where + *that* is better, at the cost of the guarantee — egglog's own comment + says it "is not worst-case optimal because it does not necessarily + pick the smallest side to scan" (`plan.rs:41`). `PlanStrategy::Gj` + remains available for when the guarantee is what you want. +
+ +## References + +- Yisu Remy Wang, Max Willsey, Dan Suciu, **"Free Join: Unifying + Worst-Case Optimal and Traditional Joins"**, SIGMOD 2023, + arXiv:2301.10841. §1 + Figure 1 (the design space), §3.1 (GHT, + Definition 3.1), §3.2 (subatom, partitioning, plan, validity, cover — + Definitions 3.4–3.8), §4.1 (conversion and factoring), §4.2 (COLT, + Figures 11–12), §4.3 (vectorized execution, Figure 13), §5 + (evaluation, JOB and LSQB), §5.4 (robustness to bad plans), §6 + (limitations). +- Hung Q. Ngo et al., **"Worst-case Optimal Join Algorithms"** — the + generic join this paper takes as the WCOJ representative. +- Mihalis Yannakakis, **"Algorithms for Acyclic Database Schemes"**, + VLDB 1981 — why acyclic queries were already solved, which is half of + Step 1. +- Viktor Leis et al., **"How Good Are Query Optimizers, Really?"**, + VLDB 2015 — the Join Order Benchmark used here, read in + [topic 10](../10-query-planning/reading-how-good-optimizers.md). +- Previous chapter: + [reading-egglog-source.md](reading-egglog-source.md), whose + `PlanStrategy` enum is this paper. diff --git a/topics/44-egraphs-egglog/reading-relational-ematching.md b/topics/44-egraphs-egglog/reading-relational-ematching.md new file mode 100644 index 0000000..9e3d328 --- /dev/null +++ b/topics/44-egraphs-egglog/reading-relational-ematching.md @@ -0,0 +1,728 @@ +# Relational e-matching: the pattern is a query, the e-graph is the database + +Topic 21's guide to egg ends on a number: e-matching, not congruence +closure, is where equality saturation spends its time. This paper — +Zhang, Wang, Willsey and Tatlock, **"Relational E-matching"**, POPL 2022 +(arXiv:2108.02290) — is the one that reads that sentence as a database +problem and answers it with an algorithm from our literature. Its whole +argument fits in one substitution: an e-graph is a set of tables, a +pattern is a conjunctive query, and *the equality constraint that +backtracking checks last is a join key*. + +This chapter builds every term it needs — e-matching, substitution, +linear pattern, conjunctive query, atom, fractional edge cover, the AGM +bound, generic join — from nothing, then applies the paper's two +theorems to the numbers this topic's own bench prints. + +Every paper claim below names the section, figure, table or theorem it +came from. Code anchors are this topic's crate +(`topics/44-egraphs-egglog/experiments/src/…`) and `egraphs-good/egg` at +the commit `resources/codebases.md` pins. + +## The problem in one sentence + +Matching the pattern `f(a, g(a))` against an e-graph that holds N `f` +e-nodes and N `g` e-nodes takes a backtracking matcher N² + N + 1 steps +to produce N answers, because it can only check that the two `a`s agree +*after* it has built each candidate — and a join algorithm checks that +first, for the same reason a database never computes a cross product +and filters it. + +## The concepts, step by step + +### Step 1 — e-matching, stated precisely + +> **In:** an e-graph, as topic 21's guide built it. **Out:** the exact +> statement of what e-matching returns, and the two words the rest of +> this chapter leans on — *substitution* and *root*. + +A quick restatement of the structure, because the definitions have to be +exact for the counting to mean anything (paper Definitions 4 and 5): + +- An **e-node** is a pair `(f, [i₁…i_k])`: a function symbol and a list + of e-class ids. `f(i₁…i_k)` is shorthand for it. +- An **e-class** is a set of e-nodes, identified by one or more ids. All + the e-nodes in one e-class are asserted to be equal. +- A **union-find** stores which ids are equal; `find(i)` returns the + class's **canonical** id — the single id that stands for it. +- A **term** is what you write on paper: `f(3, g(3))`. An e-class + **represents** a term if some e-node in it does, recursively + (Definition 6). + +A **pattern** is a term with **pattern variables** in it — `f(a, g(a))`, +where `a` may stand for any e-class. A pattern with no variable +occurring twice is called **linear**; `f(a, g(b))` is linear and +`f(a, g(a))` is not. That distinction will turn out to be the entire +performance story. + +An **e-matching substitution** σ maps every variable in the pattern to +an e-class (Definition 7). E-matching (Definition 8) returns the set of +pairs `(σ, r)` such that every term in `σ(p)` is represented in e-class +`r`; `r` is called the **root** of the match. So a match is *not* a +term — it is an assignment of e-classes to variables, plus the class +the matched terms live in. That is what makes the output small even +when the term set is enormous. + +### Step 2 — the e-graph that makes it hard + +> **In:** the definitions of Step 1. **Out:** the concrete e-graph both +> the paper and this topic's bench measure on, with its two sizes — how +> big it is, and how many terms it stands for. + +Paper Figure 2. Fix N. The e-graph has: + +``` + e-class 1 … N one constant e-node each: 1, 2, … N + e-class i_g N e-nodes: g(1), g(2), … g(N) + e-class i_f N e-nodes: f(1,i_g), f(2,i_g), … f(N,i_g) +``` + +That is **3N e-nodes** in **N + 2 e-classes**. Now count the terms it +represents. Every `f` e-node's second child is `i_g`, and `i_g` +represents N different terms, so each of the N `f` e-nodes stands for N +terms: + +``` + constants N + g-terms N g(1) … g(N) + f-terms N × N f(i, g(j)) for every i, j + ──────────────────────── + total N² + 2N +``` + +At N = 1600 that is 4,800 e-nodes representing 2,563,200 terms. **This +is the property that makes e-graphs worth having and e-matching hard: +the structure is linear, the thing it denotes is quadratic.** Any +algorithm that enumerates terms has already lost; the question is +whether an algorithm that walks the structure can avoid enumerating them +implicitly. + +`gen.rs::Fig2` builds exactly this graph, and lane 1's `e-nodes` column +is 3N in every row — the check that it did. + +### Step 3 — two kinds of constraint, and the one backtracking defers + +> **In:** the Figure 2 e-graph of Step 2 and the pattern `f(a, g(a))`. +> **Out:** the paper's classification of what a pattern demands, which +> is the diagnosis the whole paper rests on (§2.1). + +Matching `f(a, g(a))` demands three things of a candidate term `t` +(paper §2.1 lists them in this order): + +1. `t`'s symbol is `f`; +2. `t`'s second child's symbol is `g`; +3. `t`'s first child is equivalent to the child of `t`'s second child. + +The paper splits these into two kinds: + +- **Structural constraints** come from the *shape* of the pattern — + which symbol sits where. Constraints 1 and 2. +- **Equality constraints** come from a variable occurring more than + once: the positions it occupies must be the same e-class. Constraint + 3. A pattern with none of these is **linear**. + +Now the diagnosis, in the paper's words (§2.1): "Backtracking search +exploits the structural constraints first and defers checking the +equality constraints to the end." A top-down walk cannot do otherwise. +It reaches the `f` e-node, takes the first child as a candidate binding +for `a`, then must walk into the second child's e-class to find a `g` +before it has anything to compare against. By then the candidate exists. + +``` + pattern f(a, g(a)) what the walk must do + ────────────────── ───────────────────── + f pick an f e-node ← structural, usable now + / \ bind a := its 1st child ← nothing to check yet + a g find a g e-node ← structural, usable now + | compare its child to a ← equality, only now + a +``` + +### Step 4 — count the walk, on paper and on the machine + +> **In:** the diagnosis of Step 3, the e-graph of Step 2. **Out:** a +> closed form for the work backtracking does, checked against this +> topic's measured `bt visits` column. + +Paper §2.1 gives the visiting order: + +``` + f(1, g(1)) → … → f(1, g(N)) + ↩→ f(2, g(1)) → … → f(2, g(N)) + ↩→ f(N, g(1)) → … → f(N, g(N)) +``` + +and concludes: "Despite there being only N matches, backtracking search +runs in time O(N²)." + +Our implementation is egg's four-instruction VM rather than the +declarative algorithm, so the constant is visible. `backtrack.rs` +compiles `f(a, g(a))` to `Scan(f)`, `Bind f`, `Bind g`, `Compare`, and +this is the `Bind` case, where the cost lives: + +```rust +// backtrack.rs, lines 151-173 — Bind steps over every e-node of the right +// symbol; Compare cannot run until both registers are filled. The line to +// watch is 158, the loop, and 170, the check that comes too late. + 151 Ins::Bind { + 152 class, + 153 op, + 154 out: base, + 155 arity, + 156 } => { + 157 let c = regs[*class]; + 158 for n in g.nodes(c) { + 159 if n.op != *op || n.children.len() != *arity { + 160 continue; + 161 } + 162 visits.set(visits.get() + 1); + 163 for (i, &ch) in n.children.iter().enumerate() { + 164 regs[base + i] = ch; + 165 } + 166 exec(g, rest, roots, regs, visits, out); + 167 } + 168 } + 169 Ins::Compare { a, b } => { + 170 if g.find(regs[*a]) == g.find(regs[*b]) { + 171 exec(g, rest, roots, regs, visits, out); + 172 } + 173 } +``` + +Count it. `Scan` visits the one e-class containing an `f` e-node — the +op index (`egraph.rs::classes_with_op`, egg's `classes_by_op`) means it +is 1 and not N + 2. The outer `Bind f` steps over N e-nodes. For each, +the inner `Bind g` steps over N. So: + +``` + visits = 1 + N + N × N = N² + N + 1 +``` + +N = 100 → 1 + 100 + 10,000 = **10,101**, which is exactly what lane 1 +prints. N = 1600 → 2,561,601, also exact. The formula is not an +estimate; it is the number, and being able to predict a counter to the +unit is how you know the harness is measuring the algorithm rather than +the allocator. + +### Step 5 — conjunctive queries, in the vocabulary a pattern needs + +> **In:** nothing from the previous steps — this is the database half of +> the vocabulary, defined from scratch. **Out:** the five words Step 7 +> will use to restate a pattern: relation, atom, body, head, join +> variable. + +A **relation** `R` of arity k is a set of tuples of k values. A +**database** is a set of relations. + +A **conjunctive query** (paper §2.2) is a query built only from select, +project and join — no union, no difference, no aggregation. It is +written: + +``` + Q(x₁ … x_k) ← R₁(x₁,₁ … x₁,ₖ₁), … , Rₙ(xₙ,₁ … xₙ,ₖₙ) +``` + +- Each `Rᵢ(…)` is an **atom**: a relation name with a variable in each + column position. +- Everything right of the arrow is the **body**; `Q(…)` is the **head**. +- A variable in the head is **free** — it comes back in the answer. A + variable only in the body is **bound**: existentially quantified, + projected away. +- A variable appearing in two atoms is what a database person calls a + **join variable**, and answering the query means finding assignments + that make every atom simultaneously present in the database. + +There is no separate notion of "shape constraint" and "equality +constraint" here. Every constraint is the same kind of thing: a variable +that two atoms have to agree on. That is the whole trick, and Step 7 is +where the pattern acquires this form. + +### Step 6 — the e-graph as a database, and the dependency hiding in it + +> **In:** the e-graph of Step 2 and the relational vocabulary of Step 5. +> **Out:** the database the rest of the chapter queries, plus the reason +> nested patterns do not need an extra join. + +Paper §3.1. For every function symbol `f` of arity k, make a relation +`R_f` of arity k+1: the first column is the e-class id **containing** +the e-node, the remaining k are its children. Every id is canonicalised +through `find` first. + +``` + I = { R_f ← (find(i), find(j₁) … find(j_k)) | M[i] = f(j₁ … j_k) } +``` + +Figure 2 becomes (paper Figure 7): + +``` + R_f: | id | arg1 | arg2 | R_g: | id | arg1 | + | i_f | 1 | i_g | | i_g | 1 | + | i_f | 2 | i_g | | i_g | 2 | + | … | … | … | | … | … | + | i_f | N | i_g | | i_g | N | +``` + +`relational.rs::to_database` (line 29) is that formula, one loop long. +Two properties of the translation matter later: + +- **It is linear.** One tuple per e-node, so building the database costs + O(|E|) — "subsumed by the time complexity of most non-trivial + e-matching patterns" (§3.1). The paper is explicit that this is + affordable *because* e-matching happens in big batches between + rebuilds; §6.4 lists the frequently-updated case as future work, and + egglog is what that future work turned into. +- **Every id in it is canonical.** This is why compilation can join + nested patterns directly on the auxiliary variable instead of adding a + join against the equivalence relation (§3.2): for canonical ids, + `i ≡ j` is just `i = j`. + +And one that the paper flags for optimisation (§4.3): an e-graph never +contains two e-nodes with the same symbol and children, so in `R_f` the +children columns **functionally determine** the id column — a +functional dependency, in exactly the sense a schema means it. A query +planner that knows it can skip work; §4.3 is about doing so. + +### Step 7 — unnesting: from pattern to conjunctive query + +> **In:** the pattern of Step 3, the vocabulary of Step 5, the database +> of Step 6. **Out:** the query the join algorithm will answer, with the +> equality constraint now indistinguishable from the structural one. + +Paper Figure 8 defines two functions. `Aux` returns a variable standing +for a subpattern, plus the atoms that constrain it: + +``` + Aux(f(p₁ … p_k)) = v ~ R_f(v, v₁ … v_k), A₁ … A_k where Aux(pᵢ) = vᵢ ~ Aᵢ, + and v is FRESH + Aux(x) = x ~ ∅ for a pattern variable x + + Compile(p) = Q(root, v₁ … v_k) ← atoms where Aux(p) = root ~ atoms +``` + +Run it on `f(a, g(a))`, innermost decisions first: + +1. `Aux(f(a, g(a)))` mints a fresh variable — call it `root` — and will + emit `R_f(root, ?, ?)`. +2. Its first argument is the variable `a`: `Aux(a) = a ~ ∅`. No atom. +3. Its second argument is `g(a)`: mint a fresh `x`, emit `R_g(x, a)`. +4. So the body is `R_f(root, a, x), R_g(x, a)`, and the head keeps the + root and the pattern's own variables. + +``` + Q(root, a) ← R_f(root, a, x), R_g(x, a) + │ │ │ │ + │ └────────────┼──┘ a: the EQUALITY constraint + └───────────────┘ x: the STRUCTURAL constraint +``` + +Both are now the same syntactic object — a variable in two atoms — +which is the sentence the paper is built on (§3): "the relational +perspective sees no difference between the two kinds of constraint." + +Our `pattern.rs::compile` is this, and its unit test asserts the exact +rendering (auxiliaries are printed `?0`, `?1`): + +```rust +// pattern.rs, lines 171-176 — the test that pins Figure 8's output + 171 let q = compile(&[papp(f, vec![pvar("a"), papp(gg, vec![pvar("a")])])]); + 172 assert_eq!(q.atoms.len(), 2, "one atom per non-variable subpattern"); + 173 let rendered = q.render(&|s| g.sym_name(s).to_string()); + 174 assert_eq!(rendered, "Q(?0, a) <- R_f(?0, a, ?1), R_g(?1, a)"); + 175 // `a` occurs in both atoms: the equality constraint became a join. + 176 assert_eq!(q.atoms_with(q.head[1]).len(), 2); +``` + +One consequence the paper draws in §1 and we exploit in lane 3: +**multi-patterns are free.** Matching several patterns that share +variables — which backtracking needs special machinery for (de Moura and +Bjørner 2007) — is just a body with more atoms. + +### Step 8 — the AGM bound, worked on the triangle + +> **In:** the query vocabulary of Step 5. **Out:** the number that +> bounds any conjunctive query's output, and therefore the target any +> join algorithm should hit. Nothing here is about e-graphs; Step 10 +> applies it to one. + +How big can a conjunctive query's answer be? Three answers of increasing +sharpness, on the **triangle query** (paper §2.3) with +`|R| = |S| = |T| = M`: + +``` + Q(x, y, z) ← R(x, y), S(y, z), T(z, x) +``` + +1. **Cartesian product**: `|R|·|S|·|T| = M³`. Ignores the query. +2. **Any two atoms**: the answer cannot exceed `|R|·|S| = M²`, since a + triangle is in particular an `R`-`S` pair sharing `y`. +3. **The AGM bound**: `M^1.5`, and it is *tight* — there exists a + database achieving it (Atserias, Grohe, Marx 2008). + +The third needs two definitions. The **query hypergraph** has a vertex +per variable and a hyperedge per atom; the triangle's is a triangle. A +**fractional edge cover** assigns a weight `w_i ∈ [0,1]` to each atom so +that, for every variable, the weights of the atoms containing it sum to +at least 1. The **AGM bound** is then + +``` + min over covers of Π_i |R_i|^{w_i} +``` + +Work it. In the triangle each variable is in exactly two atoms, so +`w = (½, ½, ½)` is a cover: for `x`, the atoms `R` and `T` contribute +½ + ½ = 1. ✓. The bound is + +``` + M^½ · M^½ · M^½ = M^{3/2} +``` + +At M = 10,000: the cross product says 10¹², two atoms say 10⁸, AGM says +10⁶. Six orders of magnitude between the naive bound and the true one — +and a binary-join plan that materialises `R ⋈ S` first *builds* the 10⁸ +before filtering it down. This is the gap worst-case optimal joins +exist to close. + +### Step 9 — generic join, traced on the Figure 2 database + +> **In:** the AGM bound of Step 8, the database of Step 6, the query of +> Step 7. **Out:** the algorithm, its two implementation requirements, +> and an exact probe count to compare against Step 4's N² + N + 1. + +**Generic join** (paper Algorithm 1, from Ngo et al. 2014) is +variable-at-a-time, not relation-at-a-time. Given an ordering of the +query's variables, it picks the next variable `x`, computes `D_x` as the +intersection of the values every atom containing `x` allows for it, and +recurses on each survivor with `x` replaced by that value. When no +variables remain, the accumulated assignment is an answer. + +Two requirements make the AGM bound hold (§2.3): + +- the intersection must run in `O(min_j |R_j.x|)` — iterate the + *smallest* participating set and probe the others, never the largest; +- a residual relation — `R(v, y)` for a fixed `v` — must be reachable in + constant time. A **trie** gives both (Figure 5): a tree whose every + node is a map from a value to a subtrie, with the columns ordered to + agree with the variable ordering, so fixing a variable is one lookup. + +Here is the inner loop, doing exactly that: + +```rust +// relational.rs, lines 199-227 — smallest-first intersection. Line 200 picks +// the lead by map size (the O(min) requirement); line 220 is the probe into +// every other participating atom. + 199 // Intersect smallest-first, which is what buys the O(min |R_j.x|) bound. + 200 let lead = *part[..n_part] + 201 .iter() + 202 .min_by_key(|&&i| cur[i].kids.len()) + 203 .expect("non-empty"); + 204 let lead_trie: &'a Trie = cur[lead]; + // ... 205-214: copy the participating cursors into fixed-size scratch ... + 215 for (&v, sub) in &lead_trie.kids { + 216 probes.set(probes.get() + 1); + 217 let mut ok = true; + 218 for k in 0..n_others { + 219 probes.set(probes.get() + 1); + 220 match others[k].1.kids.get(&v) { + 221 Some(child) => next[k] = (others[k].0, child), + 222 None => { + 223 ok = false; + 224 break; + 225 } + 226 } + 227 } +``` + +Now trace it on `Q(root, a) ← R_f(root, a, x), R_g(x, a)` with the +ordering `[a, x, root]` (which is what `relational.rs::plan` picks: +`a` and `x` are each in two atoms, ties broken by relation size then +variable id): + +``` + level a: D_a = R_f.arg1 ∩ R_g.arg1 = {1 … N} + cost: N keys in the lead trie + N probes into the other = 2N + level x: for each a = i: R_f(_, i, x).x = {i_g} ∩ R_g(x, i).x = {i_g} + cost: 1 key + 1 probe, N times = 2N + level root: for each (i, i_g): R_f(root, i, i_g).root = {i_f} + only one atom participates — no intersection = N + ───────────────────────────────────────────────────────────────────────── + total probes = 5N +``` + +N = 100 → **500**, N = 1600 → **8,000**: precisely lane 1's `gj probes` +column. Compare Step 4: 10,101 and 2,561,601. Same answers, same +machine, same accounting. + +Notice what happened at the very first level. Intersecting `R_f.arg1` +with `R_g.arg1` *is* enforcing the equality constraint, before a single +candidate has been constructed. The paper's Figure 6 draws exactly this +contrast — backtracking with N² boxes and ✓/✗ marks, a hash join with N. + +### Step 10 — the two theorems, applied to this topic's own lanes + +> **In:** Step 8's AGM bound and Step 9's algorithm. **Out:** the paper's +> complexity results, and a check that they predict both of lane 1's +> tables — including the one where generic join loses. + +First, the objection that has to be cleared. E-matching is NP-complete +(Kozen 1977), so how can anything be optimal? Because the hardness is in +the wrong parameter. Databases distinguish **query complexity** — in the +size of the query — from **data complexity** — in the size of the +database, with the query held fixed (§1). Kozen's result is about the +pattern's size. Patterns are three or four nodes; e-graphs are millions. +Hold the pattern fixed and the problem is polynomial in the e-graph. + +**Theorem 9** (§3.4): relational e-matching is worst-case optimal — fix +a pattern `p`, and it runs in `O(max_E |M(p, E)|)`, the largest output +any e-graph of that size could produce. + +**Theorem 10** is the one with teeth, because it is stated in the +*actual* output size rather than the worst case. For a pattern that +compiles to `Q(X) ← R₁(X₁) … R_m(X_m)`: + +``` + time = O( √( |Q(I)| × Π_i |R_i| ) ) ≤ O( √( |Q(I)| × N^m ) ) +``` + +The proof is worth reading (§3.4) because it is short and it explains +the shape: add an atom `C` covering the variables that appear in only +one atom; then *every* variable is in at least two atoms, so `w = ½` +everywhere is a cover, and the AGM bound of the padded query is the +square root above. + +Now apply it to lane 1, where `m = 2` and `|R_f| = |R_g| = N`: + +``` + lane 1a, f(a, g(a)): |Q(I)| = N bound = √(N · N²) = N^1.5 + N = 1600 → 1600^1.5 = 64,000 + measured probes: 8,000 ✓ under the bound + + lane 1b, f(a, g(b)): |Q(I)| = N² bound = √(N² · N²) = N² + N = 1600 → 2,560,000 + measured probes: 2,561,603 ✓ AT the bound +``` + +The theorem predicts both rows, including the disappointing one. When +the output is quadratic, an optimal algorithm still does quadratic work +— optimality is a promise about waste, not about speed. `f(a, g(b))` is +linear, has no equality constraint, and every candidate is an answer, so +there is no waste to eliminate and generic join's more expensive +instruction (a hash lookup, ~18 ns, against a pointer walk, ~4 ns) makes +it **1.8× slower** in wall clock. That is the correct result and the +paper reports its own version of it (Step 11). + +### Step 11 — what the evaluation actually claims + +> **In:** the algorithm and its bounds. **Out:** an honest reading of +> §5, including the column most summaries drop. + +The setup (§5.1): relational e-matching implemented *inside* egg — about +80 lines to compile patterns to conjunctive queries, plus a separate +generic-join library "in fewer than 500 lines", against egg's existing +matcher of "about 500 lines … interconnected to various other parts of +egg". Two suites, `math` and `lambda`; e-graphs grown by saturation and +stopped at four sizes; each approach run 10 times, minimum taken; single +threaded, 4.6 GHz, 32 GB. + +The headline is real: "GJ can be over 6 orders of magnitude faster" +(§5.2). Table 1's `math` suite at 217,396 e-nodes, with index building +excluded, reports a best ratio of **8,575,830.58** and a median of +**80.84**. + +The column to keep is **Worst**, in the same row: **0.76**. And in the +smallest `math` configuration with index building charged, 0.03 — a +pattern on which relational e-matching was 33× *slower*. §5.2 explains +it in one sentence: "Speedup tends to be greater when the output size is +smaller. A large output indicates the e-graph is densely populated with +terms matching the given pattern, therefore backtracking search wastes +little time on unmatched terms." + +Two more honest details, both of which shaped what came next: + +- The `+`/`−` rows are with and without **index building time**. Tries + must be built before generic join can run, and §5.2 says the cost + "sometimes offset[s] the gains". Amortising that is exercise 4 here — + and it is the reason egglog stopped keeping a separate e-graph to copy + from at all. +- The **Total** column (cumulative speedup over all patterns) does not + grow with e-graph size, even while the best and median ratios do, + because total time is dominated by simple linear patterns like + `(+ (+ a b) c)` that return enormous result sets — the case where + there is nothing to win. + +## How to read the paper (with the concepts in hand) + +Straight through; it is 22 pages and the middle is the good part. + +1. **§1**, for the framing and the 60–90% number. +2. **§2.1** with our Step 3 open — the constraint taxonomy is the + diagnosis, and everything after is treatment. +3. **§2.2–2.3** can be skimmed if Step 5 and Step 8 landed; do read the + generic join walkthrough (Algorithm 2), which is our Step 9 written + as nested loops. +4. **§3.1–3.2** are short and are the translation; §3.3 shows the + generated program for our exact query. +5. **§3.4** — read the proof of Theorem 10. It is the only place the + `√` shape is explained. +6. **§4** is the practical section: variable ordering (§4.1), functional + dependencies (§4.3). Read §4.3 next to Step 6's dependency remark. +7. **§5** with Step 11 open, and look at Figure 9's log-scale spread + rather than the headline. +8. **§6.4** is one paragraph and it is the seed of egglog: what to do + when the e-graph changes constantly instead of in batches. + +## Where each step lives in the code + +| step | this crate | egg (pinned) | +|---|---|---| +| 1–2, the structure | `egraph.rs`, `gen.rs::Fig2` | `egraph.rs:970` add, `:1147` union, `:1416` rebuild | +| 3–4, the walk | `backtrack.rs:29` `Ins`, `:151` Bind, `:169` Compare | `machine.rs:24-29`, `:66-74` Scan | +| the op index | `egraph.rs::classes_with_op` | `egraph.rs:81` `classes_by_op`, `pattern.rs:300-304` | +| 6, e-graph → tables | `relational.rs:29` `to_database` | — | +| 7, Figure 8 | `pattern.rs::compile`, test at `:171` | — | +| 9, tries + generic join | `relational.rs:78` `index_atom`, `:116` `plan`, `:170` `gj` | — | +| 10, the two lanes | `bin/ematch_bench.rs::lane1` | — | + +## Questions (answer in notes.md) + +1. Lane 1a's `bt visits` is `N² + N + 1` and `gj probes` is `5N`, yet + the measured speedup at N = 1600 is 21.7×, not 320×. Account for the + difference in nanoseconds per unit, using the `index µs` column, and + say which of the two constants you could actually reduce. +2. Theorem 10 gives `√(|Q(I)| × Π|Rᵢ|)`. Compute it for the triangle + multi-pattern of lane 3 at V = 1600, E = 8000 (three atoms, all + `R_e`), and compare with the measured 79,416 probes. Is the bound + loose here, and why? +3. `relational.rs::plan` orders variables most-constrained-first. Any + ordering is worst-case optimal — so construct a pattern and an + e-graph where the reverse ordering does dramatically more probes, and + explain what the good ordering knew. +4. §4.3 says the children columns functionally determine the id column. + Name one step of the trace in Step 9 that this makes redundant, and + estimate what fraction of that lane's probes it would remove. +5. The paper builds the database from scratch on every match (§3.1) and + calls the cost "subsumed". At what ratio of e-graph size to match + count does that stop being true? Use lane 2's numbers (60,000 tuples, + 24 new) to argue the case that motivated egglog. +6. Backtracking checks the equality constraint as early as it can — our + `Compare` is emitted at the second occurrence, not at the end. Show + that this does *not* change the asymptotics on Figure 2, and describe + a pattern shape where it does. + +## Done when + +Answer each before unfolding it. + +- [ ] You can state, without looking, what an e-matching substitution is + and why the output is small even though the term set is quadratic. +
Answer + + A substitution σ maps each **pattern variable to an e-class**, and a + match is the pair `(σ, r)` where `r` is the root e-class holding the + matched terms (Definition 7, Definition 8). It is not a term. On + Figure 2 at N = 1600 the e-graph represents N² + 2N = 2,563,200 terms, + and `f(a, g(a))` has exactly N = 1600 matches — one per value of `a` — + all sharing the root `i_f`. The output is indexed by *classes*, so it + is bounded by the structure, not by what the structure denotes. +
+ +- [ ] You can classify a pattern's constraints and predict from that + alone whether relational e-matching will help. +
Answer + + Structural constraints come from the pattern's shape (which symbol + where); equality constraints come from a variable occurring more than + once. A pattern with no repeated variable is **linear**. Backtracking + exploits structural constraints immediately and can only check + equality constraints after building a candidate (§2.1), so the win is + proportional to the candidates that the equality constraints kill. + `f(a, g(a))`: N answers out of N² candidates — 21.7× measured. + `f(a, g(b))`: linear, N² answers out of N² candidates, nothing to + kill — measured **0.56×**, i.e. 1.8× slower. Predict the ratio of + candidates to answers and you have predicted the outcome. +
+ +- [ ] You can derive `bt visits = N² + N + 1` and `gj probes = 5N` from + the algorithms rather than from the table. +
Answer + + Backtracking: one `Scan` over the single e-class holding an `f` + e-node (the op index makes it 1, not N + 2), then `Bind f` over N + e-nodes, then `Bind g` over N e-nodes for each of those — 1 + N + N². + Generic join with ordering `[a, x, root]`: level `a` intersects two + N-key tries (N keys iterated + N probes = 2N); level `x` intersects + two singletons N times (2N); level `root` has one participating atom + with one key, N times (N). Total 5N. At N = 100 that is 10,101 and + 500, which is what lane 1 prints. +
+ +- [ ] You can compute the AGM bound of the triangle query and say what a + binary plan does instead. +
Answer + + Every variable of `Q(x,y,z) ← R(x,y), S(y,z), T(z,x)` sits in exactly + two atoms, so `w = (½,½,½)` is a fractional edge cover — each variable + gets ½ + ½ = 1. The AGM bound is `Π|Rᵢ|^{wᵢ} = M^½·M^½·M^½ = M^1.5`, + and it is tight. A binary plan must pick two atoms to join first; `R ⋈ + S` on `y` can reach `M²` tuples before `T` ever filters it. At M = + 10,000: M^1.5 = 10⁶ against an intermediate of 10⁸. +
+ +- [ ] You can apply Theorem 10 to both of lane 1's tables and get the + measured numbers. +
Answer + + `time = O(√(|Q(I)| × Π_i |R_i|))` with m = 2 atoms of N tuples each. + Lane 1a: |Q(I)| = N, so the bound is `√(N·N²) = N^1.5` — at N = 1600, + 64,000, and 8,000 probes were measured, comfortably inside. Lane 1b: + |Q(I)| = N², so the bound is `√(N²·N²) = N²` — 2,560,000 at N = 1600, + and 2,561,603 probes were measured, i.e. *at* the bound. Optimality + bounds waste, not time: with a quadratic answer, quadratic work is + optimal and the constant decides the winner. +
+ +- [ ] You can say what Table 1's `Worst` column means and why it is not + an embarrassment. +
Answer + + `Worst` is the smallest EM/GJ ratio over the patterns in that + configuration — 0.76 for `math` at 217,396 e-nodes without index + building, and 0.03 for `math` at 8,205 with it, meaning generic join + was 33× slower on some pattern. §5.2: speedup tracks how much + backtracking wastes, and a densely matched pattern wastes nothing. It + is the same result as this topic's lane 1b, reproduced independently, + and it is why the useful question is "what fraction of the candidate + space is discarded" rather than "which algorithm is faster". +
+ +- [ ] You can explain why NP-completeness does not contradict the + optimality claims. +
Answer + + Kozen's NP-completeness is stated over the size of the **pattern**; + the paper's bounds are **data complexity**, in the size of the + e-graph with the pattern held fixed (§1). In practice patterns have a + handful of nodes and e-graphs have millions, so the fixed-pattern + regime is the real one. The exponent hidden in the constant is the + pattern's — Theorem 10's `N^m` has the atom count `m` in it. +
+ +## References + +- Yihong Zhang, Yisu Remy Wang, Max Willsey, Zachary Tatlock, + **"Relational E-matching"**, POPL 2022, arXiv:2108.02290. Figure 2 + (the e-graph), §2.1 (the constraint taxonomy), Figure 3 (backtracking), + §2.3 (AGM, generic join), §3.1 (e-graph → database), Figure 8 + (unnesting), §3.4 (Theorems 9 and 10), §4.3 (functional dependencies), + §5 (evaluation, Table 1). +- Max Willsey et al., **"egg: Fast and Extensible Equality + Saturation"**, POPL 2021, arXiv:2004.03082 — the e-graph and the + 60–90% measurement. Read + [topic 21's guide](../21-formal/reading-egg-popl21.md) first. +- Hung Q. Ngo, Christopher Ré, Atri Rudra, **"Skew Strikes Back: New + Developments in the Theory of Join Algorithms"**, SIGMOD Record 2013 — + generic join and the AGM bound, if you want the database-side + treatment. +- Albert Atserias, Martin Grohe, Dániel Marx, **"Size Bounds and Query + Plans for Relational Joins"**, FOCS 2008 — the AGM bound itself. +- Next in this topic: [reading-egglog-pldi23.md](reading-egglog-pldi23.md), + which starts from §6.4's open problem. diff --git a/verify.sh b/verify.sh index 7ae60aa..39157ae 100755 --- a/verify.sh +++ b/verify.sh @@ -94,6 +94,7 @@ BENCHES=( "41-onchain-analytics:chain_bench:haircut tainting smears one theft over everyone" "42-recommendations-social:social_bench:the popularity trap" "43-ops-dependency-graphs:ops_bench:one gray failure, thirty-four alerts" + "44-egraphs-egglog:ematch_bench:N matches, N^2 candidates — e-matching as a join" ) # topic dir : criterion bench : what it measures (--criterion only: minutes each)