Formal Specifications & TLA+

1. Overview

형식 명세와 TLA+ (Formal Specifications & TLA+)는 복잡한 병렬/분산 시스템에서 인간의 직관으로는 도저히 찾아낼 수 없는 '경쟁 상태(Race Condition)'나 '데드락(Deadlock)' 버그를, 코드를 짜기 전 설계 단계에서 수학적 논리로 100% 찢어 발겨 증명하는 극강의 '설계 물리학'입니다.

학습자는 상태 기계(State Machine) 모델을 통해 시스템의 모든 가능한 상태 공간(State Space)을 논리 기호로 정의하는 **형식 명세(Formal Specification)**를 익힙니다. 특히 Leslie Lamport가 창시한 **TLA+(Temporal Logic of Actions)**를 활용하여, 시간에 따라 변하는 시스템의 동적(Dynamic) 특성을 수학 공식으로 압축하고 모델 체커(TLC)로 무결성을 자동 검증하는 방법을 배웁니다. 이를 통해 AWS나 Azure 같은 거대 클라우드 인프라 설계자들이 어떻게 치명적 시스템 붕괴를 사전에 차단하는지, 그 하이엔드 아키텍처 검증 능력을 확보합니다.

2. Scope & Boundaries

In-Scope

• 상태 기계와 전이 (State Machines): 초기 상태(Initial State), 다음 상태 관계(Next-State Relation), 변수와 불변성(Invariants).
• 시제 논리 역학 (Temporal Logic): 항상 참($\Box$, Always), 언젠가 참($\diamond$, Eventually), Liveness와 Safety 속성.
• TLA+ 설계 물리학 (TLA+ Modeling): TLA+ 문법 기반의 상태 명세, Action 정의, 비결정론적 전이(Nondeterministic Transitions).
• 자동 모델 체킹 (Model Checking): TLC 모델 체커를 이용한 유한 상태 공간 완전 탐색 및 반례(Counterexample) 도출.

Out-of-Scope

• 프로그래밍 언어 종속적 단위 테스트: JUnit이나 PyTest를 이용한 코드 레벨의 테스트 작성 $\rightarrow$ 09-04. QA & Quality Assurance 영역.
• 운영체제 커널의 C 코드 구현: 스핀락(Spinlock)이나 세마포어(Semaphore)를 C 언어로 짜기 $\rightarrow$ 03-02. Process & Concurrency 영역.

Boundaries

• TLA+ vs. Program Correctness (01-02-04): 프로그램 정확성(01-02-04)이 "이미 짜여진 코드(알고리즘)가 입력-출력 관계를 만족하는가(Hoare Logic)"를 본다면, TLA+는 "코드를 한 줄도 짜기 전에, 분산 시스템의 아키텍처 설계 자체에 모순(Deadlock)이 없는가"를 우주적 관점에서 검증하는 상위 레벨의 수학적 모델링입니다.

3. Counterexample

• 동시성 버그의 테스트 맹신 (Testing Fallacy in Concurrency): "유닛 테스트 1,000개를 통과했으니 우리 시스템의 분산 락(Lock) 알고리즘은 완벽해"라고 믿는 무지. 동시성 환경에서는 네트워크 지연, 스레드 스위칭 타이밍에 따라 수조($10^{12}$) 단위의 상태 공간(State Space)이 발생합니다. 테스트 코드로 이 중 몇 만 개를 찔러보는 것은 태평양에서 바늘 하나를 찾는 꼴이며, 형식 명세로 '데드락이 발생 가능한 상태 공간이 물리적으로 존재함'을 수학적으로 증명(TLC)하지 않으면 프로덕션에서 반드시 터집니다.
• Liveness와 Safety의 혼동 (Property Confusion Fallacy): "서버가 절대 죽지 않는다(Safety)"는 불변성(Invariant)만 증명해놓고 시스템이 완벽하다고 착각하는 행위. 서버가 죽지는 않지만 '영원히 응답을 주지 않는 무한 대기 상태(Liveness 결여, Starvation)'에 빠진다면 시스템은 붕괴한 것과 같습니다. TLA+에서는 $\Box(Request \rightarrow \diamond Response)$ 같은 시제 논리로 Liveness를 반드시 증명해야 합니다.

4. Prerequisites

• 명제 및 술어 논리 (Basic): TLA+의 모든 명세는 명제 논리(AND, OR)와 술어 논리($\forall, \exists$)의 수학 기호로 작성되므로 이를 읽고 쓸 수 있어야 합니다. (01-02-01 PPL)

5. Learning Map

6. Learning Topics

Basic

Core Topic 01: 상태 기계와 전이 역학 (State Machines & Transitions)

