분산 프로토콜은 단위 테스트할 수 없지만, 모델 검증은 할 수 있다

분산 프로토콜은 단위 테스트할 수 없다. 단위 테스트는 한 대의 머신에서 한 개의 프로세스를 정해진 순서로 실행한다. 당신의 프로토콜은 다섯 대의 머신에서 열 개의 프로세스를 통제할 수 없는 순서로 실행한다. 이 두 현실 사이의 간극이 바로 버그가 서식하는 곳이다.

모델 검증은 그 간극을 메운다. 프로토콜이 도달할 수 있는 모든 가능한 상태의 모든 가능한 교차 실행을 탐색한다. 두 개의 복제본이 의견을 달리하는 경로, 리더 선출이 deadlock에 빠지는 경로, split-brain 상황이 발생하는 경로가 있다면 모델 검증기는 반드시 찾아낸다. 그리고 그것은 최초의 RPC handler를 작성하기 전에 이루어진다.

왜 분산 버그는 기존 테스트를 survive 하는가

문제는 상태 폭발이다. 메시지를 교환하는 세 개의 노드는 수십억 개의 실행 경로를 만들어낼 수 있다. 수작업으로 작성된 통합 테스트는 그중 열여덟 개 정도만 커버한다. 보통은 해피 패스와 몇 가지 명백한 고장 모드뿐이다. 노드 A가 prepare를 보내고 ack를 보내는 사이에 정확히 크래시하는 버그를 CI에서 재현해 보시라.

형식 검증은 학술적 연습처럼 들리지만, 모델 검증은 다르다. 프로토콜이 영원히 올바르다는 것을 증명하는 것이 아니다. 사양 기술 언어로 프로토콜을 기술하고, 중요한 속성을 정의한 뒤, 도구가 상태 공간을 특정 경계까지 철저히 탐색하도록 한다. 위반이 발견되면 최소 추적 결과를 제공한다. 버그를 재현하기 위한 단계별 조리법을 얻는 것이다. 하이젠버그도 없고, “내 머신에서는 돌아간다”도 없다.

이를 위해 가장 실용적인 도구는 Leslie Lamport가 개발한 TLA+이다. 수학처럼 보이는 이유는 그것이 수학이기 때문이다. 하지만 그 수학은 생각보다 단순하고, 그 대가는 본 환경에서 새벽 2시에 표면화될 버그를 찾아내는 것이다.

모델 검증이 실제로 하는 일

모델 검증기는 세 가지 입력을 받는다. 시스템 기술, 환경 기술, 그리고 유지하고자 하는 속성이다. 시스템 기술은 프로토콜 논리를 포착한다. 환경 기술은 통제할 수 없는 모든 것을 포착한다. 네트워크 지연, 메시지 손실, 노드 크래시, 시계 왜곡이다. 속성은 보통 불변 조건(“커밋된 로그는 결코 덮어쓰이지 않는다”)이나 활성 조건(“모든 요청은 결국 응답을 받는다”)이다.

검증기는 도달 가능한 모든 상태와 상태 간 유효한 전이를 생성한다. 유한 상태 공간에 대해서는 철저히, 무한 상태 공간에 대해서는 유계 탐색으로 수행한다. 불변 조건이 위반되면 중단하고 최단 실패 경로를 보고한다.

이것은 마법이 아닌 무차별 대입이다. 모델 검증기는 의도를 이해하지 않는다. 단순히 모든 것을 시도할 뿐이다. 그것이 바로 핵심이다. 통합 테스트는 당신의 가정에 편향되어 있다. 모델 검증기는 가정이 없다.

TLA+에서 단순한 합의 프로토콜 명시

최소한의 예를 살펴 보자. 리더가 값을 제안하고, 수락자의 정족수가 수락해야 값이 선출되는 단일 결정 합의 프로토콜이다. 이것은 Paxos, Raft, 그리고 당신이 들어 본 다른 모든 합의 알고리즘의 핵심 아이디어이다.

