Skip to main content

Correctness invariants

These invariants are the shortest way to review a Nereus Delay data path. They focus on durable behavior rather than wire encoding.

1. Apply before source acknowledgement​

RocksDB synchronous apply
  happens-before
Kafka source commit or Pulsar source acknowledgement

The Command result, message state, indexes, deduplication changes, and applied Source Position belong to the same durable Shard update. If the process fails before that update, the source record remains replayable. If the source is acknowledged, recovery must be able to find the applied result locally or in an allowed checkpoint.

2. Record PUBLISHING before producer ownership​

Publish Admission applied as durable PUBLISHING
  happens-before
Kafka or Pulsar producer side effect

The scheduler may Claim work earlier, but Claim is reversible. Producer I/O begins only after the admitted Attempt can be reconstructed. A crash can therefore recover a durable PUBLISHING record instead of incorrectly assuming that no send began.

3. Order callbacks through the Shard Log​

Producer callback or recovered evidence
  becomes a Publish Outcome mutation
  before it changes message state

Callbacks do not update RocksDB directly. The resulting mutation is ordered with Cancel, Reschedule, expiration, retry, and Control Operations, and stale outcomes remain bound to their message generation and Attempt identity.

4. One source order per Shard​

Client Commands and authenticated System Mutations share one physical Command Topic partition and one Source Position order. Thread timing, local clocks, callback arrival order, and Oxia watch delivery are not alternative semantic orders.

5. Ownership ambiguity fails closed​

A Worker needs both the accepted source assignment and the matching Oxia Owner Lease. It restores and replays before becoming ACTIVE_FOR_COMMANDS. Lane readiness is separate. Losing ownership stops new side effects; ownerEpoch fences local state but does not erase a request that may already have reached a remote Broker.

6. Source and evidence gaps fail closed​

Recovery must prove a continuous source prefix after the selected checkpoint. A missing source range, mismatched resource incarnation, invalid signature, unsupported protocol tuple, or incomplete required evidence cannot be skipped as if nothing happened.

7. Time uncertainty may delay, never advance​

The trusted UTC interval authorizes a not-before action only when the safe boundary has passed. An ambiguous clock window pauses admission or terminal expiration; it cannot create an early delivery.

Review shortcut​

For any change, ask:

  1. What is the authoritative ordered input?
  2. What durable state proves the operation may proceed?
  3. What happens if the response is lost after external ownership?
  4. Which identity rejects a stale retry or callback?
  5. Can an allowed checkpoint plus continuous replay reconstruct the result?