AI 中文总结
本文在 Isabelle/HOL 中构建经机器验证的理论，针对崩溃后交付恢复的双写边界问题，明确了信息边界、风险与 fencing 措施，为恰好一次恢复声明提供了测试方法。
AI 中文摘要
崩溃发生后，交付过程会面临自身数据库无法回答的问题：对方是否已经接收到该操作的影响？事务外箱和变更数据捕获（CDC）消除了应用的双写操作，但它们引入的中继会将自身的交付进度记录为两个独立的持久化操作，因此相同的决策会在后续阶段再次出现。十年来，从业者一直通过重试、检查点、幂等键和 fencing（ fencing 是一种用于避免脑裂的机制）来处理这一边界问题，相关操作建议大体上是合理的，但一直缺少对其适用场景的精确说明：即这些保证所涉及的具体事件、所需的证据以及该证据的有效时长。本文在 Isabelle/HOL 中开发了一种经机器验证的理论，填补了这一空白，其核心是一个信息边界。崩溃后的两个可达状态可以在崩溃方持久化已知的所有内容上达成一致，但在接收方（sink）已接受的内容上存在差异，因此从该侧计算的任何恢复决策要么会重复一次交付，要么会留下一次未完成的交付。这并非是簿记操作不严谨的问题：仅确定性的“先交付后检查点”协议（其自身的持久化游标也包含在恢复读取的内容中）就会被崩溃时机本身所破坏。在规定的前提条件下，读取接收方的已接受记录可恰好突破该信息边界。不过，该答案可能会失效：例如仍在传输中的旧请求、与第一个恢复方竞争的第二个恢复方，每种风险在接收方的接受边界处都有已被证明的 fencing 措施，而 fencing 本身的成本也已通过定理得到验证。最后，该保证有其有效期：有限的去重内存和截断的源历史都会以已证明的方式使该保证失效。由此，对任何“恰好一次”恢复声明的简短测试为：接收方接受了什么？还有什么因素仍可能改变该答案？该证据将在多久内保持有效？
英文摘要
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.
Comments23 pages, 5 figures. Machine-checked Isabelle/HOL formal development archived at https://doi.org/10.5281/zenodo.22700396
