MongoDB 분산 트랜잭션 프로토콜이 어떻게 동작하는지, TLA+ 기반의 합성적 명세로 격리성 보장을 검증한 방법, 그리고 프로토콜의 동시성 허용 정도를 정량화하는 ‘허용성(permissiveness)’ 지표를 소개합니다.
MongoDB는 2019년부터 분산 다중 문서 트랜잭션을 지원해 왔으며, 스냅샷 격리(snapshhot isolation) 수준에서 ACID를 만족하는 샤드 간(cross-shard) 트랜잭션을 가능하게 합니다. 이 글에서는 MongoDB에서 분산 트랜잭션 프로토콜이 어떻게 동작하는지 살펴보고, 트랜잭션 프로토콜을 더 깊이 검토하기 위해 우리가 최근 수행한 형식 모델링 및 검증 작업을 논의합니다.
여기에는 MongoDB 트랜잭션 프로토콜을 위한 합성적(compositional) TLA+ 명세 개발 작업이 포함되며, 이를 통해 고수준의 격리성 정확성 보장을 정의하고 점검할 수 있었습니다. 또한 이러한 명세를 통해 분산 트랜잭션 프로토콜과 기반 키-값 저장 엔진인 WiredTiger 사이의 인터페이스 경계를 형식화할 수 있었고, 계층을 가로지르는 복잡한 시스템 상호작용에 대해 엄밀한 보증을 제공할 수 있었습니다.
프로토콜 정확성 점검에 이러한 명세를 사용하는 방법을 개략적으로 설명하는 것에 더해, 트랜잭션 프로토콜의 허용성(permissiveness) 을 측정하는 새로운 정량적 접근도 다룹니다. 허용성은 특정 격리 수준을 구현할 때 프로토콜이 얼마나 제약적(restrictive)인지 계산 가능한 지표로 나타내는 것입니다. 이는 프로토콜 분석의 새로운 차원입니다. 단지 ‘옳다/그르다’라는 이분법적 결론이 아니라, 올바른 트랜잭션 프로토콜도 효율성의 스펙트럼 위에 존재한다는 관찰을 제공합니다.
이 글은 최근 발표한 VLDB ’25 논문인 Design and Modular Verification of Distributed Transactions in MongoDB의 고수준 동반 글이기도 하며, 논문에서는 이러한 주제를 더 깊이 기술적으로 탐구합니다.
MongoDB는 클라이언트가 일반적이고 대화형(interactive)인 트랜잭션 인터페이스로 발행한 트랜잭션에 대해 스냅샷 격리를 제공하는 분산 다중 문서 트랜잭션 프로토콜을 구현합니다. 이는 읽기/쓰기 연산을 사전에 선언하도록 요구하는 일부 현대적(하지만 더 제한적인) 트랜잭션 시스템과 대비됩니다. 사용자는 익숙한 프로그래밍 언어 지향 API로 트랜잭션을 작성할 수 있고, 트랜잭션 연산을 애플리케이션 언어의 일반적인 문장처럼 순차적으로 실행할 수 있습니다.
MongoDB의 분산 트랜잭션 프로토콜은 샤딩 클러스터 전반에서 트랜잭션 간 순서와 가시성을 관리하기 위해 인과적으로 일관된 타임스탬프를 사용하며, 샤드 간 원자적 커밋을 보장하기 위해 2단계 커밋(2PC) 기반 프로토콜을 수행합니다. 우리는 단일 노드 트랜잭션(v3.2)에서 시작해 단일 레플리카 셋 트랜잭션(v4.0)을 거쳐 완전한 샤딩 클러스터 트랜잭션(v4.2)까지, 세 버전에 걸쳐 점진적으로 MongoDB의 분산 트랜잭션을 개발했습니다. 따라서 MongoDB의 분산 트랜잭션 프로토콜은 단일 노드의 다중 버전(multiversion) 트랜잭션 키-값 저장 엔진인 WiredTiger 위에 계층적으로 올라간 것으로 이해할 수 있습니다. 이 저장 엔진은 로컬 스냅샷 격리 키-값 저장을 구현하며, 분산 트랜잭션의 2단계 커밋 프로토콜과 통합하기 위한 추가 API 메서드도 제공합니다.
그림 1. MongoDB의 기본 샤딩 아키텍처.
조정자(coordinator)가 모든 참여 샤드로부터 성공적인 prepareTransaction 응답을 받으면, 트랜잭션의 커밋 타임스탬프(commit timestamp) 를 계산합니다. 이 타임스탬프는 수신한 모든 준비 타임스탬프(prepared timestamp)보다 크거나 같은 값으로 선택됩니다. 이후 조정자는 이 커밋 타임스탬프를 포함해 모든 참여 샤드에 commitTransaction 명령을 전송하며, 각 샤드는 저장 엔진 내부에서 해당 커밋 타임스탬프 시점에 트랜잭션의 쓰기(write)가 보이도록 로컬 커밋을 수행합니다.
클라이언트는 쿼리가 접근하는 데이터에 따라 적절한 샤드로 연산을 라우팅하는 무상태 라우터 노드 mongos 를 통해 샤딩 클러스터와 상호작용합니다. 트랜잭션이 시작되면 해당 라우터는 트랜잭션에 전역 읽기 타임스탬프(read timestamp) 를 할당합니다. 이후 라우터는 트랜잭션 연산이 읽거나 쓰는 키에 따라 적절한 샤드로 연속적인 트랜잭션 연산들을 디스패치하며 트랜잭션을 계속 처리합니다.
트랜잭션이 쓰기 충돌(write conflict)이나 기타 내부 오류로 인한 abort를 만나지 않고 성공적으로 완료되면, 2단계 커밋(2PC)의 변형을 시작합니다. 라우터는 2PC 실행 중 2PC 라이프사이클 데이터의 내구성을 보장하기 위해 2PC 프로세스를 조정자 샤드(coordinator shard) 에 위임하며 이로써 2PC를 시작합니다. 조정자가 실행하는 2PC 프로세스는 먼저 모든 참여 샤드에 prepareTransaction 메시지를 보내며, 각 샤드에서 준비(prepare) 단계를 실행합니다. 이 단계는 해당 샤드에서 준비 타임스탬프(prepare timestamp) 를 선택하고, 그 샤드 레플리카 셋에서 prepare 로그 항목을 영속화하고 과반수 커밋(majority commit)함으로써 트랜잭션의 쓰기를 내구적으로 만드는 과정으로 구성됩니다.
그림 2. 다중 샤드 분산 트랜잭션의 기본 커밋 흐름과 관련 타임스탬프.
샤드가 트랜잭션에 대해 prepare 단계에 들어가면, 저장 엔진 계층에서 해당 트랜잭션이 접근하는 키들을 준비(prepared) 상태로 표시합니다. 이로 인해 준비 타임스탬프보다 크거나 같은 타임스탬프에서의 모든 읽기(read)는 해당 키에서 블로킹됩니다. 아직 그 트랜잭션의 커밋 타임스탬프가 알려지지 않았기 때문에, 그 트랜잭션의 타임스탬프 이전을 읽어야 할지 이후를 읽어야 할지 판단할 수 없어 블로킹이 필요하기 때문입니다.
그림 3. 준비된 트랜잭션에 대한 타임스탬프 블로킹 동작.
또한 스냅샷 격리의 표준적인 쓰기 충돌 검사 동작도 각 샤드에서 트랜잭션 실행 동안 동일하게 적용됩니다. 즉, 동시에 실행되는 두 트랜잭션이 같은 샤드에서 동일한 키를 갱신하려 하면 둘 중 하나는 abort되어야 합니다.
2PC를 우회할 수 있는 추가 최적화도 있습니다. 예를 들어 읽기 전용 트랜잭션이나 단일 샤드에만 쓰는 트랜잭션의 경우가 그렇습니다. 하지만 위 설명은 MongoDB 샤딩 클러스터에서 분산 트랜잭션이 동작하는 일반적인 흐름을 설명합니다.
분산 트랜잭션 프로토콜의 형식 명세를 작성하는 것은, 프로토콜의 정확한 정합성(correctness) 및 격리성(isolation) 특성에 대한 신뢰를 얻기 위한 첫 단계이며, 아래에서 논의하듯 여러 다른 프로토콜 분석 및 검증 작업도 가능하게 합니다.
MongoDB처럼 복잡하고 계층화된 시스템에서는 전체 프로토콜 명세를 합성하기 전에 (특히 WiredTiger 같은) 계층 간 형식적 계약(contract)을 먼저 확립하고자 했습니다. 그래서 우리는 TLA+로 프로토콜을 합성적 방식으로 명세했습니다. 고수준 프로토콜 동작을 기술하는 동시에, 트랜잭션 프로토콜의 분산 측면과 기반 단일 노드 WiredTiger 저장 엔진 컴포넌트 사이의 경계를 형식화했습니다. 앞서 언급했듯 분산 트랜잭션 프로토콜은 더 낮은 수준의 저장 계층 위에서 동작하는 것으로 볼 수 있습니다.
그림 4. TLA+에서의 분산 트랜잭션 합성적 명세.
이 명세를 사용해, Crooks 등(PODC ’17)이 구축한 이론과 Soethout이 구현한 TLA+ 라이브러리에 기반한 상태 기반(state-based) 체커로 격리성 보장을 검증할 수 있었습니다. 이 라이브러리는 커밋된 트랜잭션 집합과 그 연산 히스토리를 입력으로 받아, 트랜잭션들이 스냅샷 격리, read committed 등을 만족하는지 검사합니다.
또한 우리의 명세는 서로 다른 readConcern 수준에서 MongoDB 트랜잭션이 제공하는 보장을 형식화하고 분석하는 데에도 도움이 됩니다. MongoDB 문서에서 논의하듯, “snapshot” readConcern은 트랜잭션에 대해 표준 스냅샷 격리를 제공합니다. “local” readConcern에서는 더 약한 격리 수준, 즉 read committed에 더 가까운 보장을 제공합니다. TLC 모델 체커를 사용하면, 작은 문제 인스턴스에 대해 약 10분, 약 12코어로 우리의 TLA+ 모델에서 이 두 readConcern 수준에 대한 스냅샷 격리 및 read committed 격리 보장을 확인할 수 있습니다. 트랜잭션 2개와 키 2개만으로도 상태 공간은 크지만 관리 가능하며, 버그가 존재한다면 작은 인스턴스에서도 드러나는 경향이 있습니다.
프로토콜 명세의 또 다른 이점은 정확성 검증을 넘어, 우리가 허용성(permissiveness) 이라고 부르는 성능 관련 성질을 측정할 수 있게 해준다는 점입니다. 본질적으로 특정 격리 수준을 구현하는 어떤 트랜잭션 프로토콜에 대해, 우리는 해당 격리 보장을 올바르게 만족하는지(안전성(safety)) 뿐 아니라 적절한 수준의 동시성(concurrency)을 허용하는지도 관심을 가질 수 있습니다. 예를 들어 직렬화 가능(serializable) 트랜잭션 프로토콜은 스냅샷 격리(또는 그보다 약한) 안전성 보장을 만족하지만, 스냅샷 격리를 목표(그리고 그에 수반되는 성능 특성)로 한다면 아마 우리가 원하는 선택은 아닐 수 있습니다.
더 나아가 고정된 격리 수준에 대해서도, 서로 다른 프로토콜 변형들이 이를 어떻게 구현하는지, 그리고 어느 쪽이 동시성 허용 측면에서 “더 잘”하는지 비교하고 싶을 수 있습니다.
유한 상태(finite state) 인스턴스에 대해서는, 도달 가능한 전체 상태 그래프를 고려한 뒤 이를 트랜잭션 히스토리 변수(즉, 커밋된 모든 트랜잭션과 그 연산 히스토리의 기록)로 사영(projection)하여 이를 수행할 수 있습니다. 그런 다음, 이 사영된 집합의 크기(cardinality)를 격리 정의가 허용하는 모든 트랜잭션 스케줄 집합에 대한 비율로 계산합니다. 유사한 허용성 개념은 트랜잭셔널 메모리 분야에서 다뤄져 왔지만, 분산 트랜잭션 프로토콜 맥락에서는 직접적으로 다뤄지지 않았습니다. 이는 단순한 이분법적 정합성 결과를 넘어선 형식 기법의 가치를 보여주는, 프로토콜 분석의 새로운 차원입니다.
그림 5. 허용성 지표 정의.
다양한 파라미터에서 프로토콜에 대해 이 비율을 계산하면, 서로 다른 변형들의 제약 정도를 정량적으로 비교할 수 있으며, 이 과정은 동시성을 높이기 위한 잠재적 격리 수준 최적화를 도출하는 가이드가 됩니다.
예를 들어 MongoDB의 readConcern: “local” 격리 수준에서, 유한한 프로토콜 파라미터에 대해 그 허용성 수준을 일반적인 read committed 정의와 비교할 수 있습니다. 특히 prepare 충돌 블로킹(앞서 논의) 및/또는 쓰기 충돌 검사 같은 저장 엔진 동시성 제어 조건을 약화(weaken)했을 때 허용성이 어떻게 달라지는지 분석할 수 있습니다. 이러한 시나리오에서 허용성을 측정하면, 프로토콜을 정량적으로 이해하고 특정 격리 보장에 대해 이론적으로 최적의 허용성 수준을 향해 나아가도록 안내하는 방법을 제공합니다.
그림 6. 서로 다른 충돌 동작에서의 허용성.
트랜잭션 프로토콜을 모델링한 결과, 이러한 접근이 정합성 검증뿐 아니라 허용성 지표 계산에 기반한 성능 관련 분석도 가능하게 함을 보여주었습니다. 개발자에게 중요한 핵심 요점은 ‘확신’입니다. 우리의 접근은 MongoDB의 분산 트랜잭션이 계층 전반에 걸쳐 올바르게 동작한다는 더 강한 신뢰를 제공하며, 프로덕션에서 발견하기 어려운 미묘한 정합성 버그를 피할 수 있게 해줍니다. 동시에 허용성을 정량화함으로써, 안전성뿐 아니라 프로토콜이 얼마나 많은 동시성을 허용하는지도(부하 상황에서 처리량과 가용성에 직접적인 영향을 주는 요소) 추론할 수 있습니다. 즉, 개발자는 자신의 애플리케이션이 ACID 보장을 유지할 뿐 아니라 시스템의 용량을 효율적으로 사용하고, 불필요한 abort와 재시도를 줄일 수 있다는 점을 신뢰할 수 있습니다.
이 글의 2부에서는 우리의 합성적 명세 접근이 추상 프로토콜의 정합성 특성을 추론하는 데 그치지 않고, 추상 저장 인터페이스가 구현의 의미론(semantics)과 올바르게 일치하는지도 자동으로 확인할 수 있게 해준 방식—즉, 저장 계층 명세를 사용해 기반 WiredTiger 키-값 저장 엔진에 대한 자동 모델 기반 테스트(model-based testing)를 수행한 방법—을 다룰 예정입니다.
이 작업에 대한 더 자세한 내용은 최근 발표한 VLDB ’25 논문과 관련 repo에서 확인할 수 있습니다. 이 저장소에는 명세와 코드가 포함되어 있으며, 브라우저에서 탐색 가능한 형태의 명세 링크도 제공됩니다. 또한 현대 분산 트랜잭션 프로토콜 검증에 관한 흥미로운 관련 연구와, 유사한 합성적 방식으로 분산 시스템을 모델링한 과거 연구도 있습니다.
