Skip to content

perf(provenance): prove from the snapshot with bound-column indexes - #212

Merged
jsam merged 1 commit into
mainfrom
fm/il-r04
Oct 3, 2026
Merged

jsam merged 1 commit into
mainfrom
fm/il-r04

Conversation

@jsam

@jsam jsam commented Oct 3, 2026 •

Copy link
Copy Markdown
Contributor

R04: snapshot-based indexed proof preparation for .why / .why full / .why_not (#134, on top of S06).

What it does

  • No deep copy per proof call. ProofContext borrows the snapshot's rules and Arc-shared relations, plus the evaluation's derived RelationMap. Removed KnowledgeGraphSnapshot::proof_inputs, relation::to_vec_map and StorageEngine::execute_and_get_context, which copied every base relation into fresh vectors on each .why. S06 already released the storage guard before proof search; that is unchanged.
  • Bound-column indexes, built at most once per proof call. provenance::proof_relations::ProofRelations answers subgoal lookups by their bound columns. A (relation, bound columns) pattern is scanned as before until it repeats 4 times in one call, then indexed once (about 3 scans' cost at ≤100K tuples) and reused for every later row. A tiny proof over a large KG builds nothing; a call over many findings stops being O(findings × relation).
  • Same DAGs. Candidates come back in insertion order and callers verify them with their existing equality, so proof DAGs are identical, node ids included. Index hashes agree with unification equality: Int32/Int64 of equal value share a key, and so do -0.0/0.0.
  • Existence checks, negation, why-not and aggregate inputs all use the same lookups. No locks added; the index cache is per-call RefCell state.

Evidence (local, release build, loaded shared host)

workload before p50 after p50
.why 1 row over 100K edges (query alone: ~6.9 ms) 12.9 ms 7.9 ms
.why 380 findings over 20K txns: proof phase 57.8 ms 6.1 ms
.why 380 findings: end to end 72–97 ms 40–45 ms
  • Proof DAG dumps of all 22 .why/.why_not example files (28 statements) are byte-identical before and after. The affected .iql.out specs pass.
  • New tests:
    • indexed vs scan-only proofs and why-not equal across recursion, negation, aggregates, comparisons, mixed widths and signed zeros (mutation-checked);
    • a write committed between snapshot capture and proof search does not change .why, .why full or .why_not.
  • tests/credential_revocation_tests.rs relied on the quadratic scan to make its proof slow. It now grows its graph until the proof takes ≥100 ms.
  • benches/proof_benchmarks.rs added.

Known limit

Proof search on left-recursive rules (reach(X,Z) <- reach(X,Y), link(Y,Z)) is still exponential in path length. That was already the case before this PR and is out of scope here.

Tracker: #199

@jsam
jsam changed the base branch from fm/il-rc1 to main October 3, 2026 20:44
@jsam
jsam marked this pull request as ready for review October 3, 2026 20:44
@jsam jsam closed this Oct 3, 2026
@jsam jsam reopened this Oct 3, 2026
A `.why` copied every base relation and the derived data of its
evaluation into fresh vectors, and proved each subgoal by scanning its
whole relation. The gateway proves every finding on every turn, so a
call over many findings cost O(findings x relation size) on top of an
O(KG) copy.

- ProofContext borrows the snapshot's rules and Arc-shared relations
  and the evaluation's derived RelationMap; nothing is copied per call.
  proof_inputs, to_vec_map and execute_and_get_context are removed.
- ProofRelations answers subgoal lookups by bound columns. A (relation,
  bound columns) pattern is scanned as before until it repeats four
  times in one call, then indexed once (about three scans' cost) and
  reused for every later row. Lookups return candidates in insertion
  order and callers verify them with their own equality, so proofs visit
  matches in the same order and build the same DAG, node ids included.
  Index hashes agree with unification: Int32/Int64 of equal value and
  -0.0/0.0 share a key.
- Existence checks, negation, why-not and aggregate inputs use the same
  lookups.

Tests: indexed proofs and why-not explanations equal scan-only ones
across recursion, negation, aggregation, comparisons, mixed integer
widths and signed zeros; a write committed between snapshot capture
and proof search does not change `.why`, `.why full` or `.why_not`.
The revocation test grows its graph until its proof is slow enough to
revoke during, instead of relying on the quadratic scan.

benches/proof_benchmarks measures a tiny proof over a large KG, many
findings per call, and recursive proofs.

Rebased onto main: the proof-search seam joins the meta-dispatch seam in
one test_hook module whose hooks follow a query to its blocking thread.
@jsam
jsam merged commit 2ba9a5a into main Oct 3, 2026
14 checks passed
@jsam
jsam deleted the fm/il-r04 branch October 3, 2026 21:36
jsam added a commit that referenced this pull request Oct 4, 2026
…ry request (#249)

The release-checkpoint performance gate fails on main: cheap_query serial
p50 is 1.110x the approved baseline e732cd5 on the 32-vCPU runner
(115 -> 126 us). Concurrent latency and throughput did not move. Bisected
to #214 (per-connection request pipelining), made worse by #222.

Cause: the pipeline runs requests in a `FuturesUnordered`. Its `poll_next`
wakes its own task and returns `Pending` after any poll that polled every
future in the set. With one request in flight, which is every serial
client, that happens on each request's first poll. The connection task
wakes itself, tokio schedules that as a yield, and a yield wakes an idle
worker to take the task. Each request therefore costs one more context
switch (4.0 -> 5.0 per query) and a hand-off of the connection task to
another core. #222 added no work per query but made the hand-off dearer:
user cycles per query rose 15% at the same instruction count.

Fix: keep one never-woken future in the set. After the pipeline's first
poll it is never polled again, so no poll reaches every future and the
forced yield no longer fires. The yield after futures that wake
themselves still applies. Pipelining, ordering, deadlines, cancellation
and the credential fence are unchanged. Nothing is added per request: no
lock, atomic or allocation. Each connection gets one more set node.

Bisect (cheap_query, `?edge(1, Y)`, serial). Server counters per query
from perf stat. Ratios are against e732cd5, from an interleaved probe
with one pinned server per commit, 40 rounds:

| commit | PR | user instr/query | ctx switches/query | p50 ratio |
|---|---|---|---|---|
| e732cd5 | baseline | 1.282M | 4.0 | 1.000 |
| d75ce6e | #208 atomic programs | 1.279M | 4.0 | 0.993 |
| 4578fe6 | #215 notification stream | 1.271M | 4.0 | 0.991 |
| 71a4d24 | #216 online backup | 1.275M | 4.0 | 1.016 |
| 2f621c5 | #200 first-update latency | 1.272M | 4.0 | 1.009 |
| e96df5c | #207 | 1.279M | 4.0 | 0.998 |
| 4dd8fe9 | #209 shard index | 1.272M | 4.0 | 0.987 |
| 277c7f0 | #206 | 1.274M | 4.0 | 1.008 |
| 3554c98 | #214 pipelining, deadlines | 1.296M | 5.0 | 1.020 |
| 3492a59 | #213 | 1.294M | 5.0 | 1.030 |
| 2ba9a5a | #212 provenance | 1.297M | 5.0 | 1.029 |
| 9ed61b4 | #204 key expiry | 1.297M | 5.0 | 1.027 |
| be35ee3 | #221 | 1.297M | 5.0 | 1.013 |
| c98a590 | #222 bounded streaming | 1.298M | 5.0 | 1.047 |
| a6fd628 | #219 wildcard fix | 1.297M | 5.0 | 1.061 |
| b7f7ad6 | #220 WAL durability | 1.300M | 5.0 | 1.056 |
| de54807 | #223 shared standing eval | 1.299M | 5.0 | 1.071 |
| 55ec34d | #225 checkpoint-1 fixes | 1.300M | 5.0 | 1.045 |
| 23712b8 | main | 1.300M | 5.0 | 1.064 |
| this change | | 1.300M | 4.0 | 1.033 |

Confirming A/Bs with the gate's own fixture (fresh pinned servers each
round, 40 rounds, ratio [95% interval]):

- #214 vs its parent 277c7f0: 1.039 [1.027..1.049]
- #222 vs its parent be35ee3: 1.025 [1.006..1.044]
- A/A 3554c98: 1.010 [1.002..1.025]
- e732cd5 -> main: 1.048 [1.028..1.066]
- main -> this change: 0.978 [0.958..0.989]
- e732cd5 -> this change: 1.021 [1.009..1.044], PASS (budget 1.05)

User cycles per query (perf stat, same instruction count): e732cd5 958K,
be35ee3 1053K, c98a590 1206K, this change 1006K.

Full gate, all fixtures, 20 rounds, servers pinned to CPUs 2-15:

- main -> this change: no metric worse. Every required metric is PASS, or
  INCONCLUSIVE with an interval that includes 1.0. cheap_query p50 0.979
  [0.953..1.007].
- e732cd5 -> this change: cheap_query p50 1.029 [1.019..1.072],
  INCONCLUSIVE on a busy host (load average up to 22); bound_query p50
  1.022, PASS. The insert and delta metrics improved since the baseline.

The shared host is about 4x slower per query than the CI runner, so the
same hand-off is a smaller share of each query here than there.

The remaining ~1.7% of user instructions per query since #214 is the
pipeline's own per-request bookkeeping: the boxed request future (one
4-8 KiB allocation), its set node, the request control and the in-flight
maps.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant