개념 개요

구조

TLA+의 개념적 틀은 세 부분으로 이루어져 있다.

첫째, 시스템과 그 시스템이 할 수 있는 일을 기술해야 한다. 이것을 명세(specification), 줄여서 스펙이라고 한다. 우리의 설계는 이런 모습일 것이다.

• 계좌들의 집합(set)이 있다. 각 계좌에는 잔액을 나타내는 숫자가 하나 있다.

• 어느 계좌든 다른 어느 계좌로든 얼마든지 송금을 시도할 수 있다.

• 송금은 먼저 잔액이 충분한지 확인한다. 충분하면 그 금액을 첫 번째 계좌에서 빼서 두 번째 계좌에 더한다.

• 송금은 원자적이지 않다. 여러 송금이 동시에 일어날 수 있다.

명세에는 “행동(behavior)”들, 즉 서로 구별되는 가능한 실행들의 집합이 있다. 스펙이 올바르려면 모든 행동이 우리의 시스템 요구사항, 즉 속성을 전부 만족해야 한다. “어떤 계좌도 초과 인출될 수 없다”가 속성의 한 예이며, 스펙의 어떤 행동에 계좌 잔액이 음수인 상태(state)가 하나라도 있으면 이 속성은 위반된다. 다른 가능한 행동들에 초과 인출이 전혀 없다는 것은 상관없다. 우리는 드문 설계 오류를 찾고 있으므로 위반 하나면 충분하다.

스펙과 속성을 작성했으면 이것을 “모델 체커(model checker)”에 넣는다. 모델 체커는 스펙을 받아 가능한 모든 행동을 생성하고, 그 행동들이 모두 우리의 속성을 전부 만족하는지 확인한다. 만족하지 않는 행동이 하나라도 있으면, 그 위반을 재현하는 방법을 보여 주는 “에러 트레이스(error trace)”를 돌려준다. TLA+용 모델 체커는 몇 가지가 있지만, 가장 널리 쓰이는 것은 툴박스에 번들로 들어 있는 TLC다. 따로 말하지 않는 한, 내가 모델 체커라고 하면 TLC를 가리킨다.

하지만 모든 가능한 행동을 검사할 수는 없다. 사실 행동은 무한히 많다. 시스템에 계좌와 송금을 얼마든지 더 추가할 수 있기 때문이다. 그래서 대신 “계좌 세 개에 각 계좌 최대 10달러, 송금 두 건에 각 송금 최대 10달러인 모든 행동”처럼 특정 제약 아래의 모든 행동을 검사한다. 이런 런타임 매개변수들의 집합을, 그 밖에 우리가 하는 모든 모델 체커 설정과 함께 모델(model)이라고 부른다.

스펙

그렇다면 실제로는 이 모든 것이 어떤 모습일까? 송금 스펙을 먼저 매개변수를 하드코딩한 형태로, 그다음 모델에서 매개변수를 정할 수 있는 형태로 보여 주겠다.

---- MODULE wire ----
EXTENDS TLC, Integers

People == {"alice", "bob"}
Money == 1..10
NumTransfers == 2

(* --algorithm wire
variables
  acct \in [People -> Money];

define
  NoOverdrafts ==
    \A p \in People:
      acct[p] >= 0
end define;

process wire \in 1..NumTransfers
variable
  amnt \in 1..5;
  from \in People;
  to \in People
begin
  Check:
    if acct[from] >= amnt then
      Withdraw:
        acct[from] := acct[from] - amnt;
      Deposit:
        acct[to] := acct[to] + amnt;
    end if;
end process;
end algorithm; *)

====

이 모든 것이 문법적으로 어떻게 동작하는지는 책의 나머지 부분에서 다룬다. 지금은 TLA+가 코드와 다르게 하는 여러 부분에 주의를 환기하고 싶을 뿐이다.

• 정의에는 ==를 쓴다. 미안, 규칙은 내가 정한 게 아니다

• People과 Money는 집합, 즉 중복 없고 순서 없는 값들의 모음이다. 프로그래밍 언어는 주로 배열과 키-값 맵(각각 시퀀스(sequence)와 구조체(structure)에 해당)을 쓰지만, 명세에서는 집합이 훨씬 더 근본적이다.

• [People -> Money]도 집합이다(이 경우에는 함수 집합(function set)). 이것은 사람에게 금액을 배정하는 가능한 모든 방식을 나타낸다. 앨리스는 5달러에 밥은 1달러, 앨리스는 10달러에 밥은 6달러, 이런 식이다.

• 변수 acct는 고정된 값이 아니라, [People -> Money]의 원소 하나하나에 대응하는 서로 다른 100개의 값 중 하나다. 이것을 모델 체킹하면, TLC는 이 100개의 가능한 초기값 하나하나에서 출발하는 모든 가능한 행동을 탐색한다.

• NoOverdrafts는 한정자(quantifier)다. 모든 계좌가 >= 0이면 참이고, 그렇지 않으면 거짓이다. 파이썬이라면 대략 all([acct[p] >= 0 for p in People])에 해당할 것이다. 한정자는 TLA+의 극히 강력한 기능으로, 아주 복잡한 속성도 쉽게 작성할 수 있게 해 준다.

• wire 프로세스(process)가 둘 이상 동시에 실행된다. NumTransfers == 2이면 스펙에 프로세스가 두 개 있다. 하지만 정말 원한다면 프로세스를 열 개, 백 개, 천 개로도 둘 수 있으며, 제약은 우리의 인내심과 RAM뿐이다.

• 알고리즘의 각 스텝(step)은 별개의 레이블(label)에 속한다. 레이블은 무엇이 원자적으로 일어나고 무엇에 다른 프로세스가 끼어들 수 있는지를 결정한다. 이렇게 해서 경쟁 조건을 표현할 수 있다.

 ---- MODULE wire ----
 EXTENDS TLC, Integers
-
-People == {"alice", "bob"}
-Money == 1..10
-NumTransfers == 2
+CONSTANTS People, Money, NumTransfers
 
 (* --algorithm wire
 variables