arXiv subjects

Andreas Andreakis

Publications and source records attributed to Andreas Andreakis.

4 recordsLinked to original sources

arXiv2026

Generalized DBLog: A Verified Contract for Interleaving Database Rows with a Change Log

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+.

cs.DB↗

arXiv2026

Machine-Checked Dual-Write Recovery from a Committed Log

Applications often need to make related facts durable in two independent systems without a transaction spanning both. If a 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. The engineering problem is familiar, and systems address it with retries, checkpoints, idempotency keys, and fencing. Formal verification has covered transaction isolation, crash safety within one store, and protocols with a shared commit. The closest formal studies model-check particular outbox designs. What is missing is a deductive account of this recovery boundary over arbitrary policies that can read the source side but not the sink's acceptance record. We give this account in Isabelle/HOL. The main result is an information bound. 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.

cs.DB↗

arXiv2026

A Theoretical Study of DBLog: Certified Virtual Cuts for a Snapshot-Equivalent Replay of Live Databases

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.

cs.DB↗

arXiv2020

DBLog: A Watermark Based Change-Data-Capture Framework

It is a commonly observed pattern for applications to utilize multiple heterogeneous databases where each is used to serve a specific need such as storing the canonical form of data or providing advanced search capabilities. For applications it is hence desired to keep multiple databases in sync. We have observed a series of distinct patterns that have tried to solve this problem such as dual-writes and distributed transactions. However, these approaches have limitations with regard to feasibility, robustness, and maintenance. An alternative approach that has recently emerged is to utilize Change-Data-Capture (CDC) in order to capture changed rows from a database's transaction log and eventually deliver them downstream with low latency. In order to solve the data synchronization problem one also needs to replicate the full state of a database and transaction logs typically do not contain the full history of changes. At the same time, there are use cases that require high availability of the transaction log events so that databases stay as closely in-sync as possible. To address the above challenges, we developed a novel CDC framework for databases, namely DBLog. DBLog utilizes a watermark based approach that allows us to interleave transaction log events with rows that we directly select from tables to capture the full state. Our solution allows log events to continue progress without stalling while processing selects. Selects can be triggered at any time on all tables, a specific table, or for specific primary keys of a table. DBLog executes selects in chunks and tracks progress, allowing them to pause and resume. The watermark approach does not use locks and has minimum impact on the source. DBLog is currently used in production by tens of microservices at Netflix.

cs.DB↗