AWS가 '절대 죽지 않는 시스템'을 만드는 법: TLA+, P

도현·2025년 12월 15일

PLanguage TLA aws chaosengineering systemdesign 동시성 소프트웨어 설계 시스템 설계

이 포스트는 GeekNews의 Amazon Web Services의 시스템 정확성 실천 사례을 참고하여 게시한 글입니다.

얼마전 TLA+에 대한 포스트를 게시하고 난 후 AWS의 시스템 정확성 설계에 대해 리서치하던 중, GeekNews에 흥미로운 글이 있어서 새로운 인사이트를 정리했습니다.

"Amazon S3가 어떻게 수조 개의 객체에 대해 '강력한 일관성(Strong Consistency)'을 보장하게 되었을까요?"

우리는 흔히 테스트 커버리지를 100% 채우면 안전하다고 착각합니다. 하지만 클라우드 규모의 분산 시스템에서는 테스트 케이스로 예측할 수 없는 '비결정적 버그(Nondeterministic Bugs)'들이 숨어 있습니다. 스레드 스케줄링이 꼬이거나, 네트워크 패킷 순서가 뒤바뀌는 순간 시스템은 멈춥니다.

AWS는 지난 15년 동안 이 문제를 해결하기 위해 수학적 증명(Formal Methods)을 현업에 가장 적극적으로 도입한 기업입니다. 오늘은 AWS가 TLA+의 한계를 넘어 P 언어, 결정적 시뮬레이션, 그리고 장애 주입(Fault Injection)까지 진화시켜 온 그들의 '무결성 생태계'를 파헤쳐 봅니다.

1. TLA+의 한계와 P 언어의 등판

초기 AWS는 TLA+를 통해 시스템을 검증했습니다. 하지만 문제가 있었습니다. TLA+는 너무 수학적이라 일반 개발자들이 배우기엔 진입장벽이 높았죠. 개발자들은 수학 공식보다는 코드와 아키텍처 다이어그램에 익숙하니까요.

그래서 AWS는 P 언어를 도입했습니다.

왜 P인가? : "개발자에게 친숙한 상태 기계(State Machine)"
P 언어는 마이크로서비스(SOA) 구조에 익숙한 개발자들을 위해 '상태 기계(State Machine)' 모델링 방식을 제공합니다.

TLA+: 수학적 논리 (Logic)
P 언어: 상태와 이벤트 (State & Event)

AWS의 핵심 서비스인 S3, EBS, DynamoDB 팀은 P를 사용하여 설계 초기 단계부터 버그를 잡아냈습니다. 특히 S3의 'Read-After-Write' 일관성 업데이트는 P로 프로토콜을 모델링하고 검증했기에 사고 없이 배포될 수 있었습니다.

최근에는 PObserve라는 도구까지 개발했습니다. 이는 실행 로그를 분석해 "실제 코드가 설계 명세(P 모델)대로 동작했는지" 사후 검증까지 해줍니다. 설계와 구현의 불일치를 막는 결정적 한 방입니다.

2. 무겁기만 한 건 싫다: 경량 형식 기법의 확대

모든 코드에 수학적 증명을 적용할 순 없습니다. 그래서 AWS는 가성비 좋은 '경량(Lightweight) 형식 기법'을 적극 활용합니다.

속성 기반 테스트 (Property-Based Testing)
"1+1=2"를 테스트하는 게 아니라, "어떤 숫자를 더하든 결과는 숫자여야 한다"는 속성을 테스트합니다. S3 ShardStore 팀은 이를 통해 예외 케이스를 무작위로 생성하고 실패 시나리오를 찾아냅니다.
결정적 시뮬레이션 (Deterministic Simulation)
분산 시스템 테스트가 어려운 이유는 '재현 불가능한 랜덤 요소(스레드 타이밍 등)' 때문입니다. AWS는 단일 스레드 시뮬레이터 안에서 시간을 통제하며 분산 시스템을 실행합니다. 즉, "우연히 발생하는 버그"를 "언제든 재현 가능한 버그"로 만듭니다. (참고: AWS는 이를 위해 shuttle, turmoil 같은 도구를 오픈소스로 공개하기도 했습니다.)
지속적 퍼징 (Continuous Fuzzing)
Aurora DB 팀은 SQL 쿼리를 무작위로 생성해 데이터베이스에 쏟아붓습니다. 이를 통해 파티셔닝 논리가 깨지지 않는지, 격리성(Isolation)이 유지되는지 검증합니다.

3. 일부러 고장 내기: FIS와 메타안정성

시스템이 논리적으로 완벽해도, 현실 세계의 하드웨어는 고장 납니다. 여기서 FIS (Fault Injection Service)가 등장합니다.

"알고 맞는 매가 덜 아프다"
AWS는 프라임 데이(Prime Day) 준비 기간에만 700번 넘게 일부러 서버를 망가뜨리고 API 오류를 주입합니다. 중요한 건, 그냥 망가뜨리는 게 아닙니다. "형식 명세(Spec)와 대조"합니다.

명세: "서버가 죽으면 3초 안에 백업 노드가 켜져야 함"
실험: 서버를 죽여본다 -> 3초 안에 켜지는지 확인한다.

메타안정성(Metastability)의 공포
가끔 시스템은 재시도(Retry) 폭풍으로 인해 '영구적인 장애 상태'에 빠집니다. 이를 메타안정성이라 부르는데, AWS는 P와 TLA+ 모델을 기반으로 시뮬레이션을 돌려 이런 최악의 좀비 상태가 발생할 확률까지 계산해 냅니다.