자주 묻는 질문

누가 만들었나?

비잔틴 장애 허용(Byzantine fault tolerance), Paxos, LaTeX를 만든 장본인이기도 한 레슬리 램포트(Leslie Lamport)다.

재미있는 사실: LaTeX는 “Lamport’s TeX”의 줄임말이다!

PlusCal이란 무엇인가?

PlusCal은 TLA+로 컴파일되는 DSL이다. 대부분의 엔지니어는 순수 TLA+보다 PlusCal로 시작하는 편이 더 쉽다고 느끼며, PlusCal은 많은 스펙에서 아주 잘 통한다. 핵심 과정은 PlusCal로 시작하지만(이유는 여기), 끝날 무렵에는 TLA+를 완전히 가르친다. 주제별 심화와 예제는 TLA+와 PlusCal 양쪽으로 모두 작성했다.

TLA+가 “정형 기법”이라고 들었다. 그게 뭔가?

“정형 기법(formal methods)”은 아주 대략적으로 말해 올바른 프로그램을 작성하는 데 전념하는 컴퓨터 과학 분야다. 보통은 먼저 “올바르다”가 무슨 뜻인지 엄밀한 수학적 정의로 적고(“정형 명세(formal specification)”), 그다음 코드가 그 정의를 만족함을 보이는(“정형 검증(formal verification)”) 식으로 진행한다. 이 과정이 실제로 어떤 모습인지는 내가 운영하는 또 다른 프로젝트인 Let’s Prove Leftpad에서 볼 수 있다.

정형 검증을 흔히 볼 수 없는 이유는 정말, 정말 어렵기 때문이다. 범용 코드에는 복잡한 것이 그냥 너무 많다. 이를 피해 가는 한 가지 방법은 추상적인 설계처럼 훨씬 단순한 영역을 검증하는 데 집중하는 것이다. TLA+가 바로 그렇게 하며, 덕분에 능력을 어느 정도 내주는 대신 쓰기가 더 쉬워진다.

TLA는 무엇의 약자인가?

“세 글자 약어(Three Letter Acronym).”1

함정은 무엇인가?

가장 큰 함정은 TLA+가 테스트하는 대상이 설계이지 코드가 아니라는 점이다. 설계에서 코드를 생성하거나 설계를 코드와 대조해 검사하는 기능은 기본으로 들어 있지 않다. 이는 고수준 설계가 코드보다 훨씬 밀도가 높기 때문이기도 하다. 50줄짜리 설계를 구현하는 데 코드가 수천 줄 들 수도 있다.

(둘을 동기화된 상태로 유지하는 데 도움이 되는 기법이 몇 가지 있다. 이것들은 언젠가 주제별 심화 글로 정리할 계획이다.)

또한 TLA+는 설계가 좋은지, 실용적인지, 심지어 구현 가능한지조차 알려 주지 못하고, 오직 요구사항을 만족하는지만 알려 준다. 좋은 설계를 찾는 데 도움은 되지만, 노력은 여전히 직접 들여야 한다. 어떤 도구도 우리를 좋은 엔지니어가 되어야 할 의무에서 면제해 주지 않는다.

TLA+로 정말 버그를 찾을 수 있나?

그렇다! (공개된!) 성공 사례 몇 가지만 들어 보면 이렇다:

• 엔지니어가 고작 열 명인 에듀테크 회사 Espark Learning은 TLA+로 분산 앱 설치 프로그램의 복잡한 버그를 찾아내, 몇 주 분량의 개발 기간을 아끼고 연간 수십만 달러의 매출을 지켰다.2

• Amazon Web Services는 TLA+로 S3와 DynamoDB의 일부를 모델링해, 모든 테스트와 두 차례의 코드 리뷰를 빠져나간 35스텝짜리 버그를 찾아냈다.

• CrowdStrike는 고작 닷새간의 워크숍 동안 여러 장애 사례를 찾아냈다.

Azure, MongoDB, Confluent, Elastic, Cockroach Labs도 버그를 찾는 데 TLA+를 사용했다.

단위 테스트/Cucumber/TDD/PBT?

이것들은 모두 코드를 대상으로 한다. 코드를 작성하면서 실수하지 않았는지 확인하는 데 쓴다. 반면 TLA+는 설계를 대상으로 한다. 설계가 정말로 원하는 대로 동작하는지 확인하는 데 쓴다.

설계를 검사하는 데는 뚜렷한 단점이 있다. 설계를 구현하다가 실수할 수 있다는 것이다. 하지만 설계 검사에는 큰 장점도 있다. 설계는 구현보다 더 빨리 만들 수 있고, 더 철저하게 테스트할 수 있다. “우리 마이크로서비스 아키텍처는 서비스가 다운되더라도 같은 결제를 절대 두 번 제출하지 않는다”를 예로 들어 보자. 이것을 철저히 테스트하려면 대공사가 될 것이다. TLA+로는 스물 몇 줄이면 된다.

트레이드오프는 중요하며, TLA+가 테스트보다 “더 나은” 것은 아니다. 그리고 아직 테스트를 하고 있지 않다면 TLA+는 최선의 투자가 아니다.3 하지만 이미 테스트를 하고 있다면, TLA+는 도구 상자에 더할 환상적인 추가 도구다.

SPARK/Idris/Dafny/Frama-C/F*?

이것들은 모두 코드를 정형 검증하기 위한 것으로, 각각이 어떤 모습인지는 Let’s Prove Leftpad에서 예시로 볼 수 있다. 앞서 말했듯 코드를 정형 검증하는 일은 극도로 어렵고, 그래서 TLA+는 대신 설계 검증에 집중한다.

(“코드 테스트”와 “코드 검증”을 비교하는 건 완전히 별개의 골칫거리라 여기서 제대로 다룰 수는 없다. 아주 대략적인 개관을 여기에 써 두었지만, 이제는 몇 년 묵은 글이다.)

Alloy/Spin/Event-B/mCRL2?

이제부터 어려운 얘기다. 이것들은 모두 TLA+와 같은 영역, 즉 동작하는 코드 대신 추상적인 설계를 검증하는 영역을 다루는 다른 정형 명세 언어(formal specification language)다. 서로 충분히 가까워서 미묘한 트레이드오프가 중요해진다. 내 생각에 이 도구들을 비교하려면 두 언어 모두에 정통한 전문가가 쓴 별도의 페이지가 있어야 한다.

P?

솔직히 고백해야겠다. 나는 아직 P를 써 보지 않아서, TLA+와 비교해 어떤지 전혀 모른다.

CTL*?

이봐, CTL*가 뭔지 안다면 그냥 나 놀리는 거잖아

1

알았다, 알았다. 사실은 “액션의 시간 논리(Temporal Logic of Actions)”다. TLA+는 TLA라는 “핵심”을 중심으로 설계되었다. TLA+ 사용자들은 이 약어의 뜻을 밝히기를 조금 꺼리는데, 그 뜻을 몰랐다면 TLA+를 별 어려움 없이 배웠을 초심자들이 겁을 먹기 때문이다.

2

밝혀 두자면, 나는 이 프로젝트에 참여했다. 사실 내가 TLA+를 쓰기 시작한 계기가 바로 이 프로젝트였다!

3

나는 이런 이유로 잠재 고객을 거절한 적도 있다.