Memory Management
=================

ProvSQL persists provenance circuits across transactions and shares them
between PostgreSQL backend processes.  This is achieved through
memory-mapped files managed by a dedicated background worker, coordinated
via PostgreSQL shared memory.


Why Not Regular Tables?
-----------------------

Earlier versions of ProvSQL stored circuits in regular PostgreSQL
tables.  This worked but had severe performance limitations: the
PL/pgSQL functions that insert gates used ``LOCK`` to serialize
access, preventing parallelism.  The current architecture uses
memory-mapped files written by a single background worker, avoiding
both lock contention and WAL overhead.  Benchmarks in the ICDE 2026
paper :cite:`sen2026provsql` show that the mmap implementation
scales linearly with dataset size, while an earlier shared-memory
variant hit limits at moderate scale factors.


Background Worker: ``provsql_mmap``
-----------------------------------

The mmap subsystem lives in :cfile:`provsql_mmap.c` and :cfile:`MMappedCircuit.cpp`.

:cfunc:`RegisterProvSQLMMapWorker` (called from :cfunc:`_PG_init`)
registers a PostgreSQL background worker with the postmaster.  When the server
starts, the postmaster forks the worker process, which calls
:cfunc:`provsql_mmap_worker`:

1. **Initialization**: :cfunc:`initialize_provsql_mmap` is a no-op --
   circuits are opened lazily on the first IPC message for each
   database (see below).

2. **Main loop**: :cfunc:`provsql_mmap_main_loop` reads messages
   from a pipe, writes gate creations to the mmap store, and sends
   replies to lookup requests.  The loop exits when reading from
   the pipe fails (end-of-file or error), e.g. at server shutdown,
   which triggers the cleanup step below.

3. **Shutdown**: :cfunc:`destroy_provsql_mmap` syncs and closes all
   open per-database circuits.


Inter-Process Communication
---------------------------

Normal backends (the processes that execute SQL queries) cannot write
directly to the mmap files -- only the background worker does.  Two
anonymous pipes provide bidirectional IPC:

- **Backend-to-worker** (``pipebmr`` / ``pipebmw``, ``bm`` for
  backend-to-mmap-worker): backends send gate-creation and lookup
  requests.
- **Worker-to-backend** (``pipembr`` / ``pipembw``): the worker sends
  replies to lookup requests (e.g., the gate type or children
  answering a query; gate creation gets no reply).

Pipe writes use buffered macros (:cfunc:`STARTWRITEM` /
:cfunc:`ADDWRITEM` / :cfunc:`SENDWRITEM`) that respect ``PIPE_BUF``
atomicity guarantees -- each message is delivered as an atomic unit
even when multiple backends write concurrently.

Every message begins with a one-byte opcode followed immediately by the
sender's ``MyDatabaseId`` (a 4-byte ``Oid``).  The worker reads this
OID before dispatching to the correct per-database
:cfunc:`MMappedCircuit` instance, opening a new one lazily if this is
the first message for that database.


Shared Memory: ``provsql_shmem``
--------------------------------

The pipe file descriptors and a lightweight lock live in a PostgreSQL
shared-memory segment managed by :cfile:`provsql_shmem.c`.

The :cfunc:`provsqlSharedState` structure contains:

- **lock** -- a PostgreSQL ``LWLock`` coordinating pipe access from
  multiple backends.  Messages that fit in a single ``PIPE_BUF``
  write are sent under a *shared* lock, relying on the kernel's
  ``PIPE_BUF`` atomicity guarantee; the exclusive mode is reserved
  for oversized multi-part writes and for request-reply round trips.
- **pipebmr / pipebmw** -- file descriptors for the backend-to-worker
  pipe.
- **pipembr / pipembw** -- file descriptors for the worker-to-backend
  pipe.

Lifecycle:

- :cfunc:`provsql_shmem_request` (called from ``shmem_request_hook`` on
  PostgreSQL >= 15) reserves the required shared-memory size.
- :cfunc:`provsql_shmem_startup` (called from ``shmem_startup_hook``)
  allocates the segment, creates the pipes, and initializes the lock.

Locking helpers (:cfunc:`provsql_shmem_lock_exclusive`,
:cfunc:`provsql_shmem_lock_shared`, :cfunc:`provsql_shmem_unlock`) wrap
the ``LWLock`` API.


