Worst-case-optimal leapfrog-unification join, byte-identical to the ProductZipper - #124
Worst-case-optimal leapfrog-unification join, byte-identical to the ProductZipper#124MesTTo wants to merge 11 commits into
Conversation
MesTTo
changed the title
a519aeb to
9c72bfa
Compare
|
Both points taken, and done on the branch. The module now sits on The move surfaced a real bug, so the critique earned its keep. Unification being orthogonal to join order is now also a test: a nested-loop reference join over Re-verified end to end: the corpus including the declined shape, 4000 random flat conjunctive One note: |
|
Two more things landed on the branch, found by pushing the differential harder. The head position was exempt from unification: with the relation head baked into the seek prefix, a variable query head returned nothing where the ProductZipper binds it to every stored head, and a wildcard stored head was invisible under a ground query head. The prefix is now the arity byte alone and the head is column 0, so both directions go through the same column machinery as every other position, and the corpus pins both cases. With the head a column, the routing gate's per-fact scan lost its purpose, and the shape declines went with it: the per-column step is Re-verified end to end: a 12-case corpus, 4000 random trials with variable heads, wildcard-headed facts, and compounds on both sides, 0 fallback, 0 mismatches; a 20000-seed in-module differential against a nested-loop reference over the same |
|
One more commit on the branch: the engine now dispatches, so this is no longer only a standalone
Dispatch is policy-gated on measurement, not reflex: only bodies with a variable column shared by Evidence, all in the branch: every The standalone repo follows: |
|
If this is indeed capable of running through metta_calculus, please run it over the existing main.rs benchmark test and benchmark suite with a flag. I.e., not touching main.rs, just toggling the (experimental) feature flag. And report on the |
|
Ran the validation on the PR branch, release build with
The asymptotic separation is in
Stock grows 20x then 28x from one clique size to the next; leapfrog grows 2.2x then 1.4x. That is the WCO/AGM separation, and it widens with query size. At k=3 the dispatch overhead makes it a wash, by k=5 it is 150x and still opening up. process_calculus: identical result, identical unification count (3,431,002), VM instructions drop from 1,062,604,016 to 544,133,432 (1.95x fewer) for the same work. Its wall-clock is unchanged because its bottleneck is the emit, not the join. bfc, counter_machine, finite_domain, taxi_lts, tile_puzzle_states, and transitive are within single-run wall-clock noise with byte-identical results. No regression. Numbers are single-run wall-clock, so the sub-benchmarks within a few percent are run-to-run noise; the clique separation is large enough to be unambiguous. |
|
Follow-on stacked on this: #130 adds factorized evaluation of the aggregate sinks (COUNT/SUM/MIN/MAX/AND in O(N^fhtw) via GHD sum-product and Yannakakis semi-join reduction), byte-identical to the enumerate sinks and gated on Alloy-checked soundness conditions. It builds directly on this join, so it reduces to just the aggregation commits once this lands. |
|
Current numbers on this tip (e491c44, O(s) on the AGM triangle where the ProductZipper is O(s^2) (the constant PZ us/s^2 column is the quadratic); the wired column is the whole engine step through metta_calculus with dispatch on. |
zipper_join.rs answers a conjunctive (exec .. (, ..) ..) by seeking the PathMap byte-trie one variable at a time and intersecting factors on each shared variable, instead of materializing the product the ProductZipper builds. The term encoding, unification, and answer emit are expr's own (Tag/byte_item, unify, apply); the module contributes the seek order. Behind a self-contained router it returns exactly the ProductZipper's answers on the conjunctive fragment it covers (ground and free-variable answers, and data-side capture of a query compound), and runs in O(s) on the AGM triangle where the ProductZipper is O(s^2). It declines the one compound shape a per-column union-find is provably unsound on (proofs/ZipperUnifySafe.thy, nonflat_uf_unsound), keeping it on the ProductZipper, and an assignment whose bindings close a cycle yields no row, mirroring Expr::_unify's occurs rejection. Depends only on PathMap and expr, and adds one pub mod line. cargo run --example wco_leapfrog reproduces the differential and the scaling table.
The relation head was baked into the seek prefix, so it was exempt from unification in both directions: a variable query head returned nothing where the ProductZipper unifies it with every stored head, and a wildcard stored head was invisible under a ground query head. The prefix is now the arity byte alone and the head is column 0 like any argument, so both directions flow through the ordinary column machinery (a ground head seeks exact plus wildcards, a variable head enumerates). With the head a column, the per-fact gate scan lost its meaning and its need: the per-column step is full unification with cycle rejection at emit, so no query or fact shape requires a decline. The router now takes every nonempty relation-prefixed conjunction, the once-declined join-propagated capture included, and the routability check is parse-level, reading nothing from the map (it was a full fact scan per query). Verified: the corpus grows head-position and cycle cases (11 shapes, all matching the ProductZipper), the random distribution gains variable heads, wildcard-headed facts, and compound columns (4000 trials, 0 fallback, 0 mismatches; variable-headed patterns keep total arity 3 so they cannot match the harness's own exec and ans atoms, which is full-evaluation semantics rather than the compared query), and an in-module adversarial differential runs the raw join against a nested-loop reference over the same unify on eleven templates around the old boundary (20000 seeds, 0 mismatches). The triangle is unchanged within noise: the O(1) gate pays for the head column.
TotalRouterSafe.thy: a solution of an equation system solves every subsystem (solvable_mono, the per-level pruning), pairwise unifiability does not give a simultaneous solution (threading_necessary, why one bindings store threads the whole descent), and a variable equated with a term properly containing it has no finite solution (occurs_unsolvable, the emit-time cycle rejection). nonflat_uf_unsound stands as the boundary of the retired byte-level union-find, the mechanism whose decline this router no longer needs. Checked with isabelle build -D proofs.
A fully-wildcard fact captures a compound and propagates it through a four-factor cycle: (h $s1 $u1) binds $u1 to (k v3), which (e (k $s0) v2) then absorbs. The total router finds the answer row, byte-identical to the ProductZipper; the shape is the one a route co-tuned to the old decline structurally misses, so the corpus pins it.
The space-to-space transform, the ,/, exec path, now routes its body through query_multi_dispatch: a nonempty relation-prefixed conjunction with a variable occurring as a whole column in two or more factors runs on the worst-case-optimal join, and everything else, with interpreted sources, sinks, and the pattern dumps, keeps the ProductZipper path. The join streams one callback per product tuple: an accepted leaf reconstructs its per-factor stored facts (a re-indexed factor's columns go back to original order and numbering), pairs them with the pattern exactly as query_multi_raw does, and re-derives the bindings with mork_expr::unify, so the template emit downstream is stock and byte-identity is inherited rather than re-proven. MORK_LEAPFROG=0 pins the stock path per thread; =all dispatches every routable body. The policy is measured, not assumed. The triangle runs 240x end to end through metta_calculus at s=4096. The counter machine, whose bodies never intersect, would run 3.4x slower dispatched everywhere (callgrind: 3.3x the instructions) and stays stock at parity; a 10^6-tuple pure product would run 1.8x slower and stays stock. Nil's bfc chainer is at parity too, its hot single-factor sol lookups correctly left stock (forced dispatch costs it 21%), and byte-identical off/on at every proof size with the bench's own assertions passing. Every resource program is byte-identical both ways to 2000 steps, as are 20000 random whole programs with chained exec atoms and machinery collisions, the corpus, and 4000 random single-flip trials, each also run through the wired engine; the transform's match count and changed flag agree case by case.
The shipped policy dispatched any body with a variable column shared by two factors, which routed finite_domain, a functional pipeline whose factors share columns, onto the join for a 3.7x loss (bench: 70ms stock, 261ms dispatched). The gate is now the actual boundary of the worst-case-optimal advantage, three conjuncts, cheapest first: the body must be cyclic over its whole-column variables (a cycle carried only inside compounds gives the seek nothing; the counter machine measured 1.6x slower without this), cyclic over its full variable sets (alpha-acyclic queries are where a relation-at-a-time plan already meets the optimal bound), and not functionally degenerate (a diamond of function tables is FD-acyclic, its AGM bound linear, per Gottlob-Lee-Valiant-Valiant and Abo Khamis-Ngo-Suciu). The first two conjuncts read no data; the third probes each simple factor's trailing functional dependency over the facts, one shared scan per prefix, dead at the first determinant collision, capped at 200k rows, so a genuine graph pattern stops paying within its first facts and dispatches. Measured: finite_domain 70.3ms stock / 79.4ms dispatched (the residual is the one-time confirm scan of the genuinely functional tables); counter machine 12/13ms parity; the s=4096 triangle keeps 2602ms -> 10ms. Resources, bfc, the corpus, 4000 trials, and 20000 random whole programs stay byte-identical; a policy test pins the four routing classes.
The full bench suite measured the boundary inside the cyclic non-functional class. bench transitive's triangle detect over a million uniform random edges ran 15% slower dispatched (the product never blows up there, so the join's per-candidate machinery loses on constants), while bench clique's 6- and 10-factor queries ran 50x faster dispatched, and the hub triangle keeps its 250x. The gate now reads a bounded region of the instance before dispatching: every relation tiny declines, since the ProductZipper's straight-line constants win outright; four or more join factors dispatch, since the product deepens multiplicatively while the join stays output-bounded; a three-factor body dispatches only when a bounded sample of first-argument values finds a heavy hitter, the hub a product blows up through. A hub outside the sample window is missed and the body merely stays on the stock path; the exact version of this decision is the cost-based dispatch these capped cursor walks approximate. Measured after: transitive 1.01 (from 1.15), clique 0.02 (kept), tile_puzzle 1.01, finite_domain 1.00, the s=4096 triangle 2506ms -> 10ms (kept), every other bench at parity. Resources, bfc, the corpus, 4000 trials, and 20000 random whole programs stay byte-identical, and the policy test pins all seven clauses.
…und_join ground_join opened a fresh read-zipper at prefix+bound for every column of every factor at every recursion node, re-walking the byte-trie from the root each time (the dominant cost; the join is compute-bound). Hold one SubtermCursor per factor instead, opened once at the relation prefix and walked column by column with a floor stack (SubtermCursor::descend_floor/ascend_floor): the zipper descends and ascends in place, never re-opened from root. Byte-identical to the prior join (ground_join_matches_brute_force) and, measured on a 3000-node/150k-edge graph (7,369,139 two-hop answers), 2731ms -> 1139ms (2.4x). ground_join_parallel partitions the leading variable's domain across worker threads by hash (hash(value) % nworkers), each running the join on the SHARED READ-ONLY map into its own buffer, concatenated at the end. Safe by construction: concurrent reads of an immutable PathMap, no shared writes; the workers' answer sets partition the whole, so the result equals sequential ground_join (ground_join_parallel_matches_sequential). Same graph: 1139ms -> 121ms at 32 workers (byte-identical). ground_join_for_each streams answers without materializing the domain. See examples/ground_join_parallel.rs.
…a only ground_join does not unify. It is complete only when every joined relation is fully ground; on schematic data it is a strict subset of the ProductZipper and silently drops answers (a stored (sol $n ..) is not matched against a query (sol Z ..); a nonground compound query column stays unconsumed). A caller that may join over schematic facts must detect that and route to a unifying join. Making the contract explicit at the API so callers gate correctly.
The routing block in query_multi_dispatch now compiles only under a new default-off leapfrog feature, so the default build takes the stock ProductZipper path unconditionally; with the feature on, the MORK_LEAPFROG runtime toggle keeps working within it, and the wco_leapfrog example requires the feature. This is the review shape requested on the PR: the join under an experimental flag, main.rs untouched. The gate contract is modeled in Alloy (fac26 in MesTTo/alloy-mork): routing requires feature AND toggle AND flat shape, every other state is the stock engine, and answers are gate-independent.
PathMap already exposes this as BitMask::test_bit (src/utils/mod.rs:609), implemented for ByteMask. The local copy duplicated it byte-for-byte and indexed the mask words directly instead of going through the bounds-checked accessor. least_ge keeps its next_bit call: ByteMask::next_bit is strictly greater-than, so testing k first is a real gap it fills.
|
dropped the local the report, by instruction and transition count so it doesn't move machine to machine. at s=4096 the ProductZipper retires ~63B instructions and the leapfrog ~250M, a 250x gap. the transition counts are exact: 99654, 395846, 1578054, 6301766, 25186374, 100704326 across s=128 to 4096, 4x per doubling, so Θ(s²) vs the leapfrog's linear scan. byte-identical answers at every s. no relation-at-a-time plan hits the AGM bound on the triangle, the seek does. on the gate: it's one WCO join behind a profitability check, not a planner picking among kernels. routability is parse-level, and the check reads bounded cardinality off the trie, so it's deterministic. yeah it's cost-based in the broad sense, but bounded and deterministic, not the wall-clock router i cut from #128. it's there because dispatching everything regresses the shapes the leapfrog can't win (counter_machine, transitive, finite_domain, bfc). if the read still bugs you i can make it purely structural, keeps most of the win. #130 is stacked on this, so its diff includes this whole file + the ghd.rs aggregation. once this lands it rebases to just the aggregation. |
2 participants
MORK evaluates a conjunctive
(exec .. (, p1 p2 ..) ..)body with the ProductZipper, arelation-at-a-time join that materializes the intermediate product before pruning it. On a triangle
over a hub that product is the s² two-paths through the hub, pruned to the few real triangles. This
module,
kernel/src/zipper_join.rs, is a variable-at-a-time leapfrog join over the PathMapbyte-trie: it fixes one join variable at a time and intersects the factors on it by seeking the
trie, so the two-paths are never built. It depends only on PathMap and
expr, and the engineintegration is one added function and one call-site change in
space.rs. The term encoding, theunification, and the answer emit are
expr's own (Tag/byte_item,unify,apply); the modulecontributes the seek order.
A router sends every nonempty relation-prefixed conjunction to the join and returns exactly the
ProductZipper's bytes; the routing decision is parse-level. And
metta_calculusnow dispatches:the space-to-space transform routes its body through
Space::query_multi_dispatch, somork runevaluates intersecting conjunctive bodies on the join with no program change. On the AGM-blowup
triangle
(e $x $y) (e $y $z) (e $x $z)over a hub of s in-edges and s out-edges:The ProductZipper's transitions grow as s² and its microseconds over s² hold near 0.14, so it is
Θ(s²); the leapfrog is linear on this instance, so the ratio widens with s, to 240x at s = 4096.
The wired column is the whole engine step through
metta_calculus, dispatch on: the engine addsnothing over the raw join. Both return the same three triangles. No relation-at-a-time plan
reaches the AGM bound on the triangle; the seek does (Ngo et al. 2012, Veldhuizen 2014).
How the engine dispatch stays stock
A dispatched body streams through the join one callback per product tuple. Each accepted
assignment reconstructs the stored facts it sits on (a re-indexed factor's columns are put back in
original order and numbering, which a test pins on a coreferent fact), pairs them with the pattern
factors exactly as
query_multi_rawdoes, and re-derives the bindings withexpr'sunify. Sothe effect closure sees the bindings the ProductZipper path produces, the template instantiation
and emit downstream are stock code fed the same inputs, occurs failures are skipped where stock
skips them, and match multiplicity is preserved (a transform-level test pins
touchedand thechanged flag per body). Interpreted sources and sinks (
I/O) and the pattern-directed dumpskeep the stock path and its enumeration order.
MORK_LEAPFROG=0pins everything stock, perthread, which is how the differentials hold one arm as the reference.
Dispatch follows a measured policy: a body routes to the join only when it has a
cycle the leapfrog can seek and win on, over an instance where winning is possible. The shape
conjuncts come first and read no data: cyclic over the whole-column variables (a cycle carried
only inside compound arguments gives the seek nothing; the counter machine measured 1.6× slower
without this conjunct), and cyclic over the full variable sets (alpha-acyclic queries are where a
relation-at-a-time plan already meets the optimal bound, which declines paths, semijoins,
enumerations, and pure products outright). Then the instance decides, through bounded cursor
walks. Every relation tiny: decline, the ProductZipper's constants win either way (the tile
puzzle's 56-fact inequality tables). Four or more join factors: dispatch, the product deepens
multiplicatively while the join stays output-bounded (
bench clique's 6- and 10-factor queriesrun 50× faster dispatched, 15.6 s to 0.3 s). Exactly three factors: dispatch only when a bounded
sample of first-argument values finds a heavy hitter, the hub a product blows up through (the
240× triangle);
bench transitive's triangle detect over a million uniform random edges hasnone, measured 15% slower dispatched, and declines to exact parity. Last, the functional
dependency probe: a diamond of function tables is a real hyperedge cycle whose AGM bound still
collapses to O(N), so a bounded scan detects each simple factor's trailing dependency and re-runs
the reduction (
finite_domain, exactly that shape, measured 3.7× slower under the earliestshared-column rule and declines at parity now). A hub outside the sample window or a mislabeled
instance only ever falls back to stock performance; the exact version of these decisions is a
cost-based dispatch, which the capped walks approximate. The policy
test pins all seven clauses, and the full
mork benchsuite runs at parity or faster both ways,byte-identical, with
clique50x faster dispatched.Data-side capture, head included
A variable in a stored fact is a wildcard, so the join unifies in both directions. For a query factor
(r (a $p) b)against a fact(r $d b), the stored$dbinds the whole compound(a $p). Arelational leapfrog binds query variables to stored subterms but not stored variables to query
subterms; this module recovers that second direction, the step MORK's matcher performs.
The head position is a column like the rest: the seek prefix is the arity byte alone, so a variable
query head unifies with every stored head, and a wildcard stored head is captured under a ground
query head. An earlier revision baked the head into the seek prefix, and the differential caught
both directions returning too little as soon as it generated those shapes; the corpus pins them
now.
cargo run --example wco_leapfrogsends a 12-case corpus and 4000 random conjunctive queries(variable heads, wildcard-headed facts, and compound columns on both sides included) through the
stock engine, the router, and the wired engine, and diffs the bytes:
The engine level is sealed in-repo: every program under
kernel/resources/runs to several depthswith the dispatch off and on and must produce identical spaces and step counts (a CLI sweep
extends this to 2000 steps), and 20000 random whole programs, several exec atoms with chained and
machinery-colliding bodies run for several steps, must agree the same way.
bench bfcpasses itsown proof assertions in every mode at size 19 (801 steps, a 2.9M-atom space), and the same
program as plain MM2 files is space-byte-identical off/on at every size 5 through 19; it runs at
parity, since its hot bodies are single-factor
sollookups with no product to prune (dispatchedeverywhere anyway it runs 21% slower, which is what the policy is for). An in-module
differential additionally runs the RAW join, no router, against a nested-loop reference over the
same
unifyon eleven templates centered on the hardest shapes: any divergence would sit in theseek order, not the unification.
No declined shape
Earlier revisions held one body back from the join: the capture that binds a non-ground compound
and propagates it through a shared variable, where a per-column union-find diverges from
unification (
nonflat_uf_unsound, ZipperUnifySafe.thy). The per-column step is no longer thatunion-find. It is
unifythreaded through one bindings store, and an assignment whose bindingsclose a cycle is rejected at the answer emit, mirroring
Expr::_unify, which covers the shape: therouter is total on relation-prefixed conjunctions. The corpus pins the recovered case, a
fully-wildcard fact capturing a compound and propagating it through a four-factor cycle,
byte-identical to the ProductZipper.
proofs/carries the Isabelle theories, checked withisabelle build -D proofsunder Isabelle2025.RoutingSafe.thyandZipperUnifySafe.thyprove the ground and flat coincidences and the retiredbyte-level mechanism's boundary.
TotalRouterSafe.thycarries the total router's facts: a solutionof an equation system solves every subsystem (
solvable_mono, the per-level pruning), pairwiseunifiability does not give a simultaneous solution (
threading_necessary, why one bindings storethreads the whole descent), and a variable equated with a term properly containing it has no finite
solution (
occurs_unsolvable, the cycle rejection).Ground join: held cursors and data parallelism
The ground special case,
ground_join, opened a fresh read-zipper atprefix + boundfor everycolumn of every factor at each recursion node, re-walking the byte-trie from the root each time. That
re-descend was the join's dominant cost (it is compute-bound). It now holds one
SubtermCursorperfactor, opened once at the relation prefix and walked column by column with a floor stack
(
SubtermCursor::descend_floor/ascend_floor): the zipper descends into a chosen column value andascends back out in place, never re-opened from the root. Byte-identical to the prior join
(
ground_join_matches_brute_force) and, on a 3000-node / 150k-edge graph (7,369,139 two-hopanswers), 2731ms -> 1139ms (2.4x).
ground_join_parallelthen partitions the leading variable's domain across worker threads by hash(
hash(value) % nworkers), each running the join on the shared read-only map into its own buffer,concatenated at the end. It is data-race free by construction: the workers only read the immutable
PathMapand each owns its output, and the leading-variable hash partition is a disjoint cover, sothe workers' answer sets union to exactly sequential
ground_join's(
ground_join_parallel_matches_sequential). Same graph: 1139ms -> 121ms at 32 workers,byte-identical, 22.6x over the original.
ground_join_for_eachstreams each answer to a closurewithout materializing the domain.
Reproduce:
RUSTFLAGS="-C target-cpu=native" cargo +nightly run -p mork --release --example ground_join_parallel.Scope
The module is a join-stage addition, the worst-case-optimal form of the ProductZipper's semantics
on join-bound conjunctive bodies, now reaching
mork runthrough the dispatch. It claims nothingabout whole-program time where the exec loop is iteration-bound rather than join-bound, and it
deliberately leaves enumeration-shaped bodies, interpreted sources and sinks, and the dumps on the
stock path; the per-eval cost-based dispatch that could also take the compound-shared class is the
next step.
A standalone repo rebuilds all of this from fresh clones of MORK and PathMap at pinned commits;
run.shoverlays the module and the engine patch, runs the demonstration, and now runs YOURprogram:
./run.sh yourfile.mm2evaluates it on the wired engine, and./run.sh compare yourfile.mm2 [steps]runs both engines and diffs the result spaces:https://github.com/MesTTo/mork-wco-leapfrog