Why DBLog Is Snapshot-Equivalent

Author: Andreas Andreakis (DBLog 저자) | Source: aandreakis.com | Published: 2026-06-05

한 줄 요약

Netflix DBLog(CDC 프레임워크)가 테이블을 락 없이·동결 없이 chunk로 백필하면서도, 결과가 단일 시점에 찍은 스냅샷과 동일함(“snapshot-equivalent”)을 Isabelle/HOL로 기계 검증한 이론적 직관.

DBLog는 row-level 변경을 스트리밍하면서 테이블 기존 행을 chunk로 추출(락 없음, 긴 read transaction 없음, write 중단 없음). Debezium·Flink CDC incremental snapshot이 이 접근 채택
의심스러운 주장: 라이브 테이블을 동결 없이 백필하는데, 결과가 단일 시점 스냅샷과 구별 불가(스냅샷은 결코 찍지 않음). chunk 1과 chunk 2가 다른 순간에 읽혀 underlying 데이터가 다름에도
단 하나의 규칙 — latest-event-wins per key: chunk refresh(키 k가 v로 관찰됨, 로그 위치)와 CDC event(커밋된 변경)를 로그 순서로 interleave → replay 시 키별로 최신 이벤트가 이김
stale read의 치유: chunk가 Bob=100을 읽은 후 write로 120이 되면, frontier를 c2로 밀고 CDC event(Bob=120)가 stale refresh(100)를 덮어씀. “chunk read는 그 순간의 첫 추측일 뿐, 로그가 교정”
핵심 통찰: read 좌표는 local(키별, 다른 시간), cut point frontier f는 global(모든 키에 하나), 변경 로그가 둘 사이의 lift. 키의 f 이전 마지막 이벤트가 정의상 f에서의 값. 등식은 시간이 아닌 outcome-space에서 성립
전제: chunk가 K를 커버, 각 chunk read는 한 로그 위치, 모든 read는 f 이하, 로그가 read~f의 모든 변경을 충실히 운반

핵심 결과: replay output ↾ K = database state at f ↾ K (scope 키 한정, whole-table은 별개의 더 어려운 결과)
“virtual cut” 개념을 paper(arXiv:2605.31475)에서 명명, Isabelle/HOL 기계 검증
delete도 같은 규칙(“absent”가 최신 이벤트의 한 상태). “snapshotless ≠ uncoordinated — 조율이 로그로 이동”