AI 中文总结
广义DBLog研究CDC中复制与日志交接问题，提出并验证了在多种变体下重建源表行的条件，确保数据一致性，并经过形式化验证。
AI 中文摘要
变更数据捕获（CDC）通过数据库的已提交行变更日志，向下游系统（如缓存、搜索索引和数据仓库）提供数据。在引导启动、添加表或修复下游数据时，管道还必须复制现有行。将这种复制与活动日志合并引入了复制到日志的交接问题。变更不得落入间隙，较旧的复制状态不得覆盖较新的日志更新或复活已删除的行。Netflix开发的DBLog通过分块读取表并将这些读取与实时日志交错来解决此问题。水印标识与每次读取重叠的变更，当复制的行过时时，日志获胜。Debezium和Flink CDC此后采用了此设计。早期工作证明，按发出顺序应用原始算法的复制行和日志变更，可以重建源表的行，包括所处理的每个日志插入、更新和删除的效果。广义DBLog探讨了该设计的变体在何种条件下能保持相同的结果。我们陈述了源和捕获实现必须满足的条件。一旦复制和协调完成，我们证明该结果适用于所有选定的表和键范围，即使它们的行是在不同时间读取的。复制不需要单一数据库快照。进一步的日志变更一次一个事件地推进重建状态。我们为经典水印、Debezium的信号表和只读模式、Flink CDC的并行块、绑定到精确日志位置的读取和转储，以及日志位置位于已知范围内的引擎一致备份建立了这些保证。完整理论在Isabelle/HOL中经过机器检查，其核心在Lean 4中独立验证，协议还通过TLA+中的有界模型检查进行了检验。
英文摘要
Change-data capture (CDC) feeds downstream systems like caches, search indexes, and data warehouses from a database's log of committed row changes. When bootstrapping, adding a table, or repairing downstream data, a pipeline must also copy existing rows. Merging this copy with the active log introduces the copy-to-log handoff problem. Changes must not fall through a gap, and older copied state must not overwrite a newer logged update or resurrect a deleted row. DBLog, developed at Netflix, addressed this problem by reading tables in chunks and interleaving those reads with the live log. Watermarks identify the changes that overlap each read, and the log wins when a copied row is stale. Debezium and Flink CDC have since adapted this design. Earlier work proved that applying the original algorithm's copied rows and logged changes in their emitted order reconstructs the source's rows, including the effect of every logged insert, update, and delete processed. Generalized DBLog asks when the same result holds for variants of that design. We state the conditions the source and capture implementation must satisfy. Once copying and reconciliation are complete, we prove that the result holds across all selected tables and key ranges even when their rows were read at different times. A single database snapshot is not required for the copy. Further logged changes advance the reconstructed state one event at a time. We establish these guarantees for classic watermarking, Debezium's signal-table and read-only modes, Flink CDC's parallel chunks, reads and dumps tied to exact log positions, and engine-consistent backups whose log position lies within known bounds. The complete theory is machine-checked in Isabelle/HOL, its core independently verified in Lean 4, and the protocols are also examined by bounded model checking in TLA+.
Comments40 pages, 6 figures. Formal verification artifacts: https://doi.org/10.5281/zenodo.22643866