시스템에 대한 TLA+ 사양은 다음과 같다:

------------------------------ MODULE Consensus ------------------------------
EXTENDS Integers, Sequences, FiniteSets

CONSTANTS Values, Acceptors, Quorum

VARIABLES chosen

Init == chosen = {}

Propose(v) ==
  /\\ v \\in Values
  /\\ chosen = {}
  /\\ chosen' = {v}

Next ==
  \\E v \\in Values : Propose(v)

Spec == Init /\\ [][Next]_chosen /\\ WF_chosen(Next)

ChosenUniqueness ==
  Cardinality(chosen) \\leq 1
=============================================================================

이 사양은 다음을 말한다. 초기에는 아무것도 선출되지 않는다. propose 동작은 chosen을 단일 값으로 설정할 수 있지만, 아직 아무것도 선출되지 않은 경우에만 가능하다. ChosenUniqueness 불변 조건은 선출될 수 있는 값이 최대 하나임을 규정한다.

TLA+ 모델 검증기인 TLC는 ChosenUniqueness를 위반하는 실행 추적이 없음을 검증한다. 두 리더가 이전 값을 확인하지 않고 동시에 제안할 수 있는 버그를 도입하면 TLC는 수 밀리초 만에 반례를 찾는다.

지저분한 부분 추가: 크래시와 메시지 손실

위의 사양은 너무 깨끗하다. 실제 분산 시스템은 깨끗하지 않다. 메시지가 유실된다. 노드가 재부팅된다. 네트워크 분할이 노드 그룹을 서로 격리한다. 이러한 고장을 모델링할 때 비로소 모델이 유용해진다.

잠재적 손실을 포함한 메시지 전달을 모델링한 보다 현실적인 단편은 다음과 같다:

VARIABLES msgs, acceptorState

Send(m) == msgs' = msgs \\cup {m}

Deliver(m) ==
  /\\ m \\in msgs
  /\\ msgs' = msgs \\ {m}
  /\\ acceptorState' = [acceptorState EXCEPT ![m.to] = @ \\cup {m.value}]

Drop(m) ==
  /\\ m \\in msgs
  /\\ msgs' = msgs \\ {m}
  /\\ UNCHANGED acceptorState

Next ==
  \\E m \\in msgs : Deliver(m) \\/ Drop(m)

Drop은 중요한 추가이다. 수락자 상태를 변경하지 않고 메시지 손실을 모델링한다. TLC는 어떤 메시지든 전달되거나, 손실되거나, 무기한 지연될 수 있는 추적을 탐색한다. 리더 크래시와 복구를 추가하면 상태 공간이 커지지만, TLC는 여전히 체계적으로 탐색한다.

이것이 내가 TLA+를 처음 시작했을 때 당황했던 부분이다. 나는 프로토콜 논리만 모델링하고 싶었다. 하지만 버그는 논리에 있지 않았다. 논리와 내가 고려하지 않은 고장 모드 사이의 상호작용에 있었다. 둘 다 모델링해야 한다.

절충: 상태 공간 폭발과 추상화

모델 검증은 공짜가 아니다. 상태 수는 프로세스 수와 메시지 페이로드 크기에 따라 지수적으로 증가한다. 다섯 개의 값과 세 명의 수락자를 가진 사양은 수백만 개의 상태를 생성할 수 있다. 네 번째 수락자를 추가하면 수십억 개에 이른다. 노트북에서 실행하면 완료되기 전에 메모리가 고갈된다.

해결책은 추상화이다. 실제 64바이트 값을 모델링하지 않는다. 두 개의 값 V1과 V2를 모델링한다. 두 값에 대해 프로토콜이 올바르게 작동하면 특정 값은 중요하지 않다. 1만 개 항목의 로그도 모델링하지 않는다. 깊이 2의 로그를 모델링한다. 깊이 2에서 안전성이 유지되면 거의 항상 임의의 깊이에서도 유지된다. 이를 small-model checking이라 하며, 해당 분야의 표준 관행이다.