Mmap-Backed Data Structures
----------------------------

:cfunc:`MMappedCircuit` (in :cfile:`MMappedCircuit.cpp`) is the
persistent circuit store.  The worker maintains one instance per
database in a ``std::map<Oid, MMappedCircuit*>``, created lazily on
first use.  Each instance holds five mmap-backed containers, stored in
``$PGDATA/base/<db_oid>/``:

- ``provsql_mapping.mmap`` -- a :cfunc:`MMappedUUIDHashTable` mapping
  UUID tokens to gate IDs, enabling O(1) lookup.
- ``provsql_gates.mmap`` -- a :cfunc:`MMappedVector` of
  :cfunc:`GateInformation` records, one per gate.
- ``provsql_wires.mmap`` -- a :cfunc:`MMappedVector` of
  ``pg_uuid_t``, the flattened child-UUID lists.
- ``provsql_extra.mmap`` -- a :cfunc:`MMappedVector` of ``char`` for
  variable-length per-gate string annotations.
- ``provsql_table_info.mmap`` -- a :cfunc:`MMappedVector` of
  :cfunc:`ProvenanceTableInfo` records, one per provenance-tracked
  relation; see :ref:`per-table-metadata` below.

Placing the files under ``$PGDATA/base/<db_oid>/`` gives per-database
isolation and automatic cleanup: PostgreSQL removes that directory when
the database is dropped.

Every mmap file begins with a **16-byte format header**:

.. code-block:: c

   uint64_t magic;      /* file-type identifier, e.g. 0x7365746147537650 for gates */
   uint16_t version;    /* format version, currently 1 */
   uint16_t elem_size;  /* sizeof(T) at write time */
   uint32_t _reserved;  /* padding, must be 0 */

The constructor validates all three fields on open and throws if they
do not match, catching type mismatches and incompatible recompilations
early.

Gate-Type ABI
^^^^^^^^^^^^^

The :cfunc:`gate_type` enum in :cfile:`provsql_utils.h` is
persisted: each :cfunc:`GateInformation` record's ``type`` field
stores the numeric enum value, not the name. The enum is
therefore **append-only**: new gate types must be added before
the ``gate_invalid`` sentinel without renumbering existing
values, and pre-existing files must remain readable by a
recompiled extension.

The companion ``provsql_arith_op`` enum (used in ``info1`` of
every ``gate_arith`` gate to identify the operator) follows
the same rule: ``PLUS = 0`` through ``PERCENTILE = 10`` are
persisted on disk and must not be reordered.

The float8 mode of ``gate_value`` introduced for the
continuous-distribution surface does not require a format
version bump: the ``extra`` blob is text, both kinds of consumer
parse that same text representation (the ``HAVING``-side
``extract_constant_string`` in :cfile:`having_semantics.cpp`, and
the ``std::stod``-based float8 readers such as
``extract_finite_double`` in :cfile:`RangeCheck.cpp`), and the
choice of parser is made by the consumer at evaluation time based
on the gate's surrounding context.

Beyond ``gate_value`` literals, the ``extra`` blob carries the
``gate_assumed`` assumption label, ``gate_annotation`` certificates,
``gate_rv`` distribution parameters, and the ``gate_mobius``
per-child coefficient map (which :cfunc:`MMappedCircuit`'s extra-copy
path preserves verbatim, the same mechanism as ``gate_arith``).  The
``info1`` field doubles as the persisted **d-DNNF certificate** on
``gate_plus`` / ``gate_times`` gates (deterministic / decomposable
bits, written via the internal ``set_infos`` entry point by the
reachability and joint-width compilers and loaded back by
:cfunc:`createGenericCircuit`).

:cfunc:`MMappedVector` (:cfile:`MMappedVector.h` /
:cfile:`MMappedVector.hpp`) provides a ``std::vector``-like interface
over an mmap region: appending with ``add``, random access (and
in-place update) with ``operator[]``, and size queries with
``nbElements``.

:cfunc:`MMappedUUIDHashTable` (:cfile:`MMappedUUIDHashTable.h`) is an
open-addressing hash table keyed by 16-byte UUIDs, stored in an mmap
region.

