Repository navigation
fix(#1379): spec + formal verification + harden snapshot completion / control-record offset commit - #1467
Merged
Conversation
…ol-record offset commit Issue #1379 ("Initial Snapshot never finishes"): a snapshot completed state rides only on a post-snapshot control record (heartbeat / tx boundary) that produces no ClickHouse row. If that record offset is never committed, snapshot_completed=false is persisted and every restart re-runs the whole snapshot. Root cause was a NPE calling setSequenceNumber on the null parsed struct, and dropping null-producing records without acknowledging them. The NPE null-skip and commitControlRecordOffset quiescence gate already landed in 2.11.0. This change defines the flow properly (spec + formal verification), hardens the remaining offset-progress gap, and proves the guarantees. Formal verification (formal_specs/lean/Replication/Snapshot.lean), no sorry, axioms [propext, Quot.sound] only: - control_commit_safe: a control record advances the committed offset ONLY when the pipeline is quiescent (outstanding = 0) - never past unwritten rows (safety, no #1285 data loss). - quiescent_control_commits: a control record on a quiescent pipeline commits its offset (liveness). - snapshot_completes: after the snapshot rows are handed off and written, the end-of-snapshot control record commits its offset (committed = snapPos) - so snapshot_completed persists and a restart does not re-run the snapshot. Code hardening (DebeziumChangeEventCapture): add markTerminalRecord and call it before every handoff so each handed-off batch carries a terminal record. Without it, a Debezium batch that ends with a control record (or is split ahead of a DDL) leaves no row flagged isLastRecordInBatch, acknowledgeRecords never calls markBatchFinished, and that batch offset is only committed by a later heartbeat - delaying, and on an idle source stranding, snapshot-completion progress. Offset progress is now independent of where control records fall in a Debezium batch. Tests: SnapshotOffsetProgressTest (markTerminalRecord flags exactly the last row; safe on empty/null). Mutation-checked: a no-op helper fails the test. Governance: add Invariant I12 (Snapshot Completion & Control-Record Offset Progress) to CONSTITUTION.md, rewrite spec 01.06 to cover both safety and the #1379 liveness, wire Snapshot.lean into the lakefile roots and the validate_specs.py Lean module + no-sorry gate, and document the theorems in the Lean README.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem (#1379 "Initial Snapshot never finishes")
A snapshot completed state rides only on a post-snapshot control record (heartbeat / transaction boundary) that produces no ClickHouse row. If that record offset is never committed, snapshot_completed=false is persisted and every restart re-runs the whole snapshot. Root cause: a NullPointerException calling setSequenceNumber on the null parsed struct every heartbeat cycle, and dropping null-producing records without acknowledging their offset.
The NPE null-skip and the commitControlRecordOffset quiescence gate already landed in 2.11.0. This PR defines the flow properly (spec + formal verification), hardens the remaining offset-progress gap, and proves the guarantees.
Formal verification (formal_specs/lean/Replication/Snapshot.lean)
No sorry; every theorem depends only on [propext, Quot.sound] (verified via #print axioms):
Code hardening (DebeziumChangeEventCapture)
Add markTerminalRecord and call it before every handoff so each handed-off batch carries a terminal record. Without it, a Debezium batch that ends with a control record (or is split ahead of a DDL) leaves no row flagged isLastRecordInBatch, acknowledgeRecords never calls markBatchFinished, and that batch offset is only committed by a later heartbeat - delaying, and on an idle source stranding, snapshot-completion progress. Offset progress is now independent of where control records fall in a Debezium batch.
Tests
SnapshotOffsetProgressTest: markTerminalRecord flags exactly the last row; safe on empty/null. Mutation-checked: a no-op helper fails the test. Existing NullParsedRecordSkipTest / ControlRecordOffsetCommitTest still cover the null-skip and quiescence gate.
Governance
Adds Invariant I12 (Snapshot Completion and Control-Record Offset Progress) to CONSTITUTION.md, rewrites spec 01.06 to cover both safety and the #1379 liveness, wires Snapshot.lean into the lakefile roots and the validate_specs.py Lean module + no-sorry gate, and documents the theorems in the Lean README. Built/checked with Lean 4.11.0 and JDK 17.