PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Andreas Andreakis

arXiv:2609.08160v4cs.DBcs.DCcs.LO

TL;DR

CDC pipelines must combine copied state with a continuing log without losing changes or letting stale rows override newer updates. Generalized DBLog formalizes conditions for that handoff and proves when replay reconstructs source state across selected data. The proofs cover several capture protocols, subject to stated conditions and scope boundaries.

  • Problem

    CDC pipelines need a baseline copy as well as live changes, but must avoid losing changes or allowing stale copied rows to override newer logged state.

    Source: §1.1 · p. 1, §1.2 · p. 1

  • Method

    The paper defines a source-and-capture correctness contract and proves a cut theorem for replaying copied rows together with logged changes.

    Source: §3.4 · p. 7, §13 · p. 38

  • Results

    The proofs establish the contract for watermarked DBLog, Debezium’s signal-table and read-only protocols, Flink CDC’s parallel chunks, and reads or dumps tied to log positions, with qualifications for some cases.

    Source: §13 · p. 38

  • Takeaways & Limitations

    The contract provides a common basis for assessing new ways of obtaining a copy against the source and connector properties needed for correct reconstruction.

    Source: §13 · p. 38

    For uncertain restores, the dataset must represent one engine-consistent source state within the recorded log bounds, and live-source tracking is guaranteed only from the known high bound onward.

    Source: §12 · p. 38

Abstract

from arXiv · show

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

1 Introduction

CDC pipelines must combine copied rows with an active log without losing changes or allowing stale copies to reverse newer updates. Generalized DBLog specifies conditions for this handoff and proves when the combined output reconstructs source state.

1.1 The production problem

  • A finite log may not provide the baseline a CDC pipeline needs, so bootstrap, expansion, and repair require copying state while avoiding lost changes and stale rows.This need can recur for a new sink, a newly added table, or downstream data loss.Source: §1.1 · p. 1

1.2 How copied state joins the change log

  • Two handoff shapes are analyzed: place a read at an exact log position, or bracket it with log positions and reconcile the overlap.An exact position depends on a promised read-coordinate relationship; an uncertain interval requires racing changes to be reconciled.Source: §1.2 · pp. 1–2

1.3 From DBLog to Generalized DBLog

  • DBLog brackets chunk reads with watermark events, and logged changes in the bracket take precedence over copied rows [1].Generalized DBLog asks when variants of this design yield a virtual cut: replayed output represents source state at one log position, assembled without a common-time physical snapshot.Source: §1.3 · p. 2

1.4 Contributions and reading paths

  • The contract’s cut theorem matches replayed output to the source for processed keys, then covers target tables and keys when all chunks finish without requiring a global database snapshot.Reads may occur at different times if each reflects source state within its watermark bracket; subsequent log events continue the reconstruction.Source: §1.4 · pp. 2–3
  • The proofs cover watermarked DBLog, Debezium and Flink CDC variants, and reads or dumps tied to log positions, with additional conditions for some PostgreSQL results.The framework is machine-checked in Isabelle/HOL, its central cut theorems are independently checked in Lean 4, and five bounded TLA+ models examine protocols and their composition.Source: §1.4 · p. 3

2 The Setting: Stores, Logs, and Coordinates

The model treats capture as a keyed store paired with a commit-ordered log, interpreted through coordinates that identify log prefixes. Its contract defines how copied state and log events relate, while leaving delivery and other downstream concerns outside its scope.

2 The Setting: Stores, Logs, and Coordinates

  • A capture scope is the set of tables or key ranges in one run, and its keys are stable logical row identities rather than scan-order values.A primary-key change is represented as absence for the old identity followed by a value for the new one.Source: §2 · p. 4, §2.1 · p. 4

2.1 Keyed stores and commit-ordered logs

  • The modeled log is a commit-ordered sequence of row events whose full images determine each key’s post-state, with deletes represented by absence.Only committed transactions contribute events; a theorem interpreted as a transactional snapshot additionally needs transaction closure.Source: §2.1 · p. 4

2.2 Mapping coordinates to log prefixes

  • Coordinates must map to nested log prefixes and their operational membership decisions must agree with that mapping.Coordinates that cannot faithfully represent commit-order prefixes fall outside the contract.Source: §2.2 · pp. 4–5