These data structures grow by extending the underlying file and
remapping.  Because only the background worker writes, there are no
concurrency issues within the mmap files themselves.

.. _per-table-metadata:

Per-Table Provenance Metadata
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

The fifth mmap file per database, ``provsql_table_info.mmap``, is
the registry the safe-query rewriter consults to decide whether a
given base relation contributes independent (TID), block-correlated
(BID), or correlated-in-ways-we-cannot-rule-out (OPAQUE) tuples,
and what the base-relation ancestry of the relation is.

Each record is a fixed-stride :cfunc:`ProvenanceTableInfo` struct
(:cfile:`MMappedTableInfo.h`) with two logically independent
halves:

- **Kind half** -- ``relid`` (primary key), ``kind`` (one of
  ``PROVSQL_TABLE_TID`` / ``PROVSQL_TABLE_BID`` /
  ``PROVSQL_TABLE_OPAQUE``), ``block_key_n`` and
  ``block_key[PROVSQL_TABLE_INFO_MAX_BLOCK_KEY]`` (the BID
  block-key column numbers ; multi-column keys supported, capped
  at 16).  Written by ``add_provenance`` (TID), ``repair_key``
  (BID), ``set_table_info`` (manual ; also reached by the
  ``provenance_guard`` trigger flipping the relation to OPAQUE
  when the user supplies their own ``provsql`` UUID).
- **Ancestor half** -- ``ancestor_n`` and
  ``ancestors[PROVSQL_TABLE_INFO_MAX_ANCESTORS]`` (the sorted,
  deduplicated ``pg_class`` OIDs of the original
  ``add_provenance`` / ``repair_key`` relations this one's atoms
  ultimately come from ; capped at 64).  Base tables auto-seed
  ``{self}`` ; CTAS-derived tables inherit the transitive union
  of source ancestor sets via the lineage hook
  (:ref:`tid-bid-propagation`).  Written by :sqlfunc:`set_ancestors`,
  read by :sqlfunc:`get_ancestors`, cleared by :sqlfunc:`remove_ancestors`.

The two halves are updated independently via separate IPC opcodes
(``T`` / ``D`` / ``s`` for the kind half ; ``A`` / ``R`` / ``a``
for the ancestor half) so a CTAS hook can set ancestry without
disturbing kind and vice versa.  The worker reads-modifies-writes
each record on partial-update opcodes so the two halves stay
consistent.

Removal uses a **tombstone scheme**: removed entries have their
``relid`` overwritten with ``InvalidOid`` and remain in place.
:cfunc:`MMappedCircuit::setTableInfo` and
:cfunc:`MMappedCircuit::setTableAncestry` reuse tombstone slots
before appending.  All readers skip ``InvalidOid`` entries.  This
avoids reaching into :cfunc:`MMappedVector`'s append-only public
API and keeps the file format trivial: a crash-recovered file is
internally consistent without any extra recovery step.  In
practice, churn on this vector is low (one entry per
``add_provenance`` / ``repair_key`` / ``remove_provenance`` call,
plus one per CTAS hook fire).

A backend-local cache (:cfunc:`provsql_lookup_table_info` and the
parallel :cfunc:`provsql_lookup_ancestry`, both in
:cfile:`provsql_utils.c`) amortises IPC across repeated lookups
in the planner hot path.  Both caches are sorted arrays keyed on
``relid``, binary-searched, and invalidated through
``CacheRegisterRelcacheCallback`` so concurrent
``add_provenance`` / ``repair_key`` / ``remove_provenance`` /
``set_ancestors`` in other backends are reflected without
polling.  The ``cleanup_table_info`` event trigger on
``sql_drop`` (installed by the extension's SQL surface) removes
the metadata when a tracked relation is dropped outside of
``remove_provenance``.

.. warning::

   ``provsql_table_info.mmap`` was introduced in 1.6.0, and the
   :cfunc:`ProvenanceTableInfo` layout grew from ~36 to ~300 bytes
   during that release's development (the ancestor half was
   appended), so only mid-1.6.0-dev builds could have written the
   short layout.  Such a stale file fails the ``elem_size``
   validation at :cfunc:`MMappedVector` open and must be deleted
   before restart ; the 1.5.0 -> 1.6.0 upgrade script seeds a TID
   entry for every tracked relation it detects from the catalog,
   as part of introducing the store.


