DBLog is a change-data-capture (CDC) mechanism for copying a table or selected keys from a source database while continuing to stream new changes from its commit log. It reads a table in primary-key ordered chunks and brackets each read with low and high watermarks in the source log. A chunk row is discarded if a log event for the same key appears anywhere in that window. The remaining rows are emitted as refresh events after the high watermark. DBLog allows backfills to run at any time during normal operation, rather than only as an initial bootstrap, while writes and live capture continue. It was introduced in the 2019 Netflix Tech Blog post and further discussed in the 2020 DBLog paper. The mechanism has since been adopted by open-source projects, including Debezium and Apache Flink CDC. The original blog post and paper explained this mechanism but did not provide a formal correctness proof or a precise description of its replay result. In this paper, we formalize how chunk reads and log events are combined and prove that their replay reconstructs the source state up to a specific log position for the keys being copied. We define this as a virtual cut, representing a snapshot-equivalent replay without requiring a physical snapshot. DBLog emits the events needed to reconstruct the source state downstream, without storing that state itself. To verify executions independently, we provide a certificate that validates this equivalence from recorded log evidence and chunk observations. Once chunk processing completes and covers all keys, this guarantee extends to the whole table. Furthermore, appending subsequent change-stream events advances the cut forward, formalizing the seamless transition from historical backfill to live streaming. All definitions and proofs are mechanized in Isabelle/HOL.

翻译：暂无翻译