vaelii.impl.dense-jtms — com.vaelii/vaelii 0.19.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)

The depths, the two adjacency maps and the three justification columns keyed by id are the fact-scaled half of that table, and the network reaches them through the TmsColumns interface rather than as fields. HeapColumns holds them in the fastutil maps above. Every relabel, sweep and mutation below is written once against the interface, so an implementation that holds the six elsewhere runs the same fixpoint.

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's node lists 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-protocol/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 :type :handle-ceiling, an actionable error naming the ceiling and carrying :remedy {:tms :reference} (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.

copy-into! clj

(copy-into! target src)

Copy every structure of dense network src into target, which must hold no node, under target's write stamp. read-image! reads into a fresh network and this moves the result into the one a KB already holds: the KB holds its network by identity, so an image cannot replace the object, and reading into a scratch network first means a truncated image leaves the KB's network untouched.

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}.

image-version clj

The byte image's layout number. read-image! refuses any other, so an image written under an earlier set of justification columns is discarded rather than misread.

node-count clj

(node-count t)

How many nodes dense network t holds — the bitmap's cardinality, read under a read stamp without materializing a handle.

read-image! clj

(read-image! t i)

Read an image write-image wrote from i into dense network t, which must hold no node. Throws IllegalStateException for a populated t and IllegalArgumentException for bytes that are not an image of image-version; both are a caller's error rather than a state of the KB, since vaelii.impl.belief-image checks the manifest before it reads a byte.

write-image clj

(write-image t o)

Write the whole of dense network t to o, under a read stamp, so a concurrent reader is not held up and a writer waits for the image to finish.