Per-Backend Circuit Cache
-------------------------

Every access to the persistent circuit -- creating a gate,
reading a gate type, fetching the children of a gate -- goes
through the anonymous pipe to the mmap worker.  That pipe trip
is cheap but not free, and for a query that touches thousands
of gates the round-trips dominate the wall-clock cost of the
SQL functions that wrap them.  :cfunc:`CircuitCache` (in
:cfile:`CircuitCache.cpp`, with a C-linkage shim in
:cfile:`circuit_cache.h`) is a small in-process cache whose
sole purpose is to avoid those round-trips for gates that the
same backend has seen recently.

A cache entry stores a gate's UUID, its :cfunc:`gate_type`, and
the list of its children.  The cache is backed by a Boost
``multi_index_container`` with two indices: a sequenced index
(used as FIFO eviction order) and a hashed-unique index on the
UUID (for O(1) lookup).  It is bounded by a fixed byte budget;
when inserting a new entry would exceed the budget,
:cfunc:`CircuitCache::insert` drops the oldest one.  The cache
is single-threaded: it lives as a file-scope singleton in
:cfile:`CircuitCache.cpp`, so each PostgreSQL backend process
has its own instance and there is no sharing between backends.

The C functions in :cfile:`circuit_cache.h` that
:cfile:`provsql_mmap.c` actually calls are:

- :cfunc:`circuit_cache_create_gate` -- insert a gate into the
  cache.  Returns ``true`` if the gate was newly inserted,
  ``false`` if it was already present.  The return value does
  *not* gate the IPC write: :cfunc:`provsql_internal_create_gate`
  always falls through to the worker, because a cache hit only
  proves the token was seen by this backend, not that the worker
  has the gate (skipping the write on a hit silently dropped gates
  under concurrent backends).  :cfunc:`MMappedCircuit::createGate`
  is idempotent on already-mapped tokens, so the unconditional
  write is safe.

- :cfunc:`circuit_cache_get_type` -- look up a gate's type.
  Returns ``gate_invalid`` on a miss; the SQL wrapper then
  falls back to an IPC read and, on success, re-enters the
  gate into the cache so that subsequent lookups hit.

- :cfunc:`circuit_cache_get_children` -- same pattern for the
  children list, used by :sqlfunc:`get_children`.

The cache thus only accelerates *reads*
(:sqlfunc:`get_gate_type` / :sqlfunc:`get_children`): every
gate-creating call reaches the mmap worker, so the persistent
store always reflects the complete circuit even though
individual lookups may resolve locally.

The data-decomposition compilers add a second, coarser per-backend
cache on top: a set of already-materialised root tokens, so
re-materialising an unchanged certified circuit (a warm rerun of the
same reachability or joint-width query) skips the per-gate IPC
entirely.  It is sound for the same reason the gate cache is: the
store is append-only and the worker pipe ordered, so a token seen
created by this backend can never designate anything else.  The
compilers also materialise at **content-addressed** UUIDs (v5 hashes
of the construction recipe, including the *plus-canonical* and
*times-canonical* namespaces probed by :sqlfunc:`provenance_plus` /
:sqlfunc:`provenance_times`), so any query phrasing that combines the
same token multiset lands on the already-planted gates.


Reading Circuits Back
---------------------

When a semiring evaluation function is called (e.g.,
:sqlfunc:`sr_boolean`), it needs to build an in-memory circuit from
the persistent mmap store.  The function :cfunc:`getGenericCircuit`
performs a breadth-first traversal starting from the root gate's
UUID, reading gates and wires from the mmap store and constructing
a :cfunc:`GenericCircuit` in process-local memory.  This is the
primitive used by all circuit readers.

Probability evaluation (:sqlfunc:`probability_evaluate`), Shapley
and Banzhaf value computation, and the :cfunc:`BoolExpr` semiring
need a pure Boolean circuit (AND / OR / NOT) suitable for knowledge
compilation and model counting.  They call
:cfunc:`getBooleanCircuit`, which first builds a
:cfunc:`GenericCircuit` via :cfunc:`getGenericCircuit` and then
evaluates it under the :cfunc:`BoolExpr` semiring to produce a
:cfunc:`BooleanCircuit`.
