TLA+와 TLC 모델 검사로 Depot Registry의 가비지 컬렉터에서 동시성 경쟁 조건을 찾아내고, S3 버전 관리로 불변 콘텐츠 주소 지정 블롭의 안전한 삭제를 보장한 방법을 설명합니다.
가장 찾기 어려운 분산 시스템 버그는 어느 한 연산 안에 있지 않습니다. 두 프로세스가 각각 올바른 일을 수행하지만, 아무도 예상하지 못한 순서로 실행되면서 데이터가 사라집니다. 테스트는 여러분이 상상한 인터리빙만 실행하고 버그는 상상하지 못한 인터리빙에 있기 때문에, 이런 버그를 잡지 못합니다.
Depot Registry 규모에서는 이것이 더 이상 가정이 아닙니다. 일정 요청량에 도달하면 백만 번 중 한 번 일어나는 인터리빙이 현실이 되며, 여러분이 통제할 수 없는 주기에 따라 발생합니다.
그래서 Depot Registry의 가비지 컬렉터를 다시 만들 때 TLA+로 모델 검사를 수행했습니다. 모델 검사기는 테스트와 검토에서 놓친 실제 버그를 발견했습니다. 또한 처음 읽으면 터무니없게 들리는 설계 결정을 정확히 정의하도록 만들었습니다. 우리 레지스트리는 불변의 콘텐츠 주소 지정 블롭(정의상 절대 바뀌지 않음)을 저장하지만, 여전히 S3 버킷 버전 관리에 의존합니다.
**TLA+**는 시스템을 상태와 전이로 기술하는 언어입니다. TLC는 도달 가능한 모든 상태와 가능한 모든 인터리빙을 탐색한 뒤, 모든 경우에 불변 조건이 유지되는지 알려 주는 모델 검사기입니다. 구현체를 TLA+로 작성하는 것이 아닙니다. 검사기가 완전히 탐색할 수 있을 만큼 작지만, 모델의 버그가 시스템의 버그를 가리킬 만큼 실제와 가까운 단순화된 모델을 작성합니다.
다음은 사소한 모델입니다. 두 클라이언트가 잠금 없이 읽은 뒤 쓰기를 수행하며 공유 지갑에서 출금합니다.
---------------- MODULE Wallet ----------------
EXTENDS Integers
VARIABLES balance, read
Init == balance = 10 /\ read = [c \in {"a", "b"} |-> -1]
Check(c) == read[c] = -1
/\ read' = [read EXCEPT ![c] = balance]
/\ UNCHANGED balance
Withdraw(c) == read[c] >= 8
/\ balance' = balance - 8
/\ read' = [read EXCEPT ![c] = -2]
Next == \E c \in {"a", "b"}: Check(c) \/ Withdraw(c)
NoOverdraft == balance >= 0
================================================
각 정의는 전이입니다. Check(c)는 잔액을 읽고, Withdraw(c)는 클라이언트가 충분한 돈을 확인했을 때 8을 뺍니다. /\는 “그리고”를, \/는 “또는”을 뜻합니다. 프라임이 붙은 변수 balance'는 다음 상태의 값이며, NoOverdraft는 모든 곳에서 유지되기를 원하는 불변 조건입니다.
TLC는 네 단계 만에 이를 깨뜨립니다. 클라이언트 a가 확인하여 10을 보고, 클라이언트 b가 확인하여 10을 본 뒤, 둘 다 출금하면 잔액은 -6이 됩니다. 이것은 전형적인 확인 후 실행 경쟁 조건이며, 정확한 재현 방법을 보여 주는 단계별 추적과 함께 기계적으로 발견됩니다. 어떤 테스트 실행도 운이 나빴던 것이 아닙니다. 검사기가 단순히 모든 순서를 시도했을 뿐입니다.
지갑은 장난감 예제입니다. 다음은 레지스트리 GC 모델의 실제 불변 조건 중 하나에 같은 아이디어를 적용한 것입니다.
ManifestNeedsData ==
\A p \in PusherIDs: manifestExists[p] => s3Versions /= {}
왼쪽에서 오른쪽으로 읽어 보겠습니다.
ManifestNeedsData는 이름이고, ==는 “다음과 같이 정의된다”를 뜻합니다.\A는 “모든”을 뜻합니다.p \in PusherIDs는 p가 모델의 모든 푸셔를 순회한다는 뜻입니다.manifestExists[p]는 푸셔 p에 커밋된 매니페스트가 있는지 묻습니다.=>는 “왼쪽이 참이면 오른쪽도 참이어야 한다”를 뜻합니다.s3Versions /= {}는 S3 버전 집합이 비어 있지 않음을 뜻합니다.합치면 이 불변 조건은 대략 다음 의사 코드와 같습니다.
for each p in PusherIDs:
if manifestExists[p]:
assert s3Versions is not empty
마지막 절은 너무 약해 보일 수 있습니다. 올바른 블롭이 존재한다고 하지 않고, 어떤 S3 버전이 존재한다고만 말하기 때문입니다. 이는 의도적입니다. 이 모델에는 단일 블롭 다이제스트가 있습니다. 우리가 관심 있는 경쟁 조건은 매니페스트가 여전히 해당 블롭을 필요로 하는 동안 GC가 그 블롭을 삭제할 수 있는지이기 때문입니다. 다중 다이제스트 모델에서는 불변 조건이 다이제스트별로 인덱싱되어야 합니다. s3Versions[manifestDigest[p]] /= {}처럼 말입니다. 모델을 검토한다는 것은 이런 선택이 답하려 했던 질문을 보존하는지 묻는 일입니다.
움직이는 부분(업로드, 데이터베이스 트랜잭션, GC 워커)을 모델링하고, 항상 참이어야 하는 것을 명시한 다음, 언젠가 프로덕션 트래픽이 여러분의 설계에 할 일을 검사기에 맡기십시오.
TLA+는 수십 년간 존재해 왔으며 평판 문제가 있습니다. 모두가 강력하다는 데 동의하지만, 변화하는 구현체 옆에서 충실한 모델을 작성하고 유지하는 데 걸리는 몇 주를 예산에 반영하는 사람은 거의 없습니다. 우리도 그랬습니다. 올해 전까지는 GC 명세가 우선순위 경쟁에서 매번 밀렸을 것입니다.
달라진 점은 더 이상 모델을 손으로 작성하지 않는다는 것입니다. 에이전트가 구현체, Go 트랜잭션과 SQL 및 S3 호출을 읽고 명세로 변환합니다. 나머지는 우리가 검토합니다. 불변 조건이 의도한 바를 말하는가, 그리고 모델이 올바른 것을 추상화하는가를 말입니다. TLA+ 작성이 비용이 많이 드는 부분이었습니다. 항상 참이어야 할 것이 무엇인지 결정하는 일은 언제나 비용이 적었고, 계속 사람이 맡는 부분입니다.
그 결과는 동시 푸셔, 두 GC 도메인, 카운터 조정기, 주입된 카운터 드리프트가 모두 인터리빙되는 레지스트리의 3계층 가비지 컬렉터 명세입니다. 이는 실제 구현체에 뿌리를 두고 있으며, 트랜잭션 단위로 모델링됩니다. TLC는 약 21분 동안 14,290,224개의 고유 상태를 탐색하고 10개의 안전성 불변 조건과 2개의 활성 속성을 증명합니다. 가장 중요한 불변 조건은 첫 번째입니다. 커밋된 매니페스트는 절대 블롭 데이터를 잃지 않습니다.
이제 우리도 모두처럼 AI를 사용해 더 빠르게 배포합니다. 하지만 이전에는 검증할 시간이 없었던 것보다 더 올바른 시스템을 만들기 위해서도 이를 사용하고 있습니다.
OCI 레지스트리는 콘텐츠 주소 지정 방식입니다. Depot Registry에서 블롭은 blobs/sha256/<digest>에 존재하며, 다이제스트는 콘텐츠의 해시입니다. 같은 블롭을 두 번 업로드하면 같은 키에 바이트 단위로 동일한 데이터가 생깁니다. 어떤 것도 제자리에서 바뀌지 않습니다. 이 모델에서는 S3 버킷 버전 관리가 무의미해 보입니다. 객체의 모든 버전이 동일할 것이기 때문입니다.
하지만 문제는 삭제입니다.
가비지 컬렉션은 더 이상 아무것도 참조하지 않는 블롭을 제거해야 합니다. GC 워커는 참조가 0인 블롭을 표시하고, 유예 기간을 기다린 뒤 다시 검증하여 삭제합니다. 하지만 참조는 MySQL에 있고 바이트는 S3에 있으며, 두 시스템에 걸친 트랜잭션은 없습니다. 이로 인해 틈이 생깁니다.
각 개별 단계는 올바릅니다. 그러나 인터리빙은 살아 있는 데이터를 삭제합니다. 그리고 “클라이언트가 블롭이 가비지가 되는 바로 그때 다시 푸시한다”는 일은 이국적인 상황이 아닙니다. 인기 있는 베이스 이미지가 사용에서 빠졌다가 다시 사용될 때 일어나는 일입니다.
잠금이나 더욱 신중한 재검증으로 이를 고치려 할 수 있지만, S3를 재검증하고 삭제하는 일을 하나의 원자적 단계로 수행할 수는 없습니다. 그래서 대신 삭제 자체를 정확하게 만들었습니다. 버킷은 버전 관리가 활성화되어 있습니다. 같은 키를 다시 업로드하면 덮어쓰는 대신 새 버전이 됩니다. GC가 블롭을 표시할 때 확인한 특정 S3 버전 ID를 기록합니다. 삭제할 때는 그 버전만 삭제합니다.
v1을 캡처합니다.v2로 쓰고 참조를 커밋합니다.v1만 삭제합니다. 새 매니페스트가 기반으로 삼은 버전인 v2는 건드리지 않습니다.버전 관리를 이력을 유지하기 위해 사용하지 않습니다. 블롭의 모든 버전은 바이트 단위로 동일하므로 유지할 이력이 없습니다. 이를 삭제 펜스로 사용합니다. 즉, “이 키를 삭제하라”를 “내가 검사한 정확히 그 바이트를 삭제하라”로 바꾸며, 삭제가 쓰기와 경쟁해도 안전하게 만듭니다. 이것이 이 절 제목의 수수께끼에 대한 답이며, 가비지 컬렉션을 수행하는 모든 콘텐츠 주소 지정 저장소에 좋은 패턴입니다. 삭제를 안전하게 만드는 것은 불변 콘텐츠가 아니라 버전 관리입니다.
레지스트리 설계에서 한 가지 우려는 장애 상황에서 참조 카운터가 어떻게 동작하는가였습니다. 핫 블롭의 경합을 줄이기 위해 가벼운 사가를 사용합니다. 참조 카운터를 증가시키고 작업을 수행한 뒤, 실패하면 감소로 보상합니다. 크래시로 이 보상이 완료되지 못하면 조정기가 카운터를 복구합니다. 중요한 세부 사항은 잘못된 카운터가 대칭적이지 않다는 점입니다. 과다 계수는 GC를 지연시키지만, 과소 계수는 GC가 참조된 블롭을 가비지로 취급하여 살아 있는 데이터를 삭제하게 만들 수 있습니다.
그 비대칭성이 우리의 의심이었기에, 에이전트에게 정확히 그것을 검증하라고 요청했습니다. 에이전트는 다음 불변 조건을 내놓았습니다.
ManifestCountNeverUndercounts ==
blobActive => blobManifestCount >= TrueGlobalManifestCount
블롭의 행이 활성 상태일 때마다 저장된 카운터는 물리적 링크 행에서 계산한 실제 카운터보다 크거나 같아야 합니다. = 대신 >=를 사용한 것은 비대칭성을 직접 포착합니다. 과다 계수는 허용되지만, 과소 계수는 위반입니다.
이 불변 조건이 유용한 것을 알려 주려면 모델에도 잘못된 카운터가 포함되어야 합니다. 실패한 보상과 과거의 비동기화가 발생시키는 것과 같은 방향으로 카운터를 바꾸는 전용 드리프트 프로세스를 추가했습니다.
process DriftInjector = "drift"
begin
Drift:
await driftBudget > 0;
either
await blobActive /\ blobLinkCount > 0;
blobLinkCount := blobLinkCount - 1; \* undercount
or
await blobActive /\ blobLinkCount < N + DRIFT;
blobLinkCount := blobLinkCount + 1; \* overcount
end either;
driftBudget := driftBudget - 1;
goto Drift;
end process;
명세의 이 부분은 TLA+로 컴파일되는 프런트엔드 문법인 PlusCal로 작성되었기 때문에 의사 코드처럼 읽힙니다. await는 조건이 충족될 때까지 단계를 막고, either/or는 비결정적 선택입니다. 이 프로세스가 실행될 수 있는 모든 곳에서 TLC는 푸셔, GC 워커, 조정기와 인터리빙하여 두 분기를 모두 탐색합니다. 이 프로세스는 하나의 특정 버그를 표현하는 대신, 다른 연산이 실행될 때 카운터가 어느 방향으로든 잘못될 수 있다는 더 넓은 조건을 표현합니다. 그러면 검사기는 파괴적인 단계가 오래된 카운터에 의존하는 대신 물리적 행을 다시 세는지 검증할 수 있습니다.
모델 자체의 내부 장부 처리를 위한 불변 조건도 있습니다.
S3HeadOK ==
/\ (s3Versions = {}) <=> (s3Current = 0)
/\ (s3Versions /= {}) =>
/\ s3Current \in s3Versions
/\ s3Current = MaxVersion(s3Versions)
S3HeadOK는 “현재 버전” 포인터가 버전 집합이 비어 있을 때 정확히 비어 있고, 그렇지 않으면 최신 버전을 가리킨다고 말합니다. 이는 제품 보장을 표현하지 않습니다. 모델의 S3 추상화가 내부적으로 일관된 상태를 유지하는지 확인합니다. 이러한 검사는 모델링되는 시스템의 실패와 모델 자체의 실수를 구분하는 데 도움이 됩니다.
테스트와 모델 검사는 서로 다른 영역을 다룹니다. 테스트는 구체적 구현체를 실행하는 반면, 모델은 의도적으로 재현하기 어려운 인터리빙을 탐색합니다.
형식 검증은 한때 여유 시간이 넘치는 팀만 누릴 수 있는 사치였습니다. 그 제약은 사라졌습니다. 구현체를 명세로 충실히 변환하는 지루한 부분은 이제 에이전트에 위임하고, 여러분은 판단을 내릴 수 있습니다. 우리가 6개월 전에 알았더라면 좋았을 내용을 소개합니다.
전투를 가려서 선택하십시오: 모든 것에 TLA+를 들이대지 마십시오. 좋은 후보는 경쟁하는 프로세스, 까다로운 트랜잭션 경계, 타이밍을 두고 경쟁하는 자율 워커, 또는 공유 트랜잭션 없이 여러 시스템에 걸친 작업입니다. 예를 들어 CRUD 엔드포인트에는 모델 검사기가 필요하지 않습니다.
행동 우선 편향을 가지십시오: 아직 TLA+를 배우는 중이라면 목표는 정확성 증명이 아닙니다. 그것은 나중의 일이며, 어쩌면 영원히 하지 않을 수도 있습니다. 사람들이 “TLA+”를 들으면 첫 번째 반론은 늘 “하지만 모델이 현실과 맞지 않으면 어떡하죠?”입니다. 그것은 핵심이 아닙니다. 테스트와 형식 검증은 모두 신뢰를 높이기 위해 존재하며, 모델 검사기는 신뢰를 조절하는 다이얼 하나를 더해 줍니다. 그러니 생성된 명세의 모든 줄을 이해할 때까지 기다리지 마십시오. 실행해서 무엇이 나오는지 보십시오. 최악의 경우 오후 한때를 잃고, 최선의 경우 파고들 실마리를 발견합니다. 실수의 비용이 높다면, 그때 명세 자체의 결함을 찾는 데 실제 시간을 투자하면 됩니다.
이 워크플로를 활용하십시오: 설계 시점이나 기존 구현체로부터, 더 저렴한 모델을 사용해 인터리빙 절차의 시퀀스 다이어그램을 생성하십시오. 이를 검토하고 단순화하며 중요하지 않은 단계를 추상화하십시오. 저는 이 탐색에 Codex를 좋아합니다. 다이어그램을 보기 좋게 렌더링하고, 보조 대화를 통해 주 대화의 흐름을 망치지 않고 주제를 파고들기 쉽습니다. 다이어그램이 의도한 바를 말하게 되면, 이를 최전선 모델(우리의 경우 추가 고노력 설정의 Fable)에 넘겨 TLA+ 명세를 생성하십시오. 첫 명세는 블랙박스일 것입니다. 아직 TLA+를 읽을 수 없으므로, 판단할 수 있는 것은 입력과 출력뿐입니다. 괜찮습니다. 거기서 시작하십시오.
워크플로를 다듬으십시오: 이제 블랙박스를 한 번에 한 부분씩 투명하게 만드십시오. 진입점은 불변 조건입니다. 읽을 수 있는 부분, 즉 항상 참이어야 하는 것에 대한 짧은 문장이기 때문입니다. 보통 명백한 것이 1–3개 있습니다. 에이전트에게 더 제안하게 한 뒤 과감하게 덜어 내십시오. 몇 번 반복하면 명세의 나머지도 더 이상 불투명하지 않게 됩니다. 전이를 인식하기 시작하고, 이어서 의문을 제기하게 됩니다. 재시도는 정말 이렇게 동작하는가? 모델은 여기서 정말 두 워커를 허용하는가? 이제 명세를 화이트박스로 읽으며, 출력을 믿기만 하는 대신 모델 자체의 문제를 찾게 됩니다.
의심을 불변 조건으로 바꾸십시오: 검사기가 줄 수 있는 확신이 바로 그것이므로, 확신하지 못하는 것을 설명하십시오. 우리에게는 GC 카운터의 비대칭성이었습니다. 과다 계수는 항상 안전하지만 과소 계수는 절대 안전하지 않습니다. 앞 절에서는 에이전트가 그 의심으로 무엇을 했는지 설명했습니다. 여러분의 의심이 명세의 가장 좋은 요구 사항입니다.
발견 사항을 판결이 아니라 실마리로 다루십시오: 모델은 현실과 일치하지 않을 수 있으므로, 위반된 불변 조건은 계속 파고들 출발점입니다. 반례 추적을 시퀀스 다이어그램으로 바꾸고, 경쟁 조건을 완전히 이해하여 수정하거나 모델과 구현체의 불일치를 찾을 때까지 확대해 보십시오. 어느 결과든 진전입니다. 알 수 없는 미지에서 가리킬 수 있는 무언가로 이동한 것입니다.
이제 도구 상자에 도구가 하나 더 생겼습니다. 테스트는 생각해 낸 인터리빙을 확인하고, TLA+는 생각하지 못한 인터리빙을 탐색합니다.
TLA+란 무엇이며 TLC 모델 검사기는 무엇을 하나요?
TLA+는 시스템을 상태와 전이로 기술하는 언어입니다. TLC는 도달 가능한 모든 상태와 가능한 모든 인터리빙을 탐색한 뒤, 모든 경우에 불변 조건이 유지되는지 알려 주는 모델 검사기입니다. 구현체를 TLA+로 작성하는 것이 아닙니다. 검사기가 완전히 탐색할 수 있을 만큼 작지만, 모델의 버그가 시스템의 버그를 가리킬 만큼 실제와 가까운 단순화된 모델을 작성합니다.
불변 블롭을 사용하는 콘텐츠 주소 지정 레지스트리에 S3 버킷 버전 관리가 필요한 이유는 무엇인가요?
버전 관리는 바이트가 제자리에서 절대 바뀌지 않으므로 블롭의 변경을 추적하기 위한 것이 아닙니다. 삭제를 안전하게 만들기 위한 것입니다. 가비지 컬렉션은 참조되지 않는 블롭을 제거해야 하지만, 참조는 MySQL에 있고 바이트는 S3에 있으며 두 시스템을 아우르는 트랜잭션은 없습니다. 이 틈으로 인해 GC가 삭제하기로 결정하는 바로 그 순간 클라이언트가 블롭을 다시 푸시할 수 있습니다. 버전 관리는 “이 키를 삭제하라”를 “내가 검사한 정확히 그 버전을 삭제하라”로 바꾸므로, GC는 이전 버전을 제거하고 새로 푸시된 버전은 그대로 남깁니다.
에이전트가 TLA+ 명세를 작성한다면, 모델이 구현체와 일치한다고 어떻게 신뢰할 수 있나요?
완전히 신뢰할 수는 없으며, 시작 단계에서는 괜찮습니다. 모델 검사기는 정확성 증명이 아니라 신뢰를 조절하는 다이얼 하나를 더하는 것입니다. 읽을 수 있는 부분인 불변 조건부터 시작해, 그것이 의도한 바를 말하는지 물으십시오. 그런 다음 전이를 화이트박스로 읽고 의문을 제기할 때까지 바깥으로 확장하십시오. 모델은 여기서 정말 두 워커를 허용하는가, 이것이 재시도 동작과 일치하는가를 말입니다. 불일치의 비용이 크다면, 그때 명세 자체의 결함을 찾는 데 실제 시간을 투자하면 됩니다.
언제 시스템을 TLA+로 모델링할 가치가 있나요?
경쟁하는 프로세스, 까다로운 트랜잭션 경계, 타이밍을 두고 경쟁하는 자율 워커, 또는 공유 트랜잭션 없이 여러 시스템에 걸친 작업이 있을 때 사용하십시오. 고유한 인터리빙이 있는 곳이 바로 여기이며, 테스트는 생각해 낸 순서만 실행하므로 정확히 이런 것을 놓칩니다. 평범한 CRUD 엔드포인트에는 모델 검사기가 필요하지 않습니다.
Wito Delnat
Depot의 스태프 엔지니어