2.3 Windows and the cutoff discipline

  • A window is the ordered log slice (low, high], excluding events at the low edge and including those at the high edge.The half-open convention prevents boundary events from being duplicated across adjacent windows or omitted from both.Source: §2.3 · p. 5

2.4 What stays outside

  • The contract defines a mathematical replay meaning for the emitted sequence, not delivery semantics; transport, sink transactionality, and schema evolution remain outside scope.Each deployment must still name how relations and key ranges were enumerated and which coordinate binds that scope witness.Source: §2.4 · p. 5

3 Capture Plans and the Contract

A capture plan partitions the selected scope into units, assigns each a log bracket and a total refresh, and records a frontier. The contract states the source and plan conditions under which canonical replay matches source state and an implementation’s emitted stream can inherit that result.

3.1 Capture plans

  • Each capture unit owns a part of the scope and carries a bracket plus a total map assigning every owned key a value-or-absence refresh result.Units form the final partition; reads may come from scans, dumps, backups, or replicas, and need not be physically simultaneous.Source: §3.1 · pp. 5–6

3.2 What the source promises

  • The source must provide a commit-ordered keyed log of committed changes with sufficient row images, while capture must observe the events its merge discipline consumes.Delta logs require strengthening or a re-read normalization to supply effective full-image events.Source: §3.2 · p. 6

3.3 Capture plan requirements

  • The plan must partition the scope, provide a complete refresh, and ensure each key’s read matches source state at some coordinate inside its unit’s bracket.This per-key existential condition permits different keys to reflect different in-bracket coordinates; a single shared read coordinate is not required.Source: §3.3 · pp. 6–7
  • If no in-window event touches a key, its value is invariant across the bracket; a scan that silently misses a key cannot justify absence by omission.O2 and O3 require bracket-local validity and a total refresh, so absence-by-omission is sound only when the key is genuinely absent.Source: §3.3 · p. 7

3.4 Canonical replay and emission equivalence

  • Canonical replay places each refresh at the bracket’s low coordinate, then lets later log events override it through the frontier.A real merge discipline is admitted when its observed emitted stream replays to the same sink state as this canonical rule.Source: §3.4 · p. 7
  • For every plan satisfying the source-side contract, canonical replay at the frontier equals source row-event replay on every key, regardless of provenance, parallelism, or bracket width.Emission equivalence connects this canonical result to the stream an implementation actually emits.Source: §3.4 · pp. 7–8

4 The Cut Theorem and Its Corollaries

Section 4 establishes the canonical replay result for conforming capture plans and derives guarantees for earlier trajectories, continued observation, and composition. It also specifies when composites reach T2 or T3 and how bracket amortization preserves level as a cost optimization.

4.1 Window invariance and the theorem

  • A conforming plan’s canonical replay equals the source’s row-event replay state at the frontier on every key in scope.The proof uses window invariance: a key with no event in a bracket has the same value at every coordinate in it. The argument is local to one key and its covering unit, but calling the result a transactional snapshot requires transaction closure.Source: §4.1 · p. 8

4.2 A worked replay

  • The worked replay shows the log evicting a stale copied value, preserving a valid absence, and superseding an absence with a later event.For key a, an in-window event overrides the stale refresh; for key c, an event after the bracket but before the frontier supplies the final value.Source: §4.2 · p. 9

4.3 Per-key validity is strictly weaker than a single read point

  • Per-key validity within a bracket is strictly weaker than requiring one shared read coordinate for all keys, yet it suffices for the cut.A two-key instance has no coordinate consistent with both reads, while single-coordinate chunk reads satisfy the per-key condition; the read-only and parallel instances do not assume a shared point.Source: §4.3 · pp. 9–10

4.4 Corollary 1: a shared witness can move the canonical trajectory earlier

  • A shared state witness guarantees that canonical replay follows the source’s row-event replay from that coordinate, potentially earlier than the latest high edge.Without a shared witness, every nonempty plan still matches from its latest high edge; a closed unit is exact at any coordinate at or after its high edge. This is a retrospective canonical trajectory, not necessarily the physical sink’s consumed prefixes.Source: §4.4 · pp. 10–11

4.5 Corollary 2: continuation under extended observation

  • When observation continues from frontier f to f′, canonical replay equals the source state at f′, provided the capture keeps observing through f′.A stopped capture cannot recover events it no longer sees; the guarantee extends as far as observation and consumption continue.Source: §4.5 · p. 11

