Machine-Checked Dual-Write Recovery from a Commit Log

Abstract

Applications often need to make related facts durable in two independent systems without a transaction spanning both. If the process crashes after the second system accepts an operation but before a source-side checkpoint is written, recovery cannot tell from source state alone whether to retry. Transactional outboxes and change data capture move this dual write out of an application process, but relay delivery and checkpointing remain separate durable operations. Systems address the problem with retries, checkpoints, idempotency keys, and fencing, and call the result exactly-once delivery. Whether that guarantee holds depends on which event it counts, what evidence recovery requires, and how long that evidence must survive. The closest formal studies model-check particular outbox and log-delivery designs, and their results hold only for the designs and instances they check. Answering the three questions in general requires statements about arbitrary recovery policies, which finite enumeration cannot reach. We prove them in Isabelle/HOL, and to our knowledge they have not been machine-checked before. The main result is an impossibility theorem for source-only recovery. We construct two reachable post-crash states with the same durable source-side state and different sink acceptance records. Any recovery policy based only on the source side must duplicate an effect in one state or leave it undelivered in the other. The same holds for a deterministic deliver-then-checkpoint protocol whose only nondeterminism is crash timing. An authoritative, complete, and current sink acceptance record lets recovery compute the missing operations when source coordinates distinguish them. We also prove arrival and claim fences for in-flight requests and concurrent recoverers. Finally, we show how bounded deduplication state and truncated source history limit the lifetime of the guarantee.