• Why to Learn: 아무리 거대한 시스템(AWS S3, 은행 송금)이라도 결국 "변수들의 현재 값"과 "그 값을 바꾸는 동작"이라는 2개의 축으로 모델링하여 두뇌 용량을 초과하는 복잡도를 박살내기 위함입니다.
• What to Learn:
  • Concepts: 상태(State), 변수(Variables), 초기 상태(Init), 다음 상태(Next).
  • Skills: 상태 전이 관계(State Transition Relation), 프라임 기호($x'$: 다음 상태의 x값).
  • Tools: State-space Graph.
  • Trade-offs: 코드를 줄줄이 읽으며 흐름을 파악하는 절차적 사고 vs 시간 개념을 배제하고 $x' = x + 1$처럼 전이 규칙(Action)만 정의하여 모든 런타임 분기를 수학 방정식으로 가둬버리는 선언적 사고의 추상화 장벽.
• How to Learn:
  • 1단계: 은행 계좌에서 A가 B에게 송금하는 행위를, 상태 전이 방정식 (A' = A - 10) AND (B' = B + 10)으로 선언하고, 이 방정식이 참(True)일 때만 물리적으로 시스템 상태가 넘어간다는 점을 해부합니다.
  • 2단계: 네트워크 패킷 손실로 인해 A의 돈은 깎였지만 B에게 도착하지 않는 비결정론적 상태(Nondeterminism)를 분기 식(OR)으로 모델링하여 분산 시스템의 불안정성을 도식화합니다.
• Implement: 2개의 프로세스가 동시에 공유 자원에 접근하려는 상황을 가정하여, 초기 상태 Init과 각 프로세스가 실행될 때의 상태 변화 Next를 TLA+ 식 문법 형태의 파이썬 객체로 추상화하여 상태 트리를 출력하는 시뮬레이터.

Recommended

Core Topic 02: 불변성과 Safety 속성 (Invariants & Safety)

• Why to Learn: "잔액은 절대 음수가 될 수 없다"나 "두 프로세스가 동시에 임계 구역에 들어갈 수 없다"와 같은 우주 불변의 법칙(Safety)이 모든 상태 공간에서 지켜지는지 100% 증명하기 위함입니다.
• What to Learn:
  • Concepts: Safety Property ("Something bad never happens"), 불변성(Invariant), 상태 공간 탐색.
  • Skills: 수학적 귀납법(Mathematical Induction), 상태 공간 그래프에서의 타당성 검사.
  • Tools: Assertions.
  • Trade-offs: 테스트 코드로 100만 번 무작위 실행하여 불변성을 확인하는 휴리스틱 신뢰도 vs 수학적 귀납법(초기 상태가 참이고, N번째가 참일 때 N+1도 참이다)으로 시스템의 붕괴 가능성을 0%로 차단하는 절대적 안정성.
• How to Learn:
  • 1단계: 송금 시스템의 불변성인 "전체 계좌의 총합은 언제나 일정하다($A + B = \text{Total}$)"라는 Safety 속성을 정의하고, Next 전이가 이 불변성을 깨뜨릴 수 있는지 귀납법으로 증명합니다.
  • 2단계: 다익스트라의 뮤텍스(Mutex) 알고리즘을 상태 기계로 그리고, "두 개의 플래그 변수가 동시에 1이 되는 상태 노드(State Node)로 가는 화살표가 아예 존재하지 않는다"는 것을 위상 수학적으로 뜯어봅니다.
• Implement: 현재 상태 State와 전이 함수 Action을 받았을 때, BFS(너비 우선 탐색)를 돌며 상태 그래프를 탐색하다가 내가 정의한 불변성 Invariant()가 거짓(False)이 되는 단 하나의 노드라도 발견하면 즉시 폭발(Panic)하는 마이크로 모델 체커 작성.

Practical

Core Topic 03: 시제 논리와 Liveness (Temporal Logic)

• Why to Learn: 교착 상태(Deadlock)는 피했지만 서로 양보만 하다가 아무 일도 안 하는 기아 상태(Starvation/Livelock)에 빠지는 치명적 버그를 '시간의 흐름'을 묘사하는 논리로 잡아내기 위함입니다.
• What to Learn:
  • Concepts: Liveness Property ("Something good eventually happens").
  • Skills: 항상 참($\Box$, Always), 언젠가 참($\diamond$, Eventually), 약한 공정성(Weak Fairness), 강한 공정성(Strong Fairness).
  • Tools: Temporal Logic Operators.
  • Trade-offs: Liveness 검증을 포기하고 단순 Safety만 챙겨서 빠른 모델링으로 타협하기 vs 무한히 실행되는 루프(Infinite execution path) 속에서 교착 상태를 완벽히 증명하기 위해 상태 그래프의 순환(Cycle) 궤도까지 분석하는 살인적인 연산 오버헤드 감수.
• How to Learn:
  • 1단계: $\Box \diamond (\text{A gets lock})$ 이라는 기호가 "아무리 시간이 흘러도 언젠가는 반드시 A가 락을 얻는 일이 무한히 반복된다"는 물리적 동작임을 해부합니다.
  • 2단계: OS의 스케줄러가 특정 프로세스에게 CPU를 주지 않는 비결정론적 방치(Starvation) 상황을 방지하기 위해 공정성(Fairness) 제약 조건을 추가하는 TLA+ 수리 역학을 뜯어봅니다.
• Implement: 상태 전이 그래프(DAG + Cycle)가 주어졌을 때, 특정 상태 타겟 노드 Goal에 절대로 도달할 수 없는 무한 궤도(Cycle)가 존재하는지 타잔 알고리즘(Tarjan's Algorithm)으로 탐지하여 Liveness 위반을 경고하는 루틴 작성.

Advanced

Core Topic 04: TLA+ 작성과 TLC 모델 체커 (TLA+ & TLC)

• Why to Learn: 펜과 종이로 증명하는 짓을 멈추고, Leslie Lamport가 만든 TLA+ 문법을 쳐서 TLC 엔진이 대신 수십억 개의 상태를 $O(N)$의 속도로 탐색하며 반례(Counterexample)를 뱉어내게 만들기 위함입니다.
• What to Learn:
  • Concepts: TLA+ Specification Structure, TLC Model Checker.
  • Skills: Init과 Next 매크로 작성, 비결정론(Choose) 활용, 모델 검증 및 에러 트레이스(Error Trace) 분석.
  • Tools: TLA+ Toolbox, VS Code TLA+ Extension.
  • Trade-offs: 프로그래밍 언어(C/Java)와 너무나도 다른 괴랄한 수학적 문법 체계를 며칠간 삽질하며 익혀야 하는 진입 장벽 vs 한 번 명세도를 만들어 돌리면 AWS DynamoDB급의 복잡한 시스템에 숨은 데드락을 5분 만에 발라내는 폭발적인 ROI.
• How to Learn:
  • 1단계: TLA+ 문법 Spec == Init /\ [][Next]_vars의 진정한 의미가 "초기 상태부터 시작하여, 모든(Always, []) 스텝은 Next를 따르거나 변수가 변하지 않는다(Stuttering step)"는 시제 논리 캡슐화임을 해부합니다.
  • 2단계: 생산자-소비자(Producer-Consumer) 큐 오버플로우 버그를 의도적으로 남긴 TLA+ 코드를 TLC에 넣고 돌린 뒤, 엔진이 "이 순서대로 스레드가 실행되면 큐가 터짐"이라는 10단계 에러 트레이스(Trace)를 뱉어내는 카타르시스를 분석합니다.
• Implement: 파이썬으로 가상의 TLC 엔진 인터페이스를 모방하여, 유한 상태 오토마타(FSA) 객체와 Safety 조건을 주입받고 전체 상태 트리를 순회하면서 에러가 난 시점까지의 히스토리 트레이스(Trace Array)를 역추적하여 텍스트로 렌더링하는 스크립트 작성.

7. Terminology

8. References

Primary

• [P1] CS2023 - DS/Discrete Structures and Modeling — Logic and state machines.
• [P2] SWEBOK v4.0 - Software Requirements / Formal Methods — Industry specs.

Secondary

• [Specifying Systems] Leslie Lamport — The original TLA+ "Bible".
• [Practical TLA+] Hillel Wayne — Modern, engineer-friendly guide.

Industry

• [TLA+ at Amazon Web Services] — Real-world case study on S3/DynamoDB.
• [Microsoft Azure Service Fabric Verification] — Verification of complex cloud fabric.

9. Final Checklist

Primary

• TLA+의 초기 상태($Init$)와 다음 상태($Next$) 수식을 보고 시스템의 전체적인 상태 머신 다이어그램을 역으로 물리적 재현 가능한가? (P1)
• '무한 루프'가 발생하는 코드를 TLA+의 생존성(Liveness) 관점에서 왜 위반인지 수학적으로 설명 가능한가? (P1)

Secondary

• TLC 모델 체커의 오류 보고서(Counterexample Trace)를 보고, 실제 코드에서 어떤 순서로 동작이 꼬였는지 물리적 버그 원인을 특정할 수 있는가?
• PlusCal 알고리즘 언어가 실제 TLA+ 논리 수식으로 어떻게 '동작 전이(Next Action)'로 번역되는지 그 논리 흐름을 소통 가능한가?

Industry

• 새로운 합의 프로토콜이나 분산 트랜잭션 설계 시, TLA+ 모델링을 통해 네트워크 파티션 상황에서도 데이터 일관성이 보장됨을 수리적으로 입증할 수 있는 가? (SFIA)
• 아키텍처 리뷰 단계에서 자연어 명세의 모호함을 지적하고, 정형 명세로 전환했을 때 기대되는 리스크 감소 효과를 정량적으로 제시할 수 있는 가?