시간 속성

들어가며

불변식(invariant)은 사실 TLA+의 일부가 아니다. TLA+에는 특별 취급되는 “불변식”이라는 개념이 없다. 모델 체커(model checker)인 TLC가 불변식을 제공하기는 하지만, 그건 “불변식”이 뭔가 깊이 중요한 개념이어서라기보다는 실용성과 효율 때문이다. 오히려 TLA+는 온갖 종류의 속성(property)을 작성하는 일반적이고 원칙적인 방법을 제공하며, 불변식은 우리가 검사할 수 있는 많은 것 중 하나일 뿐이다. 이런 속성을 작성할 때는 시간에 걸친 논리적 명제를 기술하는 시간 연산자(temporal operator)들을 사용한다. 모든 속성을 아우르는 넓은 범주를 시간 속성(temporal property)이라 부른다.

시간 속성에는 두 종류가 있다. “안전성(safety)” 속성은 시스템이 나쁜 일을 하지 않는다고 말한다. “라이브니스(liveness)” 속성은 시스템이 언제나 좋은 일을 해낸다고 말한다. “어떤 데이터베이스 제약 조건도 위반하지 않는다”는 안전성이고, “모든 트랜잭션은 완료되거나 롤백된다”는 라이브니스 속성이다. 모든 불변식은 안전성 속성이지만, 모든 안전성 속성이 불변식인 것은 아니다. 예를 들어 보자.

---- MODULE orchestrator ----
EXTENDS Integers, TLC, FiniteSets

Servers == {"s1", "s2"}

(*--algorithm threads
variables 
  online = Servers;

process orchestrator = "orchestrator"
begin
  Change:
    while TRUE do
      with s \in Servers do
       either
          await s \notin online;
          online := online \union {s};
        or
          await s \in online;
          await Cardinality(online) > 1;
          online := online \ {s};
        end either;
      end with;
    end while;
end process;

end algorithm; *)
====

“항상 온라인인 서버가 적어도 하나 있다”는 둘 중 하나를 뜻할 수 있다.

1. 어느 시점을 잡든, 온라인인 서버가 적어도 하나 있다.

2. 모든 행동(behavior)에는 특정한 서버가 하나 있고, 그 서버는 모든 시점에서 온라인이다.

(1)은 평범한 불변식이다. (2)는 안전성 속성이지만 불변식은 아니다. 그 자체만으로 이 속성을 위반하는 개별 상태는 없다. 내가 online = {1}이라는 상태를 준다고 하자. 이것은 위반인가? 오직 행동 안에 1 \notin online인 다른 상태가 있을 때만 그렇다. 따라서 상태 하나만 봐서는 (2)를 깨뜨렸는지 알 수 없다.

하지만 TLC는 (2)를 시간 속성으로 검사할 수 있다.

[] (항상/“박스”)

[]P는 모든 상태에서 P가 참이라는 뜻이다. 술어(predicate)의 바깥에 있을 때 이것은 불변식과 동등하며, 실제로 TLC가 불변식을 지원하는 방식이 바로 이것이다. P를 불변식으로 지정하는 것은 []P를 속성으로 지정하는 것과 같다.

[]가 더 큰 식(expression)의 일부가 되면 일이 더 재미있어진다. []P \/ []Q라고 쓰면 모든 행동이 P나 Q 중 하나를 불변식으로 가진다는 뜻이며, 둘 다 가질 필요는 없다. 또는 []P => []Q라고 써서 P가 Q보다 더 강한 불변식이라고 말할 수도 있다. 한정자(quantifier) 안에 []를 넣을 수도 있다. (2)를 제대로 모델링하려면 이렇게 쓰면 된다.

Safety == \E s \in Servers: [](s \in online)

