비결정성

지금까지 우리 스펙은 모두 결정적(deterministic)이었다. 가능한 시작 상태는 여러 개일 수 있지만, 각 시작 상태에서 이어지는 행동(behavior)은 정해져 있다. 대부분의 시스템은 결정적이지 않다. 몇 가지 예를 들면 다음과 같다:

무작위성은 가능한 무작위 값마다 새로운 행동을 하나씩 만들어 낸다.
사용자가 무엇을 어떤 순서로 할지 알 수 없으므로 대화형 시스템은 결정적이지 않다.
센서가 얻을 수 있는 측정값의 범위는 알 수 있겠지만, 구체적으로 어떤 값을 얻게 될지는 알 수 없다.
시스템에 독립적으로 움직이는 부분이 많으면 각 부분이 어떤 순서로 실행될지 알 수 없다.

마지막 경우인 동시성(concurrency)은 다음 장에서 다룬다. 나머지를 다루기 위해 PlusCal에는 새로운 구문이 두어 개 있다.

with

지역 변수(local variable)를 만드는 데 with를 쓰는 것은 이미 보았다:

with tmpx = x, tmpy = y do
  y := tmpx;
  x := tmpy;
end with;

스펙 변수를 정의할 때 x \in set이라고 써서 x = val을 대신할 수 있었던 것을 기억하는가? 여기서도 똑같이 할 수 있다.

with roll \in 1..6 do
  sum := sum + roll;
end with;

이 블록 안에서 roll은 여섯 값 중 어느 것이든 될 수 있다. 모델 체커(model checker)는 여섯 가지 모두를 시도하므로, 사실상 이 문장 하나에서 새로운 행동 여섯 개가 생겨난다.

팁

하나의 with 문 안에서 결정적 할당과 비결정적(nondeterministic) 할당을 섞어 쓸 수 있다. 다음은 올바른 코드다:

with
  x \in BOOLEAN,
  y \in 1..10,
  z = TRUE
do
  \* ...
end with;

집합 변수에서 비결정적으로 값을 꺼낼 수도 있다:

with thread \in sleeping do
  sleeping := sleeping \ {thread};
end with;

노트

집합 변수가 비어 있으면 with는 진행하지 못하고 멈추는데(block), 이는 데드락(deadlock)으로 이어질 수 있다. 데드락은 동시성을 다루는 다음 장에서 더 자세히 이야기한다.

either-or

either는 비결정적 제어 흐름이다.

either
  approve_pull_request();
or
  request_changes();
or
  reject_request();
end either;

이 코드를 평가할 때 TLC는 세 분기를 만든다:

digraph either {
branch[label=either, shape=point];
A -> branch[arrowhead=none, label=either];
branch -> {approve request reject};
}

either 문 안에 레이블(label)을 둘 수 있다. either 문은 상태 기계(state machine)를 구현할 때 특히 유용하다.

비결정성 활용하기

비결정성(nondeterminism)은 명세(specification)와 프로그래밍 언어가 크게 갈라지는 첫 지점이다. 또한 추상화 수준을 크게 끌어올리는 첫 번째 요소이기도 하다. 특히 비결정성을 쓰면 프로그램의 “새드 패스(sad path)”를 추상화할 수 있다.

커다란 업무 워크플로를 명세하고 있고, 그중 한 단계에서 직원이 어떤 리소스에 대한 접근을 요청한다고 하자. 해피 패스(happy path)에서는 직원이 요청을 하고, 리소스가 그 직원에게 할당되고, 워크플로가 계속 진행된다. 할당이 거부될 수 있는 업무상 이유는 많다:

직원에게 리소스 사용 권한이 없다
리소스가 사용 중이라 비워질 때까지 재할당할 수 없다
CI 검사를 통과해야만 리소스를 할당할 수 있는데, 검사가 실패했다
상급자가 요청을 거부했다
리소스를 재할당하는 코드에 버그가 있어서 크래시가 났다

이 모든 에러 상태를 빠짐없이 표현하려면 명세에 엄청나게 많은 정보를 넣어야 한다: 권한 정책, 예약 정책, CI 프로세스, 체크아웃 코드 등등. 그 밖에 가능한 다른 모든 에러는 말할 것도 없다! 이건 엄청난 작업이고, 리소스 체크아웃이 워크플로의 작은 일부일 뿐이라면 더 큰 그림을 살피는 데 쓸 수도 있었던 노력을 여기에 잔뜩 쏟는 셈이다.

비결정성이 진가를 발휘하는 곳이 바로 여기다. 그 모든 에러의 세부 사항을 넣을 필요는 없다. 할당이 성공하거나, 아니면 에러가 난다고만 말하면 된다:

macro request_resource(r) begin
  either
    reserved := reserved \union {r};
  or
    \* Request failed
    skip;
  end either;
end macro;

에러의 종류까지 모델링해야 한다면(복구 로직이 에러 종류에 따라 달라진다면), 신경 쓰는 만큼만 정확히 표현할 수 있다:

macro request_resource(r) begin
  either
    reserved := reserved \union {r};
    failure_reason := "";
  or
    with reason \in {"unauthorized", "in_use", "other"} do
      failure_reason := reason;
    end with;
  or
    \* some other error
    skip;
  end either;
end macro;

either or skip은 흔히 쓰이는 비결정성 패턴으로, 여러 곳에서 꽤 유용하다.

비결정성으로 외부의 행위를 표현할 수도 있다. 시스템으로 들어오는 요청을 모델링한다면, 스펙에 쓸 특정 요청을 하나 골라야 할 필요가 없다. 대신 RequestType을 정의해 두고 요청이 들어올 때마다 거기서 하나를 꺼내면 된다.

