핵심 과정

여기서는 언어의 핵심 내용을 다룬다. 이 섹션은 완전한 문외한을 초보 실무자로 이끌어 주는, 그 자체로 완결된 한 권의 “책”이라고 생각해도 좋다. 이미 TLA+에 익숙한 사람이라면 주제별 심화 쪽이 더 유용할 수도 있다.

개요

아주 대략적으로 안내하자면, 우리가 배울 순서는 다음과 같다:

두 수를 더하거나 두 시퀀스(sequence)를 이어 붙이는 것 같은 기본 연산을 하는 법.
“이 리스트에 중복된 항목이 있는지 확인하기” 같은 단순하고 결정적이며 동시성이 없는 알고리즘을 명세(specify)하는 법, 그리고 불변식(invariant)이 성립하는지 검사하는 법.
비결정적(nondeterministic) 알고리즘, 이를테면 무작위성이 개입하거나 실패할 가능성이 있는 알고리즘을 명세하기.
동시적(concurrent) 시스템, 이를테면 큐 하나를 공유하는 독립적인 읽기 주체와 쓰기 주체들을 명세하기.
시간 속성(temporal properties), 즉 “언젠가는 모든 서버가 온라인이 된다”처럼 시스템의 전체 수명에 걸친 속성을 명세하기.
TLA+ 우선 방식으로 스펙 작성하기.

“시간 속성” 항목을 포함해 그 앞의 모든 내용은 TLA+를 온전히 활용하는 데 필요하다. 그 뒤의 내용은 여기에 힘을 더 보태 준다.

자료에 관한 일러두기

예제

지금으로서는 이 가이드에 예제가 꽤 빈약하다. 더 흥미로운 예제는 예제 섹션에 있다.

노트

아직 예제를 많이 넣지는 못했지만, 웹 여기저기서 찾아낸 예제들의 링크는 모아 두었다!

PlusCal 대 TLA+

실무에서 사람들이 TLA+를 작성하는 언어는 두 가지다. 첫째, 모든 것을 TLA+로 할 수 있다(“순수 TLA+”). 둘째, TLA+를 일종의 “어셈블리 언어”처럼 다루면서, 기본 로직 대부분은 TLA+로 쓰되 상태 전이(state transition)는 전부 DSL에서 처리할 수 있다. 이를 위한 공식 DSL이 “PlusCal”이고, 우리가 먼저 시작할 것도 바로 이것이다. 나는 두 가지 이유로 이 방식을 선호한다:

명세는 극도로 밀도가 높고 서로 긴밀하게 얽힌 주제다. PlusCal을 먼저 가르치면 이 주제의 일부 측면을 따로 떼어 내 쓸모 있는 방식으로 가르치고, 그 위에 나머지를 차츰 쌓아 올릴 수 있다. 이렇게 하면 인지 부하가 줄어든다. 반대로 순수 TLA+부터 배우면, 뭐 하나라도 해내려면 모든 것을 한꺼번에 배워야 한다.
일단 PlusCal을 알고 나면 순수 TLA+를 배우기는 엄청나게 쉽다. “새로운 내용”은 전부 단 한 장으로 다룰 수 있을 것이다.

그렇긴 해도 모두가 이런 방식으로 배우는 편이 더 쉽다고 느끼지는 않으며, 그래도 괜찮다. TLA+부터 가르치는 자료가 두 가지 있는데, 둘 다 TLA+의 창시자가 만든 것이다:

Specifying Systems: TLA+로 시스템을 모델링하는 법을 폭넓게 다루는 입문서지만, 그렇게 만든 스펙을 검사하는 방법은 조금 덜 다룬다.
비디오 강좌: 나는 보지 않아서 품질에 대해서는 뭐라 말할 수 없지만, 내가 아는 사람 중 몇몇은 정말 좋아한다.

더 많은 학습 자료 목록은 기타 자료도 참고하라.