가벼운 정형 기법으로 검증한 S3 저장 노드 (ShardStore, SOSP 2021)

출처

참고 이 페이지는 원문 번역이 아니라 한국어 해설이에요. 정확한 표현과 수치는 원문을 확인하세요.

한눈에

• 문제: S3 는 저장 노드 소프트웨어를 새로 만든 ShardStore 로 바꾸고 있었습니다. 4만 줄이 넘는 Rust 코드가 디스크 위의 고객 데이터를 다루니, 충돌이나 동시성 버그 하나가 큰 사고가 될 수 있습니다.
• 제안: 완전한 수학적 증명 대신, 정확성을 여러 속성으로 나누고 속성마다 가장 알맞은 도구로 검사합니다. 기준이 되는 것은 Rust 로 쓴 "실행 가능한 참조 모델" 입니다.
• 결과: 기능, 충돌 일관성, 동시성 영역에서 16개의 문제를 운영 배포 전에 막았고, 검증 코드는 전체 코드의 약 13% 수준에 그쳤습니다(그림 5, 그림 6).
• 지금의 의미: 정형 기법 전문가가 만든 검사를 일반 엔지니어가 이어받아 유지하는 방식으로, AWS 에서 정형 기법을 일상 개발에 녹이는 대표 사례가 되었습니다. SOSP 2021 최우수 논문상 수상작입니다.

왜 나왔나

전통적인 검증 연구는 시스템 전체를 증명 보조기로 증명하는 데 집중했습니다. 하지만 증명은 코드의 3배에서 10배 분량이 들고, 코드가 매주 바뀌는 운영 시스템에서는 따라가기 어렵습니다. S3 팀이 원한 것은 "개발 속도를 늦추지 않고, 엔지니어가 직접 유지할 수 있고, 실제로 버그를 잡는" 방법이었습니다. 논문은 이를 "가벼운 정형 기법" 이라 부릅니다.

핵심 아이디어

ShardStore 의 구조 (2절)

ShardStore 는 샤드 ID 를 데이터 조각(chunk) 위치로 연결하는 LSM 트리를 인덱스로 쓰고, 샤드 데이터 자체는 트리 밖에 둡니다. 이렇게 하면 LSM 트리를 정리할 때 큰 데이터를 다시 쓰지 않아도 됩니다. 데이터는 디스크의 "익스텐트" 라는 덧붙이기 전용 구역에 쓰이며, 익스텐트마다 쓰기 포인터가 있습니다. 공간 회수(그림 1) 는 익스텐트를 훑어 살아 있는 조각을 다른 곳으로 옮긴 뒤 쓰기 포인터를 처음으로 되돌리는 방식입니다.

충돌 일관성은 소프트 업데이트(soft updates) 에서 착안했습니다. 모든 쓰기는 "이 쓰기가 디스크에 닿으려면 먼저 저 쓰기가 닿아야 한다" 는 의존성(Dependency) 을 갖고, I/O 스케줄러가 이 순서를 지킵니다. 그림 2 는 세 번의 put 이 만드는 의존성 그래프와 디스크 배치를 보여줍니다. 데이터는 S3 의 다른 노드에도 복제되어 있으므로, 여기서 충돌 일관성의 목적은 데이터 손실 방지라기보다 복구 트래픽과 운영자 개입을 줄이는 것입니다.

무엇을 검사할까: 속성 나누기 (3절)

핵심 속성은 "매 API 호출 뒤 구현과 참조 모델이 같은 키-값 매핑을 갖는다" 입니다. 이를 세 경우로 나눕니다.

1. 충돌 없는 순차 실행: 결과가 정확히 같아야 합니다.
2. 충돌이 있는 순차 실행: 조금 약한 동등성을 요구합니다.
3. 충돌 없는 동시 실행: 선형화 가능해야 합니다.

충돌과 동시성이 함께 있는 경우는 다루지 않습니다. 참조 모델은 Rust 로 쓰였고 크기는 구현의 약 1% 입니다. 해시맵 하나로 표현할 수 있을 만큼 단순한 모델이 복잡한 구현의 정답지 역할을 합니다. 같은 모델을 단위 테스트의 모의 객체로도 쓰기 때문에 엔지니어가 자연스럽게 최신 상태로 유지합니다.

적합성 검사 (4절)

proptest 라는 속성 기반 테스트 도구로 무작위 연산 시퀀스를 만들어 구현과 모델에 똑같이 실행하고 결과를 비교합니다(그림 3). 메모리 안의 가짜 디스크를 써서 실행을 결정적으로 만들었고, 배포 전마다 수천만 개의 시퀀스를 돌립니다.