행동이 시작될 때 온라인 서버 하나를 고른다. 그러면 그 서버는 항상 온라인이다. 이것은 참이 아니다. PROPERTY Safety로 검사하면 에러 트레이스(error trace)가 나온다.

 (*--algorithm threads
 variables 
   online = Servers;
+
+define
+  Invariant == \E s \in Servers: s \in online
+  Safety == \E s \in Servers: [](s \in online)
+end define;
 
 process orchestrator = "orchestrator"
 begin

State 1: online = {"s1", "s2"}

State 2: online = {"s2"}

State 3: online = {"s1", "s2"}

State 4: online = {"s1"}

요약하면, 언어에 []를 추가하면 모든 불변식은 물론 그 밖의 수많은 속성도 표현할 수 있다.

무엇이든 크래시할 수 있다

[]는 다른 것들과 다를 바 없는 논리 연산자(operator)일 뿐이므로, 다른 논리 연산자와 조합할 수 있다. []~P는 P가 항상 거짓이라는 뜻이다. ~[]P는 P가 항상 참인 것은 아니라는 뜻이다. 이 말은 두 가지를 뜻할 수 있다.

1. 모든 행동에 P가 거짓인 상태가 적어도 하나 있다

2. P가 거짓인 상태를 적어도 하나 가진 행동이 적어도 하나 있다.

스펙(spec)에서는 (1) 쪽이 더 자주 쓸모 있으므로, ~[]P의 형식적 의미는 (1)이다.1 다음과 같이 쓰면

 define
   Invariant == \E s \in Servers: s \in online
   Safety == \E s \in Servers: [](s \in online)
+  \* It's not the case that all servers are always online
+  Liveness == ~[](online = Servers)
 end define;
 
 process orchestrator = "orchestrator"

이것은 라이브니스 속성이지, 안전성 속성이 아니다. Liveness를 만족하려면 행동이 서버가 오프라인인 상태에 도달해야 한다.

이것은 통과하리라 예상할 것이다. 오케스트레이터는 두 가지 중 하나를 할 수 있다. online에서 기존 서버를 제거하거나, 거기 없는 서버를 추가하는 것이다. 그러니 모든 서버가 온라인으로 시작하면 언젠가는 하나를 제거하게 되지 않겠는가?

그렇게 성급하게 굴지 말자! 오케스트레이터가 할 수 있는 세 번째 일이 있다. 바로 크래시하는 것이다. TLA+에서는 어떤 행동이든 스터터(stutter)할 수 있다. 즉 아무 일도 일어나지 않고 모든 변수가 그대로인 새 상태를 만들 수 있다. 이는 스터터 스텝(stutter step)에도 해당되므로, 어떤 행동이든 무한히 스터터할 수 있다. 다시 말해 크래시할 수 있다. 그리고 PROPERTY <- Liveness로 스펙을 돌려 보면 정확히 그 결과를 보게 된다.

TLA+가 무한한 스터터 스텝을 허용하는 것은 근본적으로 최악의 시나리오를 다루는 언어이기 때문이다. 현실에서 시스템은 언제나 크래시한다. 시스템이 크래시할 수 없다고 명시적으로 말하지 않으면, TLA+는 시스템이 가능한 최악의 순간에 크래시할 수 있다고 가정한다.

그래서 “이 시스템이 크래시할 수 있다고 가정하지 마라”라고 말할 방법이 필요하다. 그 방법은 이것이 공정한 프로세스(fair process)라고 말하는 것이다.

   Liveness == ~[](online = Servers)
 end define;
 
-process orchestrator = "orchestrator"
+fair process orchestrator = "orchestrator"
 begin
   Change:
     while TRUE do

이렇게 하면 프로세스가 약하게 공정(weakly fair)해진다. 즉 “영원히 멈출” 수 없다. 이 변경을 추가하면 Liveness가 성립하는 것을 볼 수 있다. 강한 공정성(fairness)도 있다. 하지만 이것은 PlusCal보다 순수 TLA+에서 설명하기가 더 쉽다(그리고 더 유용하다). PlusCal 쪽 내용은 여기 심화 주제로 남겨 두겠다.

강한 공정성

약한 공정성(weak fairness)은 프로세스가 항상 진행할 수 있다면 언젠가는 진행한다는 것이다. 강한 공정성(strong fairness)은 프로세스가 항상 간헐적으로 진행할 수 있다면 언젠가는 진행한다는 것이다. 차이를 보기 위해, 여러 스레드(thread)가 락 하나를 공유하는 다음 모델을 생각해 보자(<>는 아래에서 정의한다).

---- MODULE threads ----
EXTENDS Integers
CONSTANT NULL

Threads == 1..2

(*--algorithm threads
variable lock = NULL;

define
  Liveness == 
    \A t \in Threads:
      <>(lock = t)
end define;

fair process thread \in Threads
begin
  GetLock:
    await lock = NULL;
    lock := self;
  ReleaseLock:
    lock := NULL;
  Reset:
    goto GetLock;
end process;
end algorithm; *)
====

GetLock에 있을 때 각 스레드는 lock = NULL일 때만 락을 얻을 수 있다. 그래서 간헐적으로만 진행할 수 있다. 락을 가진 스레드는 모두 반드시 락을 해제하므로, 항상 간헐적으로 진행할 수 있다. 약한 공정성에서는 스레드가 다섯 개일 때 다섯 개 모두 언젠가 락을 얻는다고 보장할 수 없다. 하나가 굶주릴 수 있다.

스레드 1이 계속 락을 가로채면, 스레드 2는 약하게 공정하더라도 락을 얻을 기회가 영영 없다.

fair+라고 쓰면 프로세스를 강하게 공정하게 만들 수 있다. 그러면 모든 스레드가 언젠가는 락을 얻는다. AwaitLock:+라고 써서 개별 액션(action)을 강하게 공정하게 만들 수도 있다.

       <>(lock = t)
 end define;
 
-fair process thread \in Threads
+fair+ process thread \in Threads
 begin
   GetLock:
     await lock = NULL;

강한 공정성은 순수 TLA+ 스펙 작성을 다룰 때 다시 살펴보겠다. 거기서는 강한 공정성으로 조금 더 많은 것을 할 수 있다.

<> (언젠가는 / “다이아몬드”)

~[]P에는 흥미로운 성질이 좀 있지만, 이것을 쓸 일은 드물다. 시스템에서 무언가가 “가끔” 참이 아님을 검사해야 할 일은 많지 않다. 정말 유용한 것은 ~[]~P를 쓰는 것이다. “가끔은 ‘P가 아님’이 거짓이다”, 즉 “가끔은 P가 참이다”라는 뜻이다. 이것은 P가 모든 상태에서 성립하는 불변식은 아니지만, 적어도 하나의 상태에서는 성립해야 한다는 뜻이다.

“항상 P가 아닌 것은 아니다”는 말하기 번거로우므로, 같은 뜻의 별도 연산자가 있다. 바로 <>P, 즉 “언젠가는(eventually) P”이다. 우리는 이미 duplicates와 threads에서 “언젠가는” 속성을 엉성하게 흉내 내 왔다. threads의 정확성 조건은 다음과 같다.

AllDone ==
  \A t \in Threads: pc[t] = "Done"

Correct ==
    AllDone => counter = NumThreads

AllDone =>는 알고리즘 실행이 끝났을 때 counter = NumThreads가 참이라는 것에 붙은 전제 조건일 뿐이다. <>를 사용하면 이것을 시간 속성으로 다시 쓸 수 있다.

   lock = NULL;
 
 define
-  AllDone == 
-    \A t \in Threads: pc[t] = "Done"
-
-  Correct ==
-      AllDone => counter = NumThreads
+  Liveness ==
+    <>(counter = NumThreads)
 end define;  
 
 process thread \in Threads

(이것은 “Invariants”(불변식)가 아니라 “Temporal Properties”(시간 속성) 항목에서 검사한다는 점을 잊지 말자!)

PROP Liveness, NULL <- [mv]로 돌리면 스터터링(stuttering) 때문에 스펙이 실패한다. 스레드들이 공정하지 않으므로 실행을 끝마친다는 보장이 없다. 이전에는 이것이 문제가 아니었는데, Correct는 만약 끝에 도달하면 그때 답이 올바르다고만 말하기 때문이다. 끝에 영영 도달하지 않아도 여전히 통과한다!

스레드를 공정하게 만들면 통과한다.

     <>(counter = NumThreads)
 end define;  
 
-process thread \in Threads
+fair process thread \in Threads
 variables tmp = 0;
 begin
   GetLock:

어떤 면에서는 Liveness가 Correct보다 더 정확하다. 하지만 다른 면에서는 덜 정확하다. Correct는 통과하지 못할 버그를 하나 보자.

 (* --algorithm threads
 
 variables 
-  counter = 0;
+  counter = 1;
   lock = NULL;
 
 define

끝나고 나면 counter = 3이다… 그런데도 Liveness는 여전히 통과한다! <>(counter = 2)는 counter = 2인 상태가 행동 안에 적어도 하나 있으면 참이기 때문이다. 그 뒤에 그 값에서 벗어나도 상관없다. 적어도 한 번은 참이었기 때문이다.

<>[]

다행히 시간 연산자는 매우 유연해서 서로 조합할 수 있다. []P가 “P는 항상 참이다”이고 <>P가 “P는 언젠가는 참이다”라면, <>[]P는 “언젠가는 P가 항상 참이다”이다. P는 처음에는 거짓일 수 있지만, 모든 행동에서 어느 시점 이후로는 영원히 참이 된다.

 
 define
   Liveness ==
-    <>(counter = NumThreads)
+    <>[](counter = NumThreads)
 end define;  
 
 fair process thread \in Threads

이제 이것은 실패한다. counter가 2에 머물지 않기 때문이다.

~> (leads-to)

마지막 연산자는 ~>다. P => Q는 Q에 P라는 전제 조건을 붙인다는 것을 떠올려 보자. P가 참이면 Q도 참이다. P ~> Q는 그 시간적 대응물이다. P가 참이면 Q는 (지금 또는 미래의 상태에서) 언젠가는 참이 된다.

TaskType으로 기술되는 작업 집합, inbound 풀(타입은 SUBSET TaskType), 그리고 각자 작업 집합을 가진 워커 집합이 있다고 하자. 이 시스템의 속성 하나는 들어온 작업이 모두 언젠가는 워커에게 처리된다는 것일 수 있다. 이것은 ~>로 나타낼 수 있다.

Liveness ==
  \A t \in TaskType:
    t \in inbound
      ~> \E w \in Workers:
        t \in worker_pool[w]

라이브니스는 언제 쓰나

\E x: [](P(x)) 꼴의 속성을 쓸 일은 아마 없을 것이다.

라이브니스 속성은 불변식보다 드물다. 불변식은 검사가 더 빠르고 더 세밀한 정보를 주며, 작성하기도 훨씬 쉽다! 대부분의 시스템에는 불변식은 많지만 라이브니스 속성은 두어 개뿐일 것이다. 그래도 라이브니스 속성은 스펙에서 여전히 결정적으로 중요하다. 우리가 실제로 무엇을 하고 싶은지를 정의하기 때문이다.

고려 사항

• TLC가 라이브니스 속성을 검사하는 데는 안전성 속성보다 훨씬 오래 걸린다. 보통은 안전성 속성을 검사하기 위한 큰 상수(constant)를 쓰는 모델 하나와, 라이브니스 속성을 검사하기 위한 더 작은 상수를 쓰는 모델 하나를 둔다.

• 라이브니스 속성에는 대칭 집합(symmetry set)을 쓸 수 없다.

• 구현상의 이유로, 현재 TLC는 어느 속성이 깨졌는지 알려 주지 못한다. “Temporal Properties are Violated”(시간 속성이 위반됨)라고만 알려 줄 수 있다.

• 역시 구현상의 세부 사항 때문에, 라이브니스 속성 위반 에러는 최대한 짧은 형태로 나오지 않는다. 더 작은 상수로 모델을 다시 돌리면 더 짧은(그리고 더 이해하기 쉬운) 에러 트레이스를 얻을 수도 있다.

요약

• TLA+는 상태의 속성뿐 아니라 행동 전체의 속성도 검사할 수 있다.

• 안전성 속성은 “나쁜 일이 일어나지 않는다”이고, 라이브니스 속성은 “좋은 일이 실제로 일어난다”이다. 모든 불변식은 안전성 속성이고, 모든 라이브니스 속성은 시간 속성이다.

• 모든 TLA+ 스펙은 “스터터 불변(stutter-invariant)”이다. 즉 언제든 크래시할 수 있다. “약하게 공정한” 프로세스는 “크래시하지 않음”이 보장되지만, 스핀락에 빠질 수는 있다.

• []P는 모든 행동의 모든 상태에서 P가 참이라는 뜻이다. <>P는 모든 행동의 적어도 한 상태에서 P가 참이라는 뜻이다. P ~> Q는 어떤 상태에서 P가 참이면 (현재 또는) 미래의 어떤 상태에서 Q가 참이 된다는 뜻이다.

1

이것이 “정설”은 아니다. 다른 체계에서는 ~[]P가 성립하려면 한 행동의 한 상태에서만 P가 거짓이면 된다. 이런 체계는 어떤 것은 더 못 모델링하고 어떤 것은 더 잘 모델링하는 경향이 있다.