핵심 기술은 어떤 세부 사항이 중요하고 어떤 세부 사항이 중요하지 않은지 배우는 것이다. 메시지 내용은 보통 안전성 속성에 중요하지 않다. 메시지 순서는 거의 항상 중요하다. 노드 신원은 중요하지 않을 수 있지만, 각 역할의 노드 수는 중요하다.

상태 공간이 여전히 너무 크다면 다른 선택지가 있다. 동일한 노드를 상호 교환 가능하게 처리하는 대칭성 축소를 사용할 수 있다. 탐색 깊이를 제한할 수 있다. 또는 SMT 솔버를 사용하여 모든 상태를 열거하지 않고 상태에 대해 추론하는 기호적 모델 검증기인 Apalache로 전환할 수 있다.

사양에서 구현으로: 동기화 유지

검증된 사양도 구현이 그것에서 벗어나면 무가치하다. 사양은 설계도이다. 코드는 건물이다. 둘 사이에 자동화된 다리는 없으며, 그 틈새가 버그가 기어들어가는 곳이다.

실용적인 접근법은 TLA+ 사양을 우연히도 실행 가능한 설계 문서로 취급하는 것이다. 풀 리퀘스트 시 코드와 함께 검토하라. 구현이 엣지 케이스를 처리할 때, 사양도 그것을 처리하는지 자문하라. 프로덕션에서 버그를 발견하면 사양이 그것을 잡았을지 확인하라. 그렇지 않다면 사양을 업데이트하라.

일부 팀은 TLC가 생성하는 반례에서 테스트 케이스를 생성하는 데 한 걸음 더 나아간다. 두 복제본이 분기하는 모습을 보여주는 TLC 추적이 통합 테스트 시나리오가 된다. 이는 수작업이지만, 형식 모델을 테스트 스위트와 연결한다.

Sentry에서 우리는 이 접근법을 사용하여 분산 속도 제한 프로토콜을 검증했다. 사양은 복구 중인 노드가 특정 분할 시나리오에서 기아 상태에 빠질 수 있는 활성 문제를 잡아냈다. 우리의 통합 테스트는 항상 분할을 깔끔하게 치유했기 때문에 그것을 트리거한 적이 없었다. 모델 검증기는 깔끔함을 신경 쓰지 않는다. 지저분한 경우를 시도하고, 버그를 찾아내어, 우리를 매우 혼란스러운 사고로부터 구해주었다.

시작하기: 첫 모델 검증

이것을 시도해 보고 싶다면 TLA+ Toolbox로 시작하라. 사양을 작성하고 검증하기 위한 무료 IDE이다. 함께 제공되는 Paxos와 Raft 예제를 풀어보라. 위의 합의 코드 조각보다 복잡하지만, 실제 프로토콜이 어떻게 모델링되는지 보여준다.

첫 사양을 위해 자신의 시스템에서 작은 것을 고르시라. 리더 선출 프로토콜. 분산 캐시 무효화 방식. 2단계 커밋 변종. 유지된다고 믿는 불변 조건을 적으시라. 그런 다음 TLC가 당신이 옳은지 말해주도록 하시라. 대개 그 답은 “아니다”이며, 대개 첫 시간 안에 말해준다.

모델 검증은 모든 버그를 찾지는 못한다. 성능에는 도움이 되지 않고, 직렬화 실수도 잡아내지 못하며, 구현이 사양과 일치하는지도 검증하지 못한다. 모델 검증이 하는 것은 통합 테스트가 놓치는 깊은 프로토콜 버그를 설계 시점에 찾아내는 것이며, 그때 수정 비용은 전혀 들지 않는다.

이것이 분산 시스템에서 가장 저렴한 버그 수정이다. 더 나은 디버거도, 더 많은 모니터링도 아니다. 코드가 존재하기 전에 버그를 잡는 것이다.