기술 요약: 커밋된 로그로부터의 머신 검증된 이중 쓰기 복구 (Machine-Checked Dual-Write Recovery from a Committed Log)

문제 정의

본 논문은 "이중 쓰기(dual-write)" 시나리오에 내재된 근본적인 불확실성을 다룬다: 프로세스가 소스 데이터베이스에 사실(fact)을 커밋한 후, 이어서 싱크(sink, 예: 이메일 전송, 브로커로 메시지 발행, 캐시 업데이트)에 효과(effect)를 전달하려고 시도하는 상황이다. 만약 프로세스가 전송 작업과 그 전송 기록(체크포인트) 사이에서 충돌(crash)한다면, 복구 프로세스는 자신의 로컬 상태만을 사용하여 다음과 같은 해결 불가능한 질문에 직면하게 된다: "싱크가 이미 효과를 수락했는가?"

본 논문은 기존의 운영 지침(재시도, 멱등성 키, 페이싱 등)이 대체로 타당하지만, 그것이 언제 작동하는지에 대한 정밀한 형식적 설명을 결여하고 있다고 주장한다. 구체적으로, 기존 문헌은 다음 사항들을 엄격하게 정의하지 못했다:

1. 보장(guarantee)이 참조하는 정확한 이벤트는 무엇인가?
2. 복구 결정을 내리는 데 필요한 구체적인 증거는 무엇인가?
3. 그 증거의 유효 기간(lifetime)은 얼마인가?

핵심 문제는 **정보 경계(information bound)**이다: 충돌 발생 후 도달 가능한 두 가지 포스트 크래시(post-crash) 상태는 충돌 측의 관점(데이터베이스, 쓰기 로그, 체크포인트 포함)에서는 바이트 단위로 동일할 수 있지만, 싱크가 효과를 수락했는지 여부는 다를 수 있다. 결과적으로, 충돌한 측의 내구적 상태(durable state)에만 의존하는 모든 복구 정책은 효과를 중복 전달하거나 커밋된 작업을 포기해야 하는 선택에 직면한다.

방법론

본 논문은 Isabelle/HOL을 이용한 **형식 검증(formal verification)**을 사용하여 머신 검증된 이중 쓰기 복구 이론을 구축한다. 방법론은 다음과 같이 점진적으로 복잡해지는 일련의 상태 머신(substrates)을 모델링하는 과정을 포함한다:

• 효과 머신 (Effect Machine): 소스 히스토리와 싱크 레저(ledger) 사이의 핵심 상호작용을 모델링한다.
• 체크포인트 머신 (Checkpointed Machine): "전달 후 체크포인트(deliver-then-checkpoint)" 프로토콜을 모델링하기 위해 내구적 진행 커서(durable progress cursor)를 추가한다.
• 채널 머신 (Channel Machine): 인플라이트 메시지(in-flight messages, stragglers)와 도착 펜스(arrival fences)를 모델링하기 위해 "와이어(wire)"를 도입한다.
• 동시성 머신 (Concurrency Machine): 여러 개의 동시 복구 프로세스와 클레임 펜스(claim fences)를 모델링한다.
• 스토어 티어 모델 (Store Tier Model): CDC(Change Data Capture)/아웃박스 패턴과 소스 로그 간의 관계를 형식화한다.

증명 전략: 본 논문은 특정 클래스의 정책을 무력화하는 도달 가능한 상태를 구성하는 **부정적 결과(negative results)**와 특정 전제 조건 하에서 정확성을 증명하는 **긍정적 결과(positive results)**를 혼합하여 활용한다.

머신 검증 (Machine-Checking): 모든 정리, 정의 및 증명은 Isabelle/HOL에서 검증된다. 신뢰 기반(trusted base)은 최소한의 표준 라이브러리 이론들로 구성되어, 결과가 휴리스틱이 아닌 연역적임을 보장한다.

주요 기여 및 결과

1. 정보 경계 (정리 1–3)

본 논문은 충돌한 측의 내구적 상태(스토어, 컨트롤 플레인 또는 체크포인트)에만 의존하는 복구 정책은 정확히 한 번(exactly-once) 전달를 달성할 수 없음을 증명한다.

• 정리 1 (관측 경계): 코어 스토어와 생성(generation)이 동일하지만 싱크의 수락 기록이 서로 다른 두 가지 도달 가능한 상태를 구성한다. 코어만을 관찰하는 정책은 한 세계에서는 중복을, 다른 세계에서는 손실을 일으키는 배치를 선택할 수밖에 없다.
• 정리 3 (체크포인트 딜레마): 결정론적인 "전달 후 영속화(deliver-then-persist)" 프로토콜과 내구적 커서를 사용하더라도, 전달과 영속화 사이의 윈도우에서 충돌이 발생하면 로컬 뷰에서는 구별 불가능하면서도 서로 반대되는 복구 동작을 요구하는 두 상태가 생성된다. 커서 자체로는 이 딜레마를 해결할 수 없다. 딜레마는 커서의 정확도가 아니라 그 '윈도우'에 있다.

2. 싱크 읽기를 통한 탈출 (정리 4)

본 논문은 필수적인 탈출구를 식별한다: 싱크의 **내구적이고 연산별로 기록된 수락 기록(durable, per-operation accepted record)**을 읽는 것이다.

• 정리 4 (싱크 읽기 탈출): 복구 프로세스가 싱크의 권위 있는 수락 기록을 읽을 수 있다면, "델타(committed obligations minus accepted records)"를 계산하여 누락된 작업만을 정확히 다시 실행할 수 있다. 이는 네 가지 전제 조건(기록이 해저드 프리(hazard-free)이고, 실행 중 충돌이 발생했으며, 프런티어가 범위 내에 있고, 소스 좌표가 엄격하게 상승함) 하에서 정확하다.

