Technical Summary: Machine-Checked Dual-Write Recovery from a Committed Log

Problem Statement

The paper addresses the fundamental uncertainty inherent in "dual-write" scenarios: a process commits a fact to a source database and subsequently attempts to deliver an effect to a sink (e.g., sending an email, publishing to a broker, updating a cache). If the process crashes between the send operation and the recording of that send (checkpoint), the recovery process faces an unsolvable question using only its local state: Did the sink already accept the effect?

The paper argues that standard operational advice (retries, idempotency keys, fencing) is largely sound but lacks a precise formal account of when it works. Specifically, existing literature has not rigorously defined:

1. The exact event the guarantees refer to.
2. The specific evidence required to make a recovery decision.
3. The lifetime of that evidence.

The core problem is an information bound: two reachable post-crash states can be byte-identical from the perspective of the crashed side (including its database, write-ahead log, and checkpoints) yet differ in whether the sink accepted the effect. Consequently, any recovery policy relying solely on the crashed side's durable state must either duplicate a delivery or abandon committed work.

Methodology

The paper employs formal verification using Isabelle/HOL to construct a machine-checked theory of dual-write recovery. The methodology involves:

• Model Construction: The author defines a series of increasingly complex state machines (substrates) to model the system:
  • Effect Machine: Models the core interaction between a source history and a sink ledger.
  • Checkpointed Machine: Adds a durable progress cursor to model the "deliver-then-checkpoint" protocol.
  • Channel Machine: Introduces a "wire" to model in-flight messages (stragglers) and arrival fences.
  • Concurrency Machine: Models multiple concurrent recovery processes and claim fences.
  • Store Tier Model: Formalizes the relationship between Change Data Capture (CDC)/outbox patterns and the source log.
• Proof Strategy: The paper utilizes a mix of negative results (constructions of reachable states that defeat specific classes of policies) and positive results (conditional theorems proving exactness under specific premises).
• Machine-Checking: Every theorem, definition, and proof is verified in Isabelle/HOL. The trusted base is minimal (standard library theories only), ensuring that the results are deductive rather than heuristic.

Key Contributions and Results

1. The Information Bound (Theorems 1–3)

The paper proves that no recovery policy can achieve exactly-once delivery if it relies solely on the crashed side's durable state (store, control plane, or checkpoints).

• Theorem 1 (Observation Bound): Constructs two reachable states where the core store and generation are identical, but the sink's acceptance record differs. Any policy observing only the core must choose a batch that causes a duplicate in one world or a loss in the other.
• Theorem 3 (Checkpoint Dilemma): Even with a deterministic "deliver-then-persist" protocol and a durable cursor, a crash occurring in the window between delivery and persist creates two indistinguishable states (from the local view) that require opposite recovery actions. The cursor itself cannot resolve this; the dilemma is the window, not the cursor's accuracy.

2. The Escape via Sink Reading (Theorem 4)

The paper identifies the necessary escape: reading the sink's durable, per-operation accepted record.

• Theorem 4 (Sink-Reading Escape): If the recovery process can read the sink's authoritative record of accepted work, it can compute a "delta" (committed obligations minus accepted records) to re-drive exactly the missing work. This is exact under four premises: the record is hazard-free, the run is crashed, the frontier is in-range, and source coordinates are strictly ascending.

3. Handling Stragglers: The Arrival Fence (Theorems 5–6)

Reading the sink is insufficient if old messages from the crashed incarnation are still in flight (stragglers).

• Theorem 5 (Wire Bound): A policy that reads the sink but ignores the wire (in-flight messages) is defeated by a schedule where a straggler arrives after the read, causing a duplicate.
• Theorem 6 (Arrival Fence): The solution is an atomic fenced re-drive: heal the store, compute the delta, land the batch, and simultaneously raise a generation fence to the successor of the crash-time generation. This fence causes the sink to reject any subsequent arrivals from the superseded incarnation.
• Corollary 6.1: The paper proves the cost of this fence: it trades the possibility of a "rescue" (where a straggler completes work that was thought lost) for certainty at the chosen frontier.

4. Handling Concurrent Recoverers: The Claim Fence (Theorems 7–8)

When multiple recovery processes start simultaneously (e.g., due to an orchestrator failure), they can race.

• Theorem 7 (Second-Recoverer Bound): Two honest recoverers, each reading the sink and computing a delta, can both fire if they do not coordinate, leading to duplicates or losses.
• Theorem 8 (Completed-Claim Exactness): The solution is an atomic claim discipline: a recoverer must atomically set a fence to its generation and arm its batch under that claim. Only batches fired while the fence admits them are accepted. This serializes recovery attempts.

5. Evidence Lifetime and Truncation (Theorems 9–10)

The paper analyzes how long the evidence for exactly-once delivery lasts.

• Theorem 9: Proves that "exactly-once" is equivalent to "at-least-once" only if the deduplication memory is permanent. If the deduplication window expires, the guarantee is voided.
• Theorem 10 (Truncation Dilemma): If the source history is truncated (e.g., log compaction) such that the journal content is lost but only metadata (length) remains, recovery cannot distinguish between "work already done" and "work never committed." This forces a choice between fabricating work or abandoning it.

6. Store Tier Faithfulness (Theorem 11)

The paper formally validates the "outbox pattern" and CDC.

• Theorem 11: Proves that at the store tier, crash safety is equivalent to keeping the downstream derived image faithful to the committed log. However, it clarifies that this only solves the store-tier consistency; the delivery loop itself remains a dual-write problem requiring the mechanisms described above.

Significance and Claims

The paper claims to provide the first machine-checked, deductive account of dual-write recovery. Its significance lies in:

1. Precision over Slogans: It moves beyond the heuristic "exactly-once is impossible" or "just read the sink" to define the exact conditions (premises) under which exactly-once is achievable.
2. Formalizing the Boundary: It isolates the "acceptance boundary" where store-centric reasoning fails and sink-centric reasoning is required.
3. Cost of Guarantees: It explicitly proves the costs of safety mechanisms (e.g., the trade-off between straggler rescue and frontier certainty in fencing).
4. Operational Discipline: It provides a design checklist for practitioners:
   • Identify the sink's durable acceptance record.
   • Ensure the record is authoritative and current.
   • Use generation-based fencing for stragglers and concurrent recoverers.
   • Size deduplication windows and journal retention to exceed the maximum expected outage duration.
   • Monitor for "silent loss" (omissions) separately from duplicates.

The paper does not claim to verify specific deployed systems (like Kafka or Flink) but rather provides a theoretical framework to evaluate the guarantees of such systems. It asserts that the "duplicate email" incident described in the introduction was not a bug in the checkpointing logic, but a structural limitation of the information available to the recovery process, solvable only by querying the sink's acceptance state.