4.6 Corollary 3: mixing and composition guarantees

  • Two conforming plans on disjoint scopes at the same frontier compose into one conforming plan whose replay matches the source state across their union.The plans may mix capture methods, but composition alone supplies neither a shared-state anchor nor an earlier onset; a nonempty union still has the conservative trajectory from its latest high edge.Source: §4.6 · pp. 11–12
  • Every conforming composite reaches T2, and a nonempty combined unit family has a conservative trajectory, but composition alone promises neither a shared witness nor an earlier onset.A shared witness across all members establishes T3.Source: §4.6 · p. 12
  • Bracket sharing is unconstrained by the contract; amortizing one bracket across many reads with a shared state witness preserves level and is a pure cost optimization.One witness shared by all members establishes T3.Source: §4.6 · p. 12

5 Guarantee Levels and Certification

The framework separates replay guarantees from external certification and from operational cost choices. It identifies which evidence raises a configuration’s guarantee level, including for mixed bootstraps.

5.1 Four semantic levels and one certification overlay

  • T4 is an externally checkable certification overlay on T2 or T3, not a stronger replay guarantee.The levels describe replay and witness structure; certification is a separate dimension.Source: §5 · p. 12, §5.1 · p. 13, §5.2 · p. 14
  • T2 establishes per-key replay equivalence at the frontier, while T3 adds an exhibited shared-state witness that can move the trajectory start earlier.T3 does not imply simultaneous physical reads or correct emitted-stream prefixes; those require additional conditions.Source: §5.1 · p. 13

5.2 What changes a level, and what does not

  • A configuration reaches T2 only when contract obligations and the merge discipline’s equivalence obligation are established; a shared-state witness distinguishes T3.Operational choices such as parallelism, chunk size, and bracket width affect cost, not theorem strength, when the required conditions hold.Source: §5.2 · p. 14

5.3 Reading the levels on a mixed bootstrap

  • A mixed bootstrap can reach T2 across its union even when individually T3 table dumps use distinct coordinates; a shared snapshot can restore a witness for the dumped scope.The scanned table may still join the union at T2.Source: §5.3 · p. 14

5.4 T0 in the wild

  • Polling by updated_at is T0 because it can miss deletes and its timestamps do not faithfully map to commit-order prefixes.Either failure is independently disqualifying; widening the bracket does not repair it.Source: §5.4 · p. 14

6 Merge Semantics

This section defines how emitted streams are replayed and proves that concrete merge disciplines can match the canonical result. It also distinguishes established disciplines from additional open designs.

6.1 Streams and their replay

  • A finite emitted stream replays from an empty state, with each key’s last entry deciding its value and omission representing absence.The final replay result does not by itself establish physical-prefix correctness, transport or delivery, or application to a populated sink.Source: §6.1 · pp. 14–15

6.2 Window-discard

  • Window-discard emits log events in commit order and closes units by emitting surviving refresh rows; its replay equals the canonical replay and its per-key event tags are non-decreasing.The log wins for keys with in-window events, while a surviving refresh is emitted after earlier events for its key.Source: §6.2 · pp. 15–16

6.3 Buffered range-merge

  • Range-merge replays to the canonical result when its two clauses hold, and needs only log observation from the unit’s high edge because window contents enter through the buffer.The merged entry represents the key’s value or absence at the high edge.Source: §6.3 · p. 16
  • Withholding every event at or before a unit’s high edge is necessary: narrowing withholding to the buffered window can replay a deleted value.In the two-event counterexample, an insert passes through while the in-window delete is absorbed, leaving the key present downstream.Source: §6.3 · p. 17

6.4 Point-splice

  • Point-splice is the empty-window case of window-discard, and composites with distinct splice coordinates must begin by the earliest splice.Its replay is equivalent after replay, not entry-for-entry identical.Source: §6.4 · p. 17

6.5 Analyzed and open

  • Four further disciplines remain open: key-range gating, version-max, re-read normalization, and rewind-by-preimage.Their obligations include monotone fresh reads, commit-ordered versions with delete evidence, termination of re-reads, and reconstructing the low-edge state by reversing a suffix.Source: §6.5 · pp. 17–18

