Overview
This research presents a machine-checked theory developed in Isabelle/HOL concerning dual-write recovery from a committed log, specifically addressing scenarios after a system crash. The core of the work provides a precise account of when common recovery practices are effective, detailing the specific event guarantees refer to, the required evidence, and the duration of that evidence.
Research Context
In distributed systems, a delivery process recovering from a crash frequently encounters a critical question its own database cannot resolve: whether the receiving side (the “sink”) has already processed a particular effect. This problem is relevant even with transactional outboxes and change data capture, which eliminate application-level dual writes. These mechanisms introduce a relay that performs delivery and records its progress as two distinct durable operations, reintroducing the same decision point in a subsequent stage.
For approximately a decade, practitioners have managed this boundary using various techniques, including retries, checkpoints, idempotency keys, and fencing. While operational advice for these methods is generally considered sound, a formal and precise explanation of their efficacy has been absent. The study aims to fill this gap by providing a rigorous, machine-checked theoretical framework.
Approach
The researchers developed a machine-checked theory within Isabelle/HOL. This formal verification approach allowed for a precise definition of the conditions under which dual-write recovery mechanisms function correctly. The methodology focused on identifying an information bound inherent to recovery decisions based solely on the crashed side's durable knowledge. It then explored how this bound can be circumvented and the various hazards that can emerge during recovery processes.
Findings
-
Information Bound in Recovery
A central finding is the identification of an inherent information bound. Two distinct post-crash states, both reachable, can agree on all durable information known by the crashed component. However, these states can still differ in what the sink has actually accepted. Consequently, any recovery decision derived solely from the crashed side's durable knowledge must either result in a duplicate delivery or leave an unfulfilled obligation.
This limitation is not attributable to faulty record-keeping. The study demonstrates that even a single, deterministic protocol – specifically, a "deliver-then-checkpoint" protocol that includes its own durable cursor within what recovery reads – can be compromised purely by the timing of a crash.
-
Escaping the Information Bound
The information bound can be escaped by reading the sink's accepted record. This approach provides the necessary evidence under stated premises to definitively determine the sink's state.
-
Hazards and Fencing Mechanisms
Even with knowledge of the sink's accepted record, the answer regarding delivery status can become stale. Hazards identified include an old request that remains in flight or the race condition created by a second recovery process. The research provides proved fencing mechanisms specific to each hazard, operating at the sink's acceptance boundary. The cost associated with implementing these fencing mechanisms is also quantified as a theorem.
-
Lifetime of Guarantees
The guarantee provided by recovery mechanisms has a finite lifetime. The study proves that this guarantee is voided under specific conditions: a bounded deduplication memory and a truncated source history.
-
Test for Exactly-Once Recovery
The research distills a short test for evaluating any claim of exactly-once recovery. This test requires answering three questions: "what did the sink accept?", "what can still change that answer?", and "how long will the evidence survive?".