3. 스트래글러 처리: 도착 펜스 (정리 5–6)

싱크를 읽는 것만으로는 부족하다. 충돌한 인카네이션(incarnation)에서 온 오래된 메시지(stragglers)가 여전히 인플라이트(in-flight) 상태일 수 있기 때문이다.

• 정리 5 (와이어 경계): 싱크를 읽더라도 와이어(인플라이트 메시지)를 무시하는 정책은, 읽기 이후에 스트래글러가 도착하여 중복을 유발하는 스케줄에 의해 무력화된다.
• 정리 6 (도착 펜스): 해결책은 **원자적 펜싱 재구동(atomic fenced re-drive)**이다: 스토어를 치유하고, 델타를 계산하고, 배치를 착륙(land)시킨 다음, 동시에 충돌 시점의 다음 세대(successor)에 대한 생성 펜스를 올린다. 이 펜스는 폐기된 인카네션으로부터 오는 후속 도착을 싱크가 거부하도록 만든다.
• 코롤러리 6.1: 본 논문은 이 펜스의 비용을 증명한다: 이는 "구조(rescue)"(스트래글러가 손실된 것으로 생각되었던 작업을 완료하는 것)의 가능성을 "프런티어의 확실성(certainty at the chosen frontier)"과 교환하는 것이다.

4. 동시 복구 프로세스 처리: 클레임 펜스 (정리 7–8)

여러 복구 프로세스가 동시에 시작될 때(예: 오케스트레이터 실패 시) 경합이 발생할 수 있다.

• 정리 7 (두 번째 복구자 경계): 각각 싱크를 읽고 델타를 계산하는 두 명의 정직한 복구자가 조정 없이 실행되면, 중복이나 손실을 초래하며 모두 실행될 수 있다.
• 정리 8 (완료된 클레임의 정확성): 해결책은 **원자적 클레임 디시플린(atomic claim discipline)**이다: 복구자는 자신의 생성(generation)에 대한 펜스를 원자적으로 설정하고 그 클레임 하에 배치를 준비해야 한다. 펜스가 해당 배치를 허용할 때 실행된 배치만이 수락된다. 이는 복구 시도를 직렬화한다.

5. 증거의 수명 및 절단 (정리 9–10)

본 논문은 정확히 한 번 전달를 위한 증거가 얼마나 오래 지속되는지 분석한다.

• 정리 9: "정확히 한 번"은 중복 제거 메모리가 **영구적(permanent)**일 때만 "적어도 한 번"과 동등함을 증명한다. 중복 제거 윈도우가 만료되면 그 보장은 무효화된다.
• 정리 10 (절단 딜레마): 소스 히스토리가 절단(예: 로그 압축)되어 저널 내용(journal content)은 사라지고 메타데이터(길이)만 남은 경우, 복구 프로세스는 "이미 수행된 작업"과 "수행되지 않은 작업"을 구분할 수 없다. 이는 작업을 조작하거나 작업을 포기해야 하는 선택을 강요한다.

6. 스토어 티어 충실성 (정리 11)

본 논문은 "아웃박스 패턴"과 CDC를 형식적으로 검증한다.

• 정리 11: 스토어 티어에서 충돌 안전성은 다운스트림의 파생 이미지(derived image)를 커밋된 로그에 충실하게 유지하는 것과 동등함을 증명한다. 그러나 이는 스토어 티어의 일관성만을 해결할 뿐이며, 전달 루프 자체는 여다면 위에서 설명한 메커니즘을 요구하는 이중 쓰기 문제로 남아 있음을 명확히 한다.

의의 및 주장

본 논문은 이중 쓰기 복구에 대한 최초의 머신 검증된 연역적 설명을 제공한다고 주장한다. 그 의의는 다음과 같다:

1. 구호(Slogan)를 넘어서는 정밀함: "정확히 한 번은 불가능하다"거나 "그냥 싱크를 읽어라"와 같은 휴리스틱을 넘어, 정확히 한 번이 달성 가능한 정확한 조건(전제)을 정의한다.
2. 경계의 형식화: 스토어 중심의 추론이 실패하고 싱크 중심의 추론이 필요한 "수락 경계(acceptance boundary)"를 격리한다.
3. 보장의 비용: 안전 메커니즘의 비용(예: 펜싱에서의 스트래글러 구조와 프런티어 확실성 간의 트레이드오프)을 명시적으로 증명한다.
4. 운영적 규율: 실무자를 위한 설계 체크리스트를 제공한다:
   • 싱크의 내구적 수락 기록을 식별하라.
   • 해당 기록이 권위 있고 최신 상태인지 확인하라.
   • 스트래글러와 동시 복구자를 위해 생성 기반 펜싱을 사용하라.
   • 중복 제거 윈도우와 저널 보유 기간을 최대 예상 장애 기간보다 길게 설정하라.
   • 누락(omissions)을 중복(duplicates)과 별도로 모니터링하라.

본 논문은 특정 배포 시스템(Kafka나 Flink 등)을 검증하는 것이 아니라, 그러한 시스템의 보장을 평가하기 위한 이론적 프레임워크를 제공하는 것을 목적으로 한다. 서론에서 언급된 "중복 이메일" 사건은 체크포인팅 로직의 버그가 아니라, 복구 프로세스가 가용할 수 있는 정보의 구조적 한계였으며, 이는 싱크의 수락 상태를 쿼리함으로써만 해결 가능하다는 점을 강조한다.