LLM 시대에 효과적으로 TLA+를 사용하기 위한 핵심 사고방식: 추상화, 전역 공유 메모리, 로컬 가드, 불변식, 단계적 정제, 원자성 정제, 그리고 멘털 모델의 공유.
LLM의 시대에는 TLA+를 쓰고, 읽고, 배우는 데 더 이상 문법이 병목이 아닙니다. 사람들은 알고리즘에 대한 Google Docs 설명으로부터 직접 TLA+ 모델과 반례를 생성하는 것만으로도 이미 가치를 얻고 있습니다. TLA+의 우발적 복잡성, 즉 그 문법과 도구 체인은 사라지고 있습니다.
하지만 본질적 복잡성은 남아 있습니다. 어디서 모델을 시작할지, 무엇을 무시할지, 그리고 올바른 추상화를 어떻게 고를지 아는 일입니다. 이것은 모델링 판단력이며, 가르치기 가장 어려운 기술입니다. 엔지니어들은 코드, 제어 흐름, 로컬 상태로 사고하도록 훈련받습니다. TLA+는 당신을 다른 모드로 밀어 넣습니다. 수학적이고, 선언적이며, 전역적인 모드입니다. 어떻게 달성할지를 쓰는 것이 아니라, 무엇이 성립해야 하는지를 명세합니다. 이 전환에 익숙해지고 나면, 키보드에서 떨어져 있을 때조차 시스템을 생각하는 방식이 달라집니다.
관련 글에서, 저는 8개의 산업 프로젝트에서 얻은 교훈을 바탕으로 TLA+를 설계 가속기로 설명했습니다. 여기서는 더 깊이 들어가서 효과적인 TLA+ 활용 뒤에 있는 멘털 모델을 분명히 드러내고 싶습니다. 이것들은 TLA+ 전문가들이 암묵적으로 적용하는 사고 패턴이며, 수년에 걸쳐 스며들듯 습득되는 종류의 지식입니다. 저는 이것들을 명시적이고 실천 가능하게 만들어 보려 합니다.
멘털 모델은 다음과 같습니다:
추상화는 주의를 흐트러뜨리는 요소를 피하기 위한 강력한 도구입니다. abstract라는 단어의 어원은 라틴어로 "잘라내어 떼어낸다"는 뜻에서 왔습니다. 추상화를 통해 복잡한 시스템에서 프로토콜만 도려내고, 불필요한 세부사항을 생략하며, 복잡한 시스템을 유용한 모델로 단순화할 수 있습니다. 모든 것을 모델링할 필요는 없습니다. 가치의 대부분은 무엇을 무시해야 하는지 아는 데서 나옵니다. 생략이 기본값입니다. 어떤 구성요소를 빼면 당신의 추론 목표가 깨질 때에만 그것을 추가하십시오.
추상화는 무엇을 버려야 하는지 아는 예술입니다. 당신은 조사하고 싶은 프로토콜에 초점을 맞추기 위해 횡단적으로 잘라낼 수 있습니다. 분산 시스템의 일관성 모델에 관심이 있다면, 통신의 메커니즘이 불필요한 주의 분산이라면 그것을 추상화해 버릴 수 있습니다. 복제 프로토콜에 관심이 있다면, 클라이언트 상호작용을 추상화해 버릴 수 있습니다. 우리 산업 현장의 경험에서 나온 두 가지 예를 보겠습니다.
Leslie Lamport는 Paxos를 어떻게 도출했는지 설명하면서 이것을 아름답게 보여주었습니다. 그는 가장 추상적인 명세에서 시작했습니다. 투표 배열에 기반해 합의를 정의하는 방식이었습니다. 그의 표현을 빌리면:"Paxos로 이어진 사고 과정을 나는 기억하지 못한다. 하지만 서로에게 메시지를 보내는 컴퓨터들 위에서 실행된다는 것은 무관한 세부사항이라는 점은 알고 있었다. 나는 오직 프로세스들의 집합과 그들이 서로에 대해 무엇을 알아야 하는지만 생각하고 있었다. 메시지로부터 그 정보를 어떻게 얻는지는 나중에 온 쉬운 부분이었다. 처음에 내가 가지고 있었던 것은, 훨씬 뒤에 내가 Voting 알고리즘이라고 설명하게 된 그것이었다."
TLA+는 엔지니어들에게 추상화의 기술과 분산 시스템을 생각하고 추론하는 올바른 방식을 가르치는 데 유용합니다. 모델링 과정 자체가 당신에게 이렇게 묻게 훈련시킵니다. 내가 신경 쓰는 행위의 단면은 무엇인가, 그리고 무엇을 안전하게 무시할 수 있는가? 그리고 TLA+는 촘촘한 피드백 루프를 가진 빠른 프로토타이핑 도구를 제공하기 때문에, 즉 모델을 쓰고, 검사하고, 수정하는 과정을 통해, 실제 시스템을 만들고 디버깅하는 방식보다 훨씬 더 빠르게 설계 경험을 축적하게 됩니다.
TLA+는 의도적인 허구를 제공합니다. 모든 프로세스가 읽고 쓸 수 있는 전역 공유 메모리입니다. 이 허구는 그 계산 모델의 토대이며, 이를 이해하는 것은 TLA+식 사고에 필수적입니다.
TLA+에서 프로그램은 두 가지로 이루어집니다. (1) 전역 상태 공간을 정의하는 변수들의 집합, 그리고 (2) 한 상태에서 다음 상태로 전이시키는 유한한 액션들의 집합입니다. 이것은 모든 것이 술어, 즉 불리언으로 매핑되는 함수라는 상태 중심 추론입니다. 이 접근법은 불변식 기반 사고를 촉진합니다. (멘털 모델 4를 보십시오.)
각 액션은 Sir Tony Hoare의 삼중항을 따릅니다: {state} action {state'}. 액션의 실행은 어떤 술어, 즉 "가드"가 참일 때에만 가능합니다. 예를 들어: x > 0 → x := 0; y := y + 1. 또는 TLA+ 표기에서는:
/\ x > 0
/\ x' = 0
/\ y' = y + 1
가드는 상태 공간 위의 술어입니다. 어떤 상태에서 가드가 참이면, 그 액션은 그 상태에서 "활성화되었다"고 말합니다. 프로그램은 초기 술어를 만족하는 임의의 상태에서 시작합니다. 그런 다음 활성화된 액션 하나가 비결정적으로 선택되어 원자적으로 실행됩니다. 이 과정은 무한히 반복됩니다. 선택된 액션의 가드가 거짓이라면, 그것은 단순한 skip이며 상태를 바꾸지 않습니다.
전역 공유 메모리 (GSM) 모델은 이런 스타일의 추론과 자연스럽게 맞아떨어집니다. 현재 상태를 읽고 새 상태를 설치하면 됩니다. 채널도, 메시지 직렬화도, 관리해야 할 프로세스 경계도 없습니다. 이는 guarded-command 모델에 맞는 모델을 쓰는 가장 최소한의 방식입니다. 하지만 변수를 정의할 때는 절제해야 합니다. 변수 하나하나가 상태 공간을 기하급수적으로 폭발시키기 때문입니다. 그 대가로 안전성과 활성은 전역 상태 위의 간결한 술어가 됩니다. 당신의 프로그램은 불변 집합, 즉 좋은 상태들의 집합을 정의하며, 그 바깥으로 전이해서는 안 됩니다.
채널, 메시지 직렬화, 네트워크 토폴로지를 모델링할 필요는 없습니다. 당신이 추론하려는 대상이 바로 그런 것들일 때만 필요합니다. "로컬에 가까운" 가드와 분명히 로컬인 변수 대입을 유지한다면 GSM을 메시지 패싱으로 매핑하는 것도 가능합니다. 그런데 전역 공유 상태 공간에서 "로컬 변수"란 무엇을 뜻할까요? 흔한 방법은 노드별 인덱스를 사용하는 것입니다. 그래서 vote[i]는 노드 i의 투표를 가리킵니다. 전역 변수는 투표 배열이고, 로컬 버전은 vote[i]입니다. 모든 것은 수학이며, 수학에는 추상화가 필요합니다. 전역 공유 메모리라는 허구를 중심으로 형성된 TLA+의 계산 모델은 당신이 올바른 수준의 추상화에서 추론할 수 있게 해줍니다.
TLA+의 전역 공유 메모리라는 허구는 추론에 강력하지만, 함정도 만듭니다. 실제 프로세스라면 원자적으로 관찰할 수 없는 전역 상태를 읽는 가드를 너무 쉽게 쓸 수 있기 때문입니다. 이것은 가장 흔한 모델링 오류 중 하나입니다. 서로 다른 세 노드가 동시에 무엇을 했는지를 검사하는 가드는 "불법적인 지식"입니다. 실제 분산 시스템에서 어떤 단일 노드도 그 모든 것을 한 번에 알 수 없기 때문입니다. 따라서 별도의 리뷰 단계에서 각 액션마다 이렇게 물어야 합니다. 실제 노드는 행동을 결정할 때 어떤 정보를 정말로 알 수 있는가?
그렇다면 가드를 어떻게 로컬하게 바꿀 수 있을까요? 민간에 떠도는 정리 하나가 있습니다. 바로 바로 옆 이웃을 읽는 것은 괜찮다는 것입니다. 왜냐하면 그것은 메시지 패싱으로 매핑될 수 있기 때문입니다. (hygenic dining philosophers를 떠올려 보십시오.) 본질적으로 이는 한 단계 더 간접화를 추가하고 프록시 변수를 두는 것으로 귀결되며, 결국 잠금을 뜻합니다. 잠금은 성능에 좋지 않습니다. 그리고 멘털 모델 6에서 저는 원자성을 정제하고 구현이 책임 있게 자유를 누릴 수 있도록 가능한 한 많은 동시성을 허용해야 한다고 주장할 것입니다. 그렇다면 우리는 무엇을 해야 할까요?
핵심 통찰은 가드에 사용할 안정적이거나, 단조적이거나, 혹은 로컬하게 안정적인 술어를 찾아내려 노력하는 것입니다. 제 "분산 시스템 설계 힌트" 글에서, 제가 "단조성을 받아들여라"라고 말할 때 정확히 이것을 염두에 두고 있습니다: "분산 시스템에서 조정을 효율적이고 안전하게 수행하려면, 통찰은 거의 항상 문제를 단조적인 문제로 변환하는 데 있다."
여기서부터는 미묘해지며, 좀처럼 명시되지 않는 비전수적 지식과 맞닿습니다. 이것은 이론에 가까운 쪽의 분산 시스템을 수년간 다뤄 본 뒤에야 직관적으로 얻게 되는 종류의 것입니다. 당신의 지도교수는 이를 직관으로 알고 있었고, 그들의 지도교수도 그랬으며, 그들은 이것을 가리키는 어휘상의 지름길은 발전시켰지만 완전히 명시적으로 만들지는 않았습니다. UC Berkeley의 CALM (Consistency As Logical Monotonicity) 연구는 Dedalus 같은 언어에 기반해 이것을 좀 더 구체화했지만, 그 기본 요지는 추상적인 전역 상태 추론의 수준에 존재합니다.
우리의 "Slow is Fast" 논문에서, 우리는 이 직관을 액션을 "느린 것"과 "빠른 것"으로 나누어 형식화했습니다. 느린 액션의 가드는 노드의 정보가 조금 오래되었더라도 참으로 남습니다. 이는 가드가 안정적인 술어이거나, 오직 로컬 변수에만 의존하거나, 혹은 로컬하게 안정적인 술어이기 때문입니다. 즉 그 술어를 거짓으로 만들 수 있는 것은 그 노드 자신의 액션뿐입니다. 반대로 빠른 액션은 가드를 평가하기 위해 신선한 전역 상태를 요구합니다. 핵심 결과는 이것입니다. 가드를 로컬하게 안정적으로 만들 수 있다면, 프로토콜은 더 적은 조정을 필요로 하고 통신 지연을 우아하게 견딥니다. 그래서 느림이 곧 빠름입니다.
이것은 쉬운 일이 아닙니다. Ernie Cohen은 이 기술을 내면화하고 있었고, 프로토콜 탐색에서 활용할 수 있는 단조적이거나 로컬하게 안정적인 술어를 빠르게 찾아낼 수 있었습니다. 어떤 사람들은 이런 사고방식 속에 너무 완전히 살고 있어서, 마치 물속의 물고기처럼 그것을 어떻게 말로 설명해야 하는지조차 모를 수 있습니다. (좋은 예로, "전역 공유 메모리 허구"라는 표현은 Marc Brooker가 제게 짚어준 것입니다. 때로는 내부자들이 당연하게 여기는 것에 이름을 붙여 주는 사람은 약간의 외부자입니다.) TLA+ 모델링을 위한 실질적 요점은 이것입니다. 가드를 쓸 때, 그 가드가 의존하는 정보가 오래될 수 있는지, 그리고 그렇다면 그 가드에 따라 행동하는 것이 여전히 안전한지를 자문하십시오. 가드를 단조적이거나 로컬하게 안정적인 술어에 의존하도록 만들 수 있다면, 당신의 프로토콜은 더 견고하고, 더 동시적이며, 올바른 분산 구현에 더 가까워질 것입니다.
Lamport의 Paxos 도출은 이것을 아름답게 보여줍니다. 그는 가장 단순한 합의 명세에서 시작합니다. chosen은 빈 집합으로 시작해 singleton 로 전이합니다. 그것이 전체 다음 상태 공식입니다. 그런 다음 acceptor가 투표하고 과반수가 어떤 값에 투표하면 그 값이 선택된다고 하는 voting 알고리즘으로 정제하고, 거기서 발생하는 문제들을 처리하기 위해 다시 Paxos로 정제합니다. (예를 들어 N개의 acceptor가 에 투표하고, N개가 에 투표하며, 남은 acceptor 하나가 실패하면 어떻게 될까요?) 각 정제 단계마다 가드는 더 로컬해집니다. Paxos에서 어떤 acceptor가 투표해야 하는지에 대한 가드는 로컬 지식에 의존합니다. 이 acceptor가 어떤 ballot들에 참여했는가 하는 점입니다. ballot 번호의 단조 구조는 이 로컬 지식이 무효가 되지 않도록 보장합니다. 일단 어떤 acceptor가 투표 진행 상황에 대해 어떤 사실을 알게 되면, 그 사실은 영구적입니다. 이것이 Paxos가 비동기성과 장애에도 불구하고 동작하는 이유입니다.
당신은 재미 삼아 모델링을 한 것이 아니라 목적을 가지고 했습니다. 당신은 프로토콜에 대한 추론 통찰에 도달하고 싶어 하며, 불변식은 그 통찰이 증류된 형태입니다. 불변식 기반 추론은 비작동적입니다. 실행 경로를 따라가고 happy-path로 생각하는 대신, "무엇이 올바르게 되어야 하는가?"를 묻습니다. 경계 조건을 명세하면, 모델 체커가 가능한 모든 인터리빙을 탐색해 그것을 검증합니다.
좋은 불변식을 증류하는 데 시간을 들이십시오. 그것들은 여러 방식으로 당신을 도와주기 때문입니다. 프로토콜 변형을 탐색할 때 지침이 되어 무엇을 바꿀 수 있고 바꿀 수 없는지 알려줍니다. 구성요소를 조합할 때 계약처럼 작동하여 각 부분이 다른 부분에 무엇을 보장하는지 정의합니다. 구현의 런타임 assertion과 테스트 oracle로 직접 번역됩니다. 그리고 내결함성을 추가할 때 필수적입니다. 불변식을 알고 나면, 장애 이후 어디까지 복구해야 하는지 알게 되고, 그것을 다시 성립시키는 복구 액션을 설계할 수 있기 때문입니다.
불변식 작성은 여전히 대부분 수작업입니다. LLM은 이것에 약합니다. 불변식은 명세에서 가장 신호 밀도가 높은 부분이기 때문입니다. 그것들은 이 프로토콜이 무엇을 보장해야 하는지에 대한 당신의 이해를 농축합니다. 그것을 올바르게 만든다는 것은 당신이 그 문제에 대해 폐쇄를 얻었다는 뜻입니다.
TLA+와 형식 기법에 처음 접하는 사람들은 반복적으로 이 단계에서 실패합니다. 저도 가끔 어려움을 겪습니다. 특히 익숙하지 않은 도메인에 들어갈 때는 먼저 시간을 치르고 더 깊이 생각해 이해를 얻어야 합니다. 가장 흔한 실패 양상은 "자명한 불변식"을 쓰는 것입니다. 프로토콜이 무엇을 하든 항상 참인 것을 쓴다면, 당신은 헛되이 명세를 쓴 셈입니다. 또 다른 실패는 "최종 상태"를 불변식과 혼동하는 것입니다. 불변식은 최종 상태에서만이 아니라 도달 가능한 모든 상태에서 성립해야 합니다. 우리는 귀납적 불변식까지 기대하는 것은 아닙니다. 그것은 훨씬 더 어렵고, 또한 더 가치가 큽니다. 형식적 증명이 그것으로부터 쉽게 따라오기 때문입니다. 하지만 이해를 보여주고 추가 탐색의 발판이 되는, 적당히 빡빡한 불변식, 그것이 당신이 목표로 해야 할 것입니다.
안전성 속성, 즉 시스템이 해도 되는 일에만 멈추지 마십시오. 활성 속성도 쓰십시오. 즉 시스템이 결국 해야 하는 일입니다. <> Termination과 Init ~> Solution 같은 속성을 점검하는 것은 중요합니다. 요청은 완료되는가? 리더는 등장하는가? 많은 "올바른" 모델은 조용히 영원히 아무것도 하지 않습니다. 안전성을 결코 위반하지 않지만 진전도 없는 모델은 쓸모가 없습니다. 활성 검사는 멈춰 버리는 경로, 지나치게 제약된 명세, 그리고 결코 활성화되지 않는 액션을 잡아냅니다.
앞서의 예로 돌아가 봅시다. Lamport의 Paxos 도출에서 각 정제 수준의 불변식은 많은 것을 보여줍니다. Consensus 수준에서 안전성 불변식은 단순히 최대 하나의 값만 선택된다는 것입니다. (Cardinality(chosen) <= 1) Voting 수준에서는 chosen이 어떤 ballot가 존재하여 acceptor의 quorum이 모두 그 값에 투표한 값들의 집합으로 정의됩니다. (chosen == {v \in Value : \E b \in Ballot : ChosenAt(b, v)}) Voting 알고리즘의 안전성은 두 규칙에 기대고 있습니다. (1) 같은 ballot에서 서로 다른 acceptor들이 서로 다른 값에 투표할 수 없다. (2) acceptor는 ballot 에서 값 가 안전할 때에만 에 투표할 수 있다. 이 불변식들은 빡빡하고, 자명하지 않으며, Paxos까지 내려가는 전체 정제 사슬의 발판이 됩니다. 그것들은 왜 합의가 동작하는지에 대한 진짜 이해를 보여주며, 그것이 제가 말하는 "문제에 대한 폐쇄"입니다.
TLA+의 가장 큰 강점 중 하나는 프로토콜 변형을 빠르게 탐색할 수 있게 해준다는 점입니다. 핵심 기법은 단계적 정제입니다. 문제의 가장 추상적인 명세에서 시작한 뒤, 구현 세부사항을 점진적으로 추가하면서 각 단계마다 그 정제가 상위 수준의 불변식을 보존하는지 검증합니다.
전형적인 예는 다시 Lamport의 Paxos 도출입니다. 추상적인 Consensus 명세는 빈 집합에서 singleton으로 전이하는 단일 변수 chosen을 정의합니다. 그런 다음 중간 단계의 Voting 모델이 정의되고, 그것이 Consensus의 정제임이 보입니다. 이 모델은 투표가 어떤 성질을 만족해야 하는지를 설명하지만, acceptor가 그것을 어떻게 구현하는지는 말하지 않습니다. 마지막으로 Paxos 모델은 메시지 패싱, ballot 리더, 그리고 2단계 프로토콜을 추가함으로써 Voting을 정제합니다. 각 수준에서 정제는 세부사항, 즉 ballot, quorum, 메시지를 추가하면서도 상위의 안전성 속성을 보존합니다.
정제는 추상화의 핵심에 있으며 TLA+의 초석입니다. TLA+에서 정제는 단순히 함의입니다. 구체 시스템의 행위는 추상 시스템이 허용하는 행위의 부분집합이어야 합니다. 이것은 구체 명세 안에 추상 명세의 인스턴스를 선언하고, 구체 시스템의 모든 행위가 추상 시스템이 받아들이는 행위인지 TLC로 검증함으로써 점검합니다. 불변식 검사조차 변장한 정제입니다. 시스템 모델이 이 불변식 공식을 구현하는가를 묻는 것이기 때문입니다.
단계적 정제의 큰 장점은 프로토콜 변형을 탐색하고 싶을 때 처음부터 다시 시작하지 않아도 된다는 점입니다. 적절한 추상화 수준으로 다시 올라가 정제 단계 하나를 바꾸면, 동일한 상위 명세를 만족하는 다른 프로토콜을 얻을 수 있습니다. 이것이 체계적인 설계 공간 탐색입니다. 예를 들어 LeaseGuard에서는, 우리는 Raft를 위한 lease 프로토콜을 초기에 모델링하기 시작했습니다. 추상 명세를 정제하는 과정에서 우리는 예상하지 못했던 두 가지 최적화를 발견했는데, 그중 하나가 inherited lease reads였고, 여러 수준의 추상화에서 생각하지 않았다면 아마 발견하지 못했을 것입니다.
여기서 흔한 실패 패턴은 어떤 세부 수준에 갇혀 모서리 사례를 하나씩 덧대어 패치하는 것입니다. 이것은 구현 마인드셋이 모델링으로 새어 들어온 경우입니다. 이런 일이 생기면, 다시 위로 올라가십시오. 저는 이것을 Aurora DSQL의 Secondary Index 프로젝트에서 보았습니다. 한 엔지니어의 설계는 덧붙이기의 방식으로 자라나고 있었고, 각 코너 케이스 패치는 새로운 코너 케이스를 만들고 있었습니다. TLA+는 다른 접근을 강제했습니다. 보조 인덱스가 추상적으로 무엇을 보장해야 하는지를 명세하고, 그런 다음 정제를 통해 해법 공간을 탐색하는 방식이었습니다. 주말 하나 동안, TLA+ 경험이 전혀 없었음에도 그 엔지니어는 여러 가지 변형을 작성했습니다. 교훈은 이것입니다. 구현이 아니라 행위를 명세하고, 그다음 정제를 통해 서로 다른 "어떻게"의 선택지를 탐색하라.
지나치게 큰 원자적 액션은 경쟁 상태를 숨깁니다. 당신의 TLA+ 액션이 한 단계에서 원자적으로 열 가지 일을 한다면, 동시성을 카펫 아래로 쓸어 넣고 있는 것입니다. 모델은 올바르게 보이겠지만, 실제 시스템이 맞닥뜨릴 인터리빙을 표현하지는 못합니다. 액션은 정확성이 허용하는 한 가능한 한 세분되어야 합니다. 더 작은 단계는 프로토콜이 견뎌야 하는 인터리빙을 드러내고, 불변식을 더 의미 있게 만듭니다.
실용적인 접근은 먼저 거친 입도로 시작해 정확성을 확립한 뒤, 체계적으로 액션을 더 작은 단계들로 쪼개고 안전성이 여전히 유지되는지 검증하는 것입니다. 이것은 액션의 세분성에 적용한 단계적 정제입니다. 각 분할은 인터리빙 공간을 증가시키며, 바로 그 지점에서 TLC가 진가를 발휘합니다. 간섭의 표면적은 폭발할 수 있지만, TLC는 당신의 불변식이 유지되는지 철저히 검사할 것입니다.
여기서 목표는 구현에 가능한 최대의 자유를 주어 재배열과 병렬화를 허용하면서도, 그런 동시성 아래에서 프로토콜이 여전히 올바름을 검증하는 것입니다. 명세에서 세분된 원자성은 구현이 가드 조건을 존중하는 한 어떤 순서로든 연산을 스케줄할 수 있음을 뜻합니다.
우리의 StableEmptySet 프로젝트는 좋은 예입니다. Ernie Cohen은 분산 잠금을 피하기 위해 원자적 액션을 가능한 가장 미세한 세분성까지 밀어붙였고, 그 결과 프로토콜은 잠금 기반 설계보다 더 높은 동시성을 갖게 되었습니다. 인터리빙 표면적은 늘어났지만, TLC는 전혀 힘들어하지 않고 이를 처리했습니다. 여기서 멘털 모델 3의 "느림이 곧 빠름" 통찰이 다시 연결됩니다. 가드를 로컬하게 안정적인 술어에 의존하도록 정제하면, 액션을 잘게 쪼개더라도 불법적인 지식을 도입하지 않을 수 있습니다. 단계 사이에서 전역 상태가 바뀌더라도 가드는 여전히 유효하기 때문입니다.
TLA+ 모델은 의사소통 도구이기도 합니다. 잘 쓰인 명세는 프로토콜의 정확하고 실행 가능한 문서 역할을 하며, 산문 명세나 코드 주석으로는 담아낼 수 없는 방식으로 설계 의도를 포착합니다.
AWS에서 제가 Aurora DSQL의 분산 트랜잭션 프로토콜에 대한 첫 번째 TLA+ 모델을 썼을 때, 그 모델의 가치는 곧 정확성에 대한 신뢰를 넘어서게 되었습니다. 그것은 큰 팀을 위한 의사소통의 기준점 역할을 했습니다. 우리가 추가적인 형식 기법 지원을 요청했을 때, TLA+ 모델은 새 팀원의 온보딩을 빠르게 하고 모두가 프로토콜 설계에 대해 같은 이해를 유지하도록 도왔습니다. 설계 문서의 모호한 산문을 두고 논쟁하는 대신, 팀은 명세 안의 특정 액션과 불변식을 가리킬 수 있었습니다.
MongoDB 분산 트랜잭션 작업은 이것을 다시 확인해 줍니다. 우리는 프로토콜이 실제 운영에 들어간 지 여러 해가 지난 뒤에야 그것의 첫 번째 모듈형 TLA+ 명세를 작성했습니다. 이제 그 모델은 프로토콜이 실제로 무엇을 보장하는지에 대한 권위 있는 설명 역할을 하며, 전체로서 추론하기 어려워진 시스템에 명확성을 가져다줍니다.
그러므로 명세는 단지 TLC만을 위해서가 아니라 사람을 위해 쓰십시오. 명확한 액션 이름을 사용하고, TypeOK 불변식을 일찍 작성하십시오. 그것들은 당신의 데이터 모델에 대한 실행 가능한 문서 역할을 합니다. 그리고 중요한 모든 속성을 명시적인 불변식으로 만드십시오. 잘 구조화된 명세는 수천 줄의 구현 코드보다 프로토콜 의도를 더 분명하게 전달합니다. 오류 처리, 직렬화, 설정의 잡음을 걷어내고 본질적 논리만 보여주기 때문입니다.
Spectacle 같은 도구는 TLA+의 상태 공간과 실행 추적을 시각화할 수 있어, 수학적 정밀함과 엔지니어들이 잘 발휘하는 작동적 직관 사이의 간극을 메워 줍니다. TLA+는 가장 순수한 지적 즐거움 중 하나입니다. 복잡한 분산 시스템을 그 본질적 논리로 환원하는 일이기 때문입니다. 당신의 모델에 대해 글을 쓰고, 발표하고, 가르치는 데 활용함으로써 그 즐거움을 다른 사람들과도 나누어 주십시오.
LLM이 우리의 코드를 더 많이 작성하게 될수록, 설계와 추론을 위한 TLA+의 가치는 더욱 커질 것입니다. TLA+는 시스템을 구축하기 위한 AI+형식 기법 스택의 초석이 될 잠재력을 가지고 있습니다. 여기서 제가 설명한 멘털 모델은 그 미래의 토대입니다. 추상화를 숙달하고, 전역 공유 메모리 모델을 받아들이고, 로컬 가드로 정제하고, 좋은 불변식을 도출하고, 정제를 통해 대안을 탐색하고, 원자성을 과감하게 정제하고, 우리의 멘털 모델을 공유함으로써, 우리는 AI 시대에 더 나은 분산 시스템을 설계하기 위한 TLA+의 완전한 힘을 끌어낼 수 있습니다.
