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)