RequestType == [from: Client, type: {"GET", "POST"}, params: ParamType]

with request \in RequestType do
  if request.type = "GET" then
    \* get logic
  elsif request.type = "POST" then
    \* post logic
  else
    \* something's wrong with our spec!
    assert FALSE;
  end if;
end with;

예제: 계산기

비결정성을 쓰는 한 가지 방법은 사용자 입력을 시뮬레이션하는 것이다. 시스템은 모든 사용자 동작을 제대로 처리해야 하므로, 사용자가 유효한 집합에서 비결정적으로 동작을 고른다고 모델링한다. 예로 아주 단순한 계산기를 명세해 보자. TLA+는 소수점이 있는 수를 표현할 수 없지만, 덧셈, 곱셈, 뺄셈은 할 수 있다. 먼저 사용자가 현재 합계에 아무 한 자리 숫자나 더할 수 있게 하자:

---- MODULE calculator ----
EXTENDS Integers, TLC
CONSTANT NumInputs

Digits == 0..9

(* --algorithm calculator
variables 
  i = 0;
  sum = 0;

begin
  Calculator:
    while i < NumInputs do
      with x \in Digits do
          \* Add
          sum := sum + x;
      end with;
      i := i + 1;
    end while;
end algorithm; *)
====

spec

주목할 점이 두 가지 있다:

사용자는 한 자리 숫자를 아무거나 입력할 수 있으며, 이는 with로 표현한다. 상태 공간(state space)을 작게 유지하기 위해 선택지를 0..9로 제한한다.
스펙이 행동 하나당 NumInputs번의 연산만 하도록 제한한다. 대신 while TRUE로 했다면 sum에는 상한이 없어지고, 상태 공간은 무한히 커지며, 모델 체커는 영원히 돌 것이다. 쉽게 바꿀 수 있도록 NumInputs는 모델 상수(model constant)로 만든다.

이 스펙 전체에서 나는 NumInputs <- 5를 쓰며, 그러면 상태 1043개 / 고유 상태 187개가 나온다. (발견한 상태 / 고유 상태)의 비율이 전에 보던 것보다 훨씬 높다: 5를 더한 뒤 3을 더하든, 3을 더한 뒤 5를 더하든 같은 상태가 되기 때문이다. (발견한 상태 / 초기 상태(initial state))의 비율도 훨씬 높다. 전에는 시작 상태마다 행동이 하나뿐이었지만, 이제는 여러 개다.

사용자가 빼기와 곱하기도 할 수 있게 하려면, 덧셈 로직을 either의 한 분기에 넣고 분기를 두 개 더 만들면 된다.

   Calculator:
     while i < NumInputs do
       with x \in Digits do
+        either
           \* Add
           sum := sum + x;
+        or
+          \* Subtract
+          sum := sum - x;
+        or
+          \* Multiply
+          sum := sum * x;
+        end either;
       end with;
       i := i + 1;
     end while;

spec

연산자를 비결정적으로 고르게 하면 상태 공간이 더 불어나 상태 71333개 / 고유 상태 16551개가 된다. 비결정성을 다룰 때는 가능한 상태가 아주 많은데, 이것이 비결정성을 추론하기 더 어려운 이유 중 하나다.

보통은 이 스펙이 제대로 동작하는지 확인하는 불변식(invariant)을 작성하겠지만, 타입 불변식(type invariant) 한두 개를 빼면 여기서는 확인할 것이 별로 없다. 그러니 발상을 뒤집어서, TLA+로 어떤 문제의 해를 찾을 수 있는지 보자. 다섯 번의 입력으로 어떤 수, 이를테면 417에 도달할 수 있을까?

이를 알아내기 위해 sum이 417이 아니라는 불변식을 추가하자. 그러면 그 sum에 도달할 수 있을 경우 모델 체커가 실패하면서, 417까지 가는 경로를 나타내는 에러 트레이스(error trace)를 보여 준다.

 ---- MODULE calculator ----
 EXTENDS Integers, TLC
-CONSTANT NumInputs
+CONSTANT NumInputs, Target
 
 Digits == 0..9
 
@@ -8,6 +8,9 @@
 variables 
   i = 0;
   sum = 0;
+define
+  Invariant == sum # Target
+end define;
 
 begin
   Calculator:

spec

이제 INVARIANT Invariant와 NumInputs <- 5, Target <- 417로 체커를 돌리면 다음 에러 트레이스가 나온다:

State 1:
/\ sum = 0
/\ i = 0

State 2:
/\ sum = 1
/\ i = 1

State 3:
/\ sum = 10
/\ i = 2

State 4:
/\ sum = 60
/\ i = 3

State 5:
/\ sum = 420
/\ i = 4

State 6:
/\ sum = 417
/\ i = 5

즉 417은 ((((0+1)+9)*6)*7)-3이다.

(이 스펙을 보다가 궁금해졌다: 5번의 입력으로 도달할 수 없는 가장 작은 수는 무엇일까? 모델 체킹 한 번으로 이를 알아낼 쉬운 방법은 없다. 그래서 모델 체커를 명령줄에서 실행하되 Target을 0부터 1000까지 모든 값으로 바꿔 가며 돌리는 스크립트를 작성했다. 에러 트레이스가 나오지 않는 첫 번째 수는 851이다.)

요약

비결정성이란 스펙이 한 스텝(step)에서 여러 가지 다른 일 중 하나를 할 수 있는 것을 말한다.
with x \in set은 set에서 값 하나를 비결정적으로 골라 x에 준다.
either branch1 or branch2는 실행할 분기를 비결정적으로 고른다.
비결정성을 쓰면 구현 세부 사항을 하나의 고수준 스텝으로 추상화할 수 있다.