무작위 입력은 그냥 두면 흥미로운 상황을 잘 만들지 못합니다. 그래서 get 은 이전에 put 한 키를 고르게 하고, 크기는 페이지 경계 근처에 몰리게 하는 식으로 입력에 편향을 줍니다. 버그가 나오면 자동으로 최소 사례로 줄이는데, 한 예(문제 #9) 에서는 61개 연산이 6개 연산과 충돌 1번, 합계 2바이트의 쓰기 2번으로 줄었습니다. 디스크 I/O 실패도 주입해 검사합니다.

충돌 일관성 (5절)

"DirtyReboot" 라는 연산을 시퀀스에 섞어, 충돌 시 어떤 쓰기가 디스크에 남을지 고르게 합니다. 검사하는 속성은 두 가지입니다. 영속성: 의존성이 디스크에 닿았다고 보고된 데이터는 재부팅 후 읽혀야 합니다. 전진성: 충돌 후에도 결국 모든 쓰기가 영속될 수 있어야 합니다. 문제 #10 은 UUID 가 우연히 페이지 경계의 매직 바이트와 겹쳐 생기는 버그로, 이 방법으로 찾았습니다.

동시성 (6절)

작은 동기화 부품은 Loom 으로 모든 스레드 실행 순서를 빠짐없이 탐색하고, 큰 시나리오는 무작위 스케줄링 도구 Shuttle 로 검사합니다(그림 4). 문제 #14 는 압축(compaction) 과 공간 회수가 겹칠 때 인덱스 항목을 잃을 수 있는 경쟁 조건이었고, 압축 중 익스텐트를 잠그는 것으로 고쳤습니다.

그 밖의 속성 (7절)

unsafe 코드의 정의되지 않은 동작은 Miri 로 검사했고, 그 과정에서 Miri 에 스레드와 잠금 지원을 더해 오픈소스에 기여했습니다. 역직렬화 코드가 일정 크기 이하 입력에서 패닉하지 않음은 Crux 로 기호 실행해 증명하고, 더 큰 입력은 퍼징으로 보완했습니다.

실험과 결과

8절의 경험 보고가 이 논문의 결과입니다.

• 막은 문제 (그림 5): 16개입니다. 기능 문제 5개(#1 에서 #5), 충돌 일관성 문제 5개(#6 에서 #10), 동시성 문제 6개(#11 에서 #16) 이며, 대부분 데이터 무결성에 영향을 줄 수 있었고 #12 는 교착 상태였습니다.
• 노력 (그림 6): 구현은 44,048줄, 전체는 72,460줄입니다. 검증용 코드(모델, 하네스 등) 는 코드베이스의 약 13% 이고 구현 크기의 약 20% 로, 전통적인 증명의 3배에서 10배 부담과 대비됩니다.
• 사람: 정형 기법 전문가 두 명이 9개월, 한 명이 3개월 전담했습니다. 이후 하네스 코드의 18% 는 전문가가 아닌 엔지니어가 마지막으로 수정했습니다.
• 한계: 테스트가 아주 큰 캐시를 쓰는 바람에 캐시 미스 경로의 버그 하나를 놓쳤습니다. 요청 파싱, 라우팅, 제어 평면 일부는 아직 범위 밖이었습니다.

지금 AWS 에서는

• 논문 시점에 ShardStore 는 Amazon S3 의 저장 노드에 배포되고 있었습니다. S3 의 저장 노드 구현을 이 논문 이후 AWS 가 따로 공개한 자료는 확인하지 않았습니다.
• 논문에서 쓴 무작위 동시성 테스트 도구 Shuttle 은 AWS 가 awslabs 조직에서 오픈소스로 공개해 유지하고 있습니다.
• 저자들은 향후 과제로 검증을 S3 의 분산 시스템 수준으로 넓히는 일을 꼽았습니다. 이 논문은 이후 AWS 엔지니어들이 정형 기법과 테스트 실천을 소개할 때 자주 인용하는 사례가 되었습니다.

함께 읽기

• Amazon S3: 이 사이트의 기능 문서
• Physalia 논문 해설: TLA+ 와 시뮬레이션 테스트를 함께 쓴 또 다른 AWS 사례
• DynamoDB 논문 해설: 복제 프로토콜을 TLA+ 로 검증한 사례
• 저자 발표 슬라이드