7 Instantiating the Contract

The section maps production protocol shapes—including Debezium and Flink CDC, coordinate-bound reads, and native dumps—to the contract, distinguishing plan guarantees from emitted-stream guarantees under explicit assumptions. It identifies where replay guarantees hold, where evidence leaves gaps or limits claims, and how native dumps can support T3 or T2 contracts.

7.1 How a protocol inherits the theorem

  • A protocol inherits the theorem by mapping coordinates to nested log prefixes, mapping reads and brackets to a capture plan, and proving its source and plan obligations.The proof then matches emitted output to a proved discipline or establishes an additional equivalence condition; shared-state-witness claims require that witness.Source: §7.1 · p. 18

7.2 What an instantiation establishes

  • A contract proof establishes the canonical frontier result, but an emitted stream needs a separate merge-equivalence argument, and T3 does not describe every physical stream prefix.T3 concerns the retrospective canonical family and an exhibited common state witness; transaction closure is needed to interpret results as transactional snapshots or histories.Source: §7.2 · p. 18

7.3 Classic watermarked DBLog

  • Every wellformed classic DBLog run [6] instantiates the contract, and its canonical replay at the frontier equals the source’s per-key latest-event state there.The result includes the initial value when no event for a key occurs at or before the frontier; the imported plan is T2.Source: §7.3 · pp. 18–20
  • On PostgreSQL, a snapshot can omit a transaction already logged before the low watermark, causing stale copied rows or resurrection; snapshot comparison can widen the bracket to restore O2.The snapshot comparison relies on stated conditions, including compatible transaction-ID spaces and per-key read consistency; the paper assumes rather than derives the latter.Source: §7.3 · p. 20
  • Debezium’s signal-table insert_insert mode has the classic span-bracket and log-wins shape, yielding T2 and conditionally emitted final replay when its stated capture and read conditions hold.For PostgreSQL signal-table mode, the argument uses snapshot comparison in place of W6; insert_delete also requires the delete before-image to preserve the opening row’s identifier.Source: §7.3 · pp. 20–21

7.4 Debezium read-only capture: MySQL, MariaDB, and PostgreSQL

  • Transaction-complete executed-set samples faithfully select the half-open log window, enabling a read-only Debezium plan to attain T2 and, conditionally, emitted final source replay.The samples must correspond to gap-free prefixes ending between complete transaction blocks; emission additionally requires A-discard and window-discard S-OBS.Source: §7.4 · pp. 21–22
  • Under their respective bridges and shared assumptions, the MySQL set plan, two MariaDB cases, and PostgreSQL plan are T2, with final replay equality conditional on lifecycle, observation, and emission equivalence.The MariaDB cases are an empty difference (point splice) and an empty buffer with a nonempty difference (window-discard); a populated buffer with a nonempty difference remains unanalyzed.Source: §7.4 · p. 23

7.5 Flink CDC parallel chunks

  • Flink CDC parallel-chunk plans satisfy T2 under plan conditions, and their finite emitted streams have final source replay equality under additional window, merge, observation, and handoff conditions.Chunk brackets may overlap or nest without a pairwise ordering assumption, though connector coordination and the global handoff and gate remain necessary; skipping backfill has no T2 mapping here.Source: §7.5 · pp. 24–25

7.6 Coordinate-bound reads: LSNs, binlog positions, and consistent points

  • A consistent read bound to a recorded log coordinate gives a point-splice plan at T3 on its captured scope; per-table splices at distinct coordinates compose to global T2, not a shared-state witness.The analyzed examples include MariaDB and Percona binlog snapshot coordinates and PostgreSQL replication-slot snapshots; final replay equality for finite output remains conditional on scope and observation assumptions.Source: §7.6 · pp. 25–26

