For contributors — how XLOG works internally. This page assumes you work on the engine itself. It is dense on purpose, but every internal name is glossed on first use.
XLOG is a CUDA-backed logic engine. It has one language frontend and several execution backends. Source programs enter through the xlog-logic crate. They fan out from the normalized frontend into three reasoning intermediate representations: RIR for deterministic relational execution, PIR for probabilistic provenance, and EIR for epistemic semantics. Neural-symbolic training composes with the applicable reasoning route. SAT/MaxSAT and verification use the shared GpuCnf and CDCL solver service rather than another reasoning IR. Host-side control code then launches CUDA kernels over device-resident relation, circuit, and solver state. The important boundary is simple. The compiler and executor live on the host. The GPU holds relation buffers, kernel workspaces, solver arenas, and selected hot-path training state. “GPU-resident” refers to that device data plane, not to the host executor object. Tagged releases capture a fixed point in the source history. Use CHANGELOG.md and the selected artifact’s release notes to determine packaged availability; this page describes the implemented architecture without copying a mutable workspace version into prose.

Architecture Layers

The engine is organized into five layers, each owned by a small set of crates. Three reasoning-IR abbreviations appear above. RIR is the relational intermediate representation — the plan form the deterministic runtime interprets. PIR is the probabilistic intermediate representation — the provenance graph used by probabilistic execution. EIR is the epistemic intermediate representation — a separate plan form for epistemic (knowledge-and- belief) queries. XGCF is the downstream GPU circuit format produced by probabilistic knowledge compilation, while GpuCnf is the input representation for the shared CDCL solver service; neither is another reasoning IR. Three optimized join routes appear in the sections below (the table names WCOJ directly); here is what each name means. WCOJ (worst-case-optimal join) computes multiway graph patterns — such as triangles or cycles — without first building a large intermediate table. Free Join is a broader multiway-join route that applies to more rule bodies than the dedicated WCOJ kernels. Factorized delta keeps recursive intermediate results in a compact, unexpanded form instead of materializing every row. Each is expanded again below where it matters. Ten Rust packages are publishable on crates.io: xlog-cli, xlog-core, xlog-cuda, xlog-gpu, xlog-ir, xlog-logic, xlog-prob, xlog-runtime, xlog-solve, and xlog-stats. Five more packages are workspace-only — pyxlog, xlog-neural, xlog-induce, xlog-cuda-tests, and xlog-integration — and cover Python packaging, internal development, validation, or integration coverage.

Compile Pipeline

The deterministic compile path turns source text into a runnable plan. It is implemented in xlog-logic:
  1. parser::parse_program converts source text into the frontend AST.
  2. Meta and list builtins are normalized into the supported safe subset.
  3. Magic-set rewrites run, then negation-safety checks. (A magic-set rewrite restricts a rule so it only computes rows relevant to the query.)
  4. stratify computes dependency strata. Stratification splits the program into ordered layers so that recursion, negation, and aggregates each evaluate in a sound order.
  5. Lowerer::lower_program emits RIR execution plans.
  6. A set of refinement passes rewrites eligible plan shapes: helper-split, predicate-pushdown, selectivity, and multiway-promotion. (Helper-split breaks a plan node into smaller helper nodes the optimizer can specialize.)
Epistemic execution builds EIR directly from the parsed AST. Probabilistic execution builds PIR from provenance over the normalized program. Neither route branches from RIR. Neural predicates compose with the applicable symbolic route rather than introducing another reasoning IR. Features that require SAT/MaxSAT search or verification supply a device-resident GpuCnf to the shared CDCL service; the solver does not introduce an IR or compile into XGCF.

Runtime Boundary

xlog-runtime::Executor is the host-side interpreter and dispatcher for RIR plans. It holds the engine’s runtime state and decides which kernel route to run for each plan node. Concretely, the executor owns relation metadata, runtime statistics, and the persistent join-index cache state. It also owns common-subexpression telemetry, adaptive observations, and the dispatch counters for the optimized join routes: WCOJ, Free Join, aggregate fusion, and factorized delta. These route names are explained under Execution Families and Factorized execution routes below. The executor itself does not run on the GPU. It orchestrates work that does:
  • relation uploads and device-buffer ownership;
  • RIR node evaluation over CUDA kernels;
  • recursive SCC seed and delta iterations (an SCC is a strongly connected component of the rule dependency graph — the unit of recursive evaluation);
  • opportunistic route selection for WCOJ, Free Join, nested-loop, hash-join, groupby, and solver-backed operations;
  • diagnostics that show whether an optimized route actually fired.
Device-resident state lives in CUDA buffers and kernel workspaces managed by xlog-cuda. The host may launch kernels, synchronize streams, and read control status when an API requires it. The “no host transfer” claim for the data plane holds only for specific paths that track and expose that contract — not for the engine as a whole.

Execution Families

XLOG runs work through several execution families. Each has its own kernels and its own user-facing documentation. Three terms from that table are worth naming plainly. A worst-case-optimal join (WCOJ) computes multiway patterns — such as triangles or cycles — without first building a large intermediate table. Free Join is a broader multiway-join route that applies to more rule bodies than the dedicated WCOJ kernels. A CNF (conjunctive normal form) is the clause form a SAT solver consumes, and CDCL (conflict-driven clause learning) is the search algorithm the solver workspace runs over it.

Factorized execution routes

Factorized execution keeps intermediate results in a compact, unexpanded form instead of materializing every row, which lowers peak memory. The routes below are available in tagged artifacts beginning with 0.10.0. The implemented routes are:
  • aggregate-fused WCOJ for selected triangle, 4-cycle, and clique aggregate shapes;
  • GPU Free Join for general multiway bodies, plus factorized count-by-root (a count computed per root node without expanding the full join);
  • dense and sparse factorized recursive-delta routes for transitive-closure shaped recursion (the delta step is the semi-naive idea of only processing newly derived rows each iteration);
  • factorized non-count aggregate folding in probabilistic provenance.

Operational Contracts

XLOG favors an explicit decline over silent semantic drift. When an optimized path cannot handle a shape, it says so rather than quietly returning a different result. The contracts a contributor must preserve:
  • Unsupported optimizer or kernel shapes fall back to the ordinary route. The fallback returns the same row set (row-set parity).
  • Solver and compilation guards are fail-closed. They return typed errors instead of turning an incomplete proof into a reported success.
  • CUDA-required release gates must run on a GPU host with the environment variable XLOG_REQUIRE_CUDA=1.
To confirm that a specific optimized route actually fired, read the runtime counters, toggle the relevant kill switch (a flag that disables a route so you can compare against it), or run the certification commands. A correct final answer alone does not prove GPU residency or an optimized dispatch — always check the counters.