vaelii.impl.dense-jtms — com.vaelii/vaelii 0.9.0

The dense truth-maintenance network — the :tms :dense option, the default since 0.9.0 (it holds the network in ~3.8× less RAM at corpus scale; docs/density.md).

The JTMS is always resident, so its footprint is a wall in its own right (measured: ~467 B/node, which is ~43 GB at 100M nodes), and the decomposition (lein bench-jtms) says exactly where the bytes are:

  nodes  71%   <- 310 B/node of it is the per-node MAP OBJECT and its HAMT slot
  in     13%   <- 100% dense; RoaringBitmap measured 384x here
  groundable 13%

Two findings shape everything below. The per-node scalars are already free — stripping :depth, :premise? or :datum from the reference releases nothing, because they are shared cached objects (small Longs, keywords, booleans). So the lever is not "shrink the fields", it is "stop having a map per node": a node here is a bit in a bitmap and, where it has one, an entry in a primitive-keyed map. And belief sets are the opposite regime from the index's postings — bench-postings found RoaringBitmap a loss (1.07-1.45x) on the index's millions of tiny postings, while :in holds nearly every node and compresses 384x. Both measurements are right; density is the variable.

  nodes / premises / in / groundable / defeated / blocked
  touched / touched-in / touched-new                         RoaringBitmap
  depths                                    Int2IntOpenHashMap  (absent => 0)
  supports / consequences   Int2ObjectOpenHashMap<IntPostings>  (absent => empty)
  a justification            columns keyed by id, never an object  (see below)
  superseded                             atom of a persistent map  (sparse)

Two of those deserve their reasons. The defeat-classes are one bitmap because the lattice has exactly two elements (vaelii.impl.strength — monotonic > default, and the reference already stores only the entries above the bottom), so "the class map" is precisely "the set of monotonic datums". Adjacency reuses Phase 1's IntPostings (a sorted int[] promoted to a bitmap past 128) rather than a bare int[]: a node's supports are usually one or two, but the consequences of a much-used premise — a rule handle is an antecedent of every justification it licensed — grow without bound, and an array-copy insert would make loading such a rule quadratic.

Why this is a second implementation and not a swap

RoaringBitmap is mutable, and the reference is an atom over one persistent map whose all-or-nothing mutation jtms_atomicity_test pins. A mutable bitmap inside that value would break swap!'s retry semantics and let a reader observe a half-applied relabel — so the dense structures cannot be dropped into the reference, and the two ship side by side behind vaelii.impl.jtms/Tms. That is the same shape the index took (:memory-columnar is a whole second trie beside KvIndexStore), and it carries the same obligation: the algorithms are duplicated here against the dense structures, so jtms_dense_oracle_test proves the two answer identically under randomized operation streams before either is trusted.

Concurrency. A StampedLock gives the incidental reader the consistent view the single-writer contract owes one — "a reader thread beside a writer thread (the web browser over a REPL's KB) is the supported shape" (docs/storage.md), and the atom- over-persistent-map reference gives that reader a consistent view for free. The dense network mutates its bitmaps in place, so it earns the same guarantee with a lock, and the lock is chosen so the engine's own single writer never pays for it. Writers take the exclusive stamp — serializing exactly as the reference's swap! retry does. Point reads (in?, the hottest call in the engine, one per candidate on the match path) run optimistically: no lock in the steady state, since writes are bursty and reads are the hot path, validated after the fact and redone under a shared read stamp only if a write intervened or the lock-free read saw torn state. Iterating reads take the shared stamp directly — they already allocate O(nodes), so the acquisition disappears into the materialization, and an unlocked walk over a bitmap a writer is rewriting in place could tear. A reader never observes a partially-applied relabel; it sees the state either fully before or fully after, exactly as it would on the reference. The lock is non-reentrant: every protocol method below takes a stamp once and calls only raw-field helpers (no method re-enters), and every read body is side-effect-free (so the optimistic retry is safe).

Precondition. ensure-node precedes add-justification, and a justification's antecedents already have nodes — which every engine path does. (The reference tolerates the violation by growing a malformed phantom node; neither implementation is specified there.)

Limit. The bitmaps and the fastutil maps are int-keyed, so a handle or justification id must fit a 32-bit int: the ceiling is 2^31-1 = 2,147,483,647. Handles are allocated in assertion order and never reused, so this bounds a KB's cumulative allocations (~2.1B), not its live node count — 21x the engine's 100M target, but reachable by a long-lived writer that churns assert/retract for long enough. Crossing it throws an actionable error naming the ceiling and the {:tms :reference} remedy (check-handle!, at the two entry points a new id enters), rather than the bare "integer overflow" the cast would raise — and never a silent truncation that would collide two handles, so belief is never corrupted. A KB that expects to churn past 2^31 pins {:tms :reference}, whose Long-keyed persistent maps have no such ceiling. This is measured in density.md.

create-dense-tms clj

(create-dense-tms)

A fresh, empty dense truth-maintenance network — vaelii.impl.jtms/create-tms's counterpart, selected by open-kb's {:tms :dense}.