7.7 Native dumps and uncertainty intervals

  • Native mysqldump, mariadb-dump, and pg_dump instances use a recorded coordinate as a point splice, with no closing marker for the dump.The point bindings are trusted assumptions, and the stated consistency scope excludes non-InnoDB tables for mysqldump.Source: §7.7 · pp. 26–27
  • When the restored scope equals one source state at unknown v and recorded bounds establish b⊑v⊑e, widening the bracket to (b,e) satisfies the contract at T2 and yields a canonical trajectory from e.The theorem requires the whole restored dataset in scope to correspond to that single view; the trusted point is the degenerate case b=v=e=r.Source: §7.7 · pp. 27–28
  • Final replay through f equals the canonical sink only with an exact survivor listing, consumption starting by b, ordered scoped-log observation through f, and closure at e after processing events through e.This guarantees equality after replay, not prefix equivalence of the emitted stream.Source: §7.7 · pp. 27–28
  • A native dump with a trusted point reaches T3 when its engine, scope, DDL, and dump/log representation conditions hold.The dump’s recorded coordinate binds its enumerated relations and key ranges; representation agreement between dump and log paths must be established.Source: §7.7 · pp. 27–28
  • Without a trusted point or justified interval, this placement does not apply; an interval costs reconciliation across (b,e) but preserves frontier equivalence and the post-e canonical trajectory.For example, window-discard buffers a restored value, discards it when an in-window update appears, and lets the update through.Source: §7.7 · p. 28

8 Generalized DBLog at a Glance

Generalized DBLog is a correctness contract for combining copied rows with a live change log. When its conditions hold, replay reconstructs source state at a shared log position across the captured scope, even when units were read at different times.

8.1 What Generalized DBLog is

  • Once all units close, replay matches source-log state key by key at a shared observation frontier, without requiring a global database snapshot.Later logged changes continue to advance the reconstructed state; no claim is made yet for keys in open units.Source: §8.1 · p. 28

8.2 What the datastore and change log must provide

  • Datastores must provide commit-ordered complete events, precise log positions, stable row identities, full after-images, complete committed reads, and sufficient log retention.Primary-key changes are modeled as deleting the old identity and inserting the new one; sortable keys are needed only for ordered chunk scans.Source: §8.2 · pp. 29–30

8.3 What the connector must establish

  • Connectors must partition scope without gaps or overlaps, bracket each read, preserve row operations, let log events win, and reconcile the full window before closing a unit.The emitted stream need only replay to the same final per-key state as the source log, not reproduce its events one for one.Source: §8.3 · p. 30

8.4 How to read the observation frontier

  • The frontier guarantees exact row-event replay; it guarantees a transactional snapshot only when it lands on a transaction boundary.Individual downstream event application may still expose intermediate states to sink readers.Source: §8.4 · pp. 30–31

8.5 How the protocol families fit

  • Window-discard, range-merge, and point splice all yield source-log-equivalent final state under the baseline conditions.Point splice is the zero-width bracket case; multiple-table splices must start log streaming at or before the earliest recorded coordinate.Source: §8.5 · p. 31

8.6 Conditions for the named protocols

  • The analyzed DBLog, Debezium, and Flink CDC designs fit the contract only under their stated datastore and implementation conditions.Flink’s parallel splits require immutable split keys; classic DBLog requires recognizable watermark events and a complete chunk scan.Source: §8.6 · pp. 31–32
  • Debezium read-only variants require valid sampled log prefixes, while bounded physical restores guarantee live-source tracking from the backup’s high bound onward.The analyzed MariaDB bridge does not cover a populated buffer with a nonempty GTID difference.Source: §8.6 · pp. 31–33

8.7 Retention, restart, and failover guidance

  • Recovery guidance requires retaining logs for open work, coordinating checkpoints with buffers and gates, and verifying coordinate continuity after failover; it is not a proved lifecycle protocol.If required history or coordinate continuity cannot be guaranteed, the guidance calls for failing closed and rebuilding affected units.Source: §8.7 · p. 33

9 Making the 2020 Requirements Explicit

The paper makes explicit that correct capture requires both complete reads and mechanism-specific handoff conditions. This clarifies why the original DBLog requirements were underspecified while preserving watermarking as one valid way to construct brackets.

9 Making the 2020 Requirements Explicit

  • The 2020 DBLog requirements omitted scan completeness and several watermark preconditions, which the generalized contract states explicitly [1].Freshness alone cannot guarantee that a scan returns every unchanged row.Source: §9 · p. 33, §9.1 · p. 34

9.1 Read completeness

  • The original paper’s single-coordinate read condition is stronger than its portability criterion of non-stale reads, and the two are not equivalent [1].A PostgreSQL primary can meet the plain non-stale reading condition yet violate the log-order requirement W6.Source: §9.1 · pp. 33–34
  • O2 and O3 together require every key that remains present throughout a bracket to be returned with a valid value.A silently skipped unchanged row has no log event to restore it, so the sink can remain missing it.Source: §9.1 · pp. 33–34

