跳到主要内容

Guarantees

This page lists the guarantees Memlake gives Hindsight Enterprise, and how we check them.

  • Durable writes. A write is committed to object storage before Memlake acknowledges it, and before a synchronous retain returns. Losing a query node, its disk or its memory loses no acknowledged data.

  • Consistent reads. Every memory read (recall, get and list) sees every write acknowledged before it started, from any query node. There is no eventual-consistency window: memories not yet indexed are read from the log at query time. Aggregate counts, such as per-tag totals, may be computed as of the last index update.

  • Atomic writes. All operations in one write are applied together or not at all. A Hindsight retain (replacing a document's old facts, writing the new ones and registering newly seen entities) is one atomic write.

  • Consistent deletes. Get, list and recall apply the same visibility rule, so a deleted or replaced memory never reappears in one path while it is gone from another.

  • Complete indexes only. Readers always see a complete set of segments, never half of an index update, because publishing an index is a single conditional swap of the bank's manifest.

  • Safe garbage collection. Garbage collection deletes only files the current manifest no longer references, and only after a safety window (15 minutes by default) measured on the object store's own clock.

  • Organization isolation at the bucket. Each organization's memories live in their own bucket, which carries its own access policy, default encryption and delete scope. Bucket names are salted per deployment. Query query nodes are shared across organizations.

  • Any query node can serve any bank. High availability is the number of query nodes running, not a replica you pay for. Routing keeps a bank on the same query node for cache warmth; if that query node goes away, another takes the bank with no handover.

  • Object storage is the only stateful dependency for memory. Memlake has no database, lock service or consensus system of its own; all concurrency control goes through conditional writes to object storage. Hindsight keeps its operational data (banks and settings, the job queue, the audit log) in a small Postgres database, which holds no memories.

  • Compute separation. Indexing runs on separate indexer query nodes, so building indexes does not compete with recall for CPU.

  • Bounded memory for un-indexed writes. Reading writes that are not yet indexed is charged to one per-query node memory budget. If indexing falls behind, the query node rejects new writes with a retryable error rather than letting that data outgrow memory. A rejected write was never acknowledged, so nothing is lost.

  • Backups in a separate failure domain. When backups are on, an archiver continuously copies every bank's log, and a daily snapshot copies the rest, to a separate bucket, which can be in another account with a credential that cannot delete. A bank can be restored to a point in time, and each restore is verified before traffic is routed to it.

Verification​

Because correctness comes down to a handful of conditional writes, the protocol is small enough to prove. The write, indexing and garbage-collection protocols are specified in TLA+, and a model checker explores every possible interleaving of them: many writers and indexers racing, query nodes crashing at any step, responses lost, processes stalling for arbitrarily long. Across all of it, it checks that:

  • an acknowledged write is never lost, and a position in the log is never reused;
  • every query sees every acknowledged write, from any query node;
  • readers always see a complete index, never half of an update;
  • garbage collection never deletes anything still in use;
  • two indexers racing on the same bank stay safe with no lock between them.

Three things keep that from being a one-off exercise:

  • In CI. The specifications are re-checked on every change to the protocol code or the specifications, and nightly.
  • Against broken variants. Each specification has deliberately broken variants, with one safety mechanism removed, that the checker must catch, so we know the checks aren't vacuous.
  • Against the real engine. Executions recorded from the engine are checked against the specification, so the code can't drift from what was proven. A property-based test harness injects storage faults into the real code, and a nightly chaos test kills query nodes mid-flight and checks that no acknowledged write is lost.

Model checking is exhaustive within a bounded scope (a few writers, indexers and log positions), which is where interleaving bugs live. It verifies the protocol as specified; the trace checks and fault-injection tests tie that back to the code.

ACID​

Memlake provides Atomicity, Consistency and Durability.

Isolation does not broadly apply, because Memlake does not offer general read-write transactions. Each write is a single atomic entry, and writes to a bank are applied in log order. Replacing "all facts from this document" is evaluated at that write's own position in the log, so a replace and the new facts written with it cannot interleave with another writer's changes. For read-then-write updates, a write can carry a precondition on the log position, so a lost race is retried rather than applied.

CAP theorem​

Memlake prioritizes consistency over availability when object storage is unreachable: a query that cannot confirm it has the latest writes fails rather than returning stale results.

The one exception is the optional cross-encoder reranker that Memlake calls when it runs ranking for Hindsight. It fails open: if it is slow or unreachable, recall returns results in fused order and flags that reranking was skipped.

For more, see Architecture and Tradeoffs.