Verified methods ensure safe merging of copied and live database changes
Generalized DBLog: A Verified Contract for Interleaving Database Rows with a Change Log
DatabasesDistributed, Parallel, and Cluster ComputingLogic in Computer Science
Summary
When databases send updates to other systems, they often need to copy existing data and keep track of new changes without mistakes. The authors study how to safely combine this copied data with live updates so that no changes are lost or overwritten incorrectly. They show how to do this correctly across different scenarios, even if the data is copied at different times or in parts. Their results come with strong mathematical proofs checked by computer tools to make sure everything is reliable.
change-data capturedatabase logcopied rowslive logwatermarksdata consistencyDebeziumFlink CDCIsabelle/HOLLean 4
Authors
Andreas Andreakis
Abstract
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+.