9.2 Watermark preconditions

  • Watermark writes are preconditions of that bracket mechanism, not universal CDC requirements; write-free mechanisms can satisfy the same contract obligations.W1–W5 formalize requirements already implicit in the original mechanism, while W6 captures its log-order read condition.Source: §9.2 · p. 34

10 Mechanization

The paper supports its generalized contract with machine-checked proofs, an independent Lean re-proof of central results, and bounded protocol models. The mechanizations cover different scopes, and the bounded checks complement rather than replace the general proof.

10 Mechanization

  • The Isabelle/HOL development machine-checks the normalized mathematical content of every numbered definition and result, in about 5,000 lines.Coordinate fidelity, raw representation agreement, and connector-release conformance remain instance evidence outside the prover.Source: §10 · pp. 34–35
  • The PostgreSQL argument in §7.3, including its snapshot comparison, is not mechanized.The general Isabelle development covers the normalized numbered results, but this specific instance argument is given in prose.Source: §10 · pp. 34–35
  • The proof effort concentrates on emission equivalences and countermodels rather than the per-key cut argument itself.Buffering disciplines account for roughly a third of development lines, more than the contract and cut theorem together.Source: §10 · p. 35
  • Five TLA+ models checked protocol behavior across 25 bounded runs, including frontier replay, monotonicity, degradation, and mixed composition.These bounded checks do not establish the general result, which comes from the machine-checked proof.Source: §10 · p. 35
  • Lean 4 independently re-proves the contract core, cut theorem, three corollaries, and the no-shared-read-point instance of Proposition 1.It is not a port of every placement or merge.Source: §10 · pp. 35–36

11 Related Work

The paper relates its contract to database recovery, online schema changes, and other list-copy-and-resume protocols, while distinguishing specification proofs from implementation verification. It also identifies earlier work that supplies its virtual-cut foundation and separates delivery-side concerns.

12 Related Work

  • ARIES and Generalized DBLog both reconcile state with ordered history, but address different problems: ARIES uses page LSNs and transaction undo, while DBLog uses committed row states and full post-images.DBLog's O2 condition requires bracket-local validity without recording a version for each copied component.Source: §11 · p. 36
  • Online schema-change tools copy into a ghost table and reconcile concurrent changes through binary-log capture or triggers before cut-over.Whether either tool satisfies the paper's equivalence obligation is left open; trigger forwarding is not a commit-ordered log and needs a separate admissibility argument.Source: §11 · p. 36
  • Kubernetes list-then-watch and PostgreSQL tablesync and Vitess key-range copying share the copy-coordinate-handoff shape, but their equivalence obligations are not all established here [49,18,50].Kubernetes re-lists after 410 Gone; PostgreSQL's per-table workers compose under Proposition 2, while Vitess's key-range discipline remains an open obligation.Source: §11 · p. 36
  • Generalized DBLog verifies a contract and conditional protocol placements, not an implementation, distinguishing its approach from verified implementations and bounded exploration of formal specifications.The paper compares its method to specification frameworks that characterize guarantees through what clients can observe.Source: §11 · p. 36
  • The paper builds on a predecessor's certified virtual-cut object [6], leaves sink recovery and acceptance to delivery-side work [17], and completes the 2020 operational requirements in its framework [1].The replayed row-event state in Theorem 6 matches the earlier formalization.Source: §11 · p. 36

12 Scope and Limitations

The formal guarantee concerns reconstructing source state from the emitted stream under explicit source and connector conditions. Its scope excludes several sink, lifecycle, and connector behaviors, and some protocol paths remain conditional or open.

12 Scope and Limitations

  • The capture contract proves that replaying the emitted stream from an empty state reconstructs the source database, but does not itself guarantee repair of an already populated sink.A source-deleted row can remain unless the target scope is cleared first or explicit tombstones are emitted.Source: §12 · pp. 36–37
  • Populated-sink repair, transport, duplicate delivery, exactly-once application, schema evolution, checkpointing, restart, rescaling, and failover are outside the formal proofs.Operational guidance preserves invariants but is not a verified lifecycle result; resumed runs qualify only if recovered plans and outputs again satisfy the same conditions. The analysis evaluates protocol designs based on Debezium 3.6 documentation and Debezium 3.6.1.Final and Flink CDC 3.6.0 source code, not certified releases.Source: §12 · p. 37
  • Table and key-range discovery must itself correspond to a valid log coordinate, and MariaDB point-splice snapshot coordinates must be queried from the exact session holding the snapshot.For native dumps, scope enumeration is bound directly to the tool's recorded server-wide snapshot position.Source: §12 · pp. 37–38
  • Debezium signal-table bridges require ordered window-edge events, complete reads, correct buffering and release, gap-free observation, and valid signaling-collection conditions; no release is verified by the bridge.For insert_delete, the deletion closes the window only if its before-image retains the signal-row identifier.Source: §12 · p. 37
  • Debezium read-only bridges rely on exact-prefix assumptions for MySQL and PostgreSQL, while the MariaDB analysis leaves populated-buffer cases with a nonempty GTID difference unresolved.MySQL requires accepted GTID sets to map to gap-free transaction prefixes; PostgreSQL's primary guarantees neither required prefix condition. MariaDB's result covers quiet-point and empty-buffer cases, not every tagged implementation path.Source: §12 · p. 37
  • Flink CDC's parallel-chunk mapping requires complete reads, retained logs, faithful high-watermark merging, per-split gating, complete event observation, and stable non-primary split keys when used.Append-only output requires an explicit normalization proof; checkpointing, failover, and several other runtime behaviors are excluded. Complete chunk scanning is an explicit precondition, not implied by an isolation-level label such as READ COMMITTED.Source: §12 · pp. 37–38
  • An uncertain restore must be an engine-consistent source state at some coordinate within recorded log bounds; tracking the live source is guaranteed only from the known high bound onward.Torn or inconsistent copies assembled from reads at different times are outside this theorem.Source: §12 · p. 38
  • Equivalence theorems remain open for key-range gating, version-max, re-read normalization, and rewind-by-preimage, despite defined proof obligations.The open designs are analyzed in the model but not fully proved equivalent.Source: §12 · p. 38

13 Conclusion

Generalized DBLog makes the conditions for copy-and-log reconciliation explicit and proves the contract for several capture designs. Its composition result permits different methods across tables or key ranges, while delivery and recovery remain separate verification concerns.

13 Conclusion

  • The framework states which properties must come from the source and which from the connector, providing a common contract for assessing new copy methods.Its central requirement is correct reconstruction of selected data after copying and reconciliation finish.Source: §13 · p. 38
  • The contract is proved for classic watermarking, Debezium signal-table and MySQL and PostgreSQL read-only protocols, and Flink CDC parallel chunks; native dumps and bounded-position backups also satisfy it.The PostgreSQL proofs require further conditions, and the MariaDB read-only proof covers quiet-point and empty-buffer cases but leaves populated-buffer cases with a nonempty GTID difference open.Source: §13 · p. 38
  • Read-only capture must identify overlapping changes, parallel capture must preserve key ownership and prevent stale reversion, and native dumps must align their log position and decoded keys and values.Chunk size and parallelism can be selected around source load, buffering, and retention limits while preserving these requirements.Source: §13 · p. 38
  • Different capture methods can be composed across tables or key ranges when each establishes its handoff to the same source history and their assigned keys do not overlap.For example, one table can use a native dump while another uses chunked reads.Source: §13 · p. 38
  • The machine-checked proofs provide reusable support for extensions and combinations, while delivery, crash recovery, and downstream application require separate verification.The contract gives maintainers and connector authors a basis for checking or changing capture paths while preserving copied-row and change handling.Source: §13 · p. 38

AI assistance disclosure

The author reports using AI tools to assist with theory, formalization, modeling, and prose drafting, while taking responsibility for the paper's content and conclusions.

AI assistance disclosure

  • Claude Fable 5, ChatGPT 5.5 and 5.6 Sol, and GPT 6 Astra assisted with theory, Isabelle/HOL and Lean formalizations, TLA+ models, and drafting; the author edited the prose and takes responsibility for the conclusions.The disclosure does not assign responsibility for the paper's content to the tools.Source: AI assistance disclosure · p. 39
Loading 2609.08160v4…