액션 속성

문법 이해하기

한편으로는 근사한 묘기다. 다른 한편으로는, 이제 [][counter' >= counter]_counter가 대체 무슨 뜻인지 알아내야 한다.

드디어 “액션의 시간 논리(Temporal Logic of Actions)”에서 말하는 “액션”에 대해 이야기할 때가 왔다.

한참 전에 문자열에는 반드시 큰따옴표를 써야 한다고 했던 것을 기억하는가? 작은따옴표가 TLA+에서 특별한 역할을 맡고 있기 때문이다. 어떤 스텝(step)에서든 x'는 스텝이 끝날 때의 x 값이자 다음 스텝에서 x가 시작하는 값이다. 그러니 [](x' >= x)는 “x의 다음 값이 x보다 크거나 같다는 것은 항상 참이다”라는 뜻이다.

하지만 이건 (아직) 유효한 TLA+ 속성이 아니다. 살짝 다른 속성 [](x' = x + 1), 즉 “x는 항상 정확히 1씩 증가한다”를 생각해 보자. 여기에 스터터 스텝(stutter step)을 끼워 넣으면 어떻게 될까? 그러면 x가 전혀 바뀌지 않으니 이 속성은 거짓이 된다. 그런데 TLA+의 정의상 스터터 스텝은 언제든 어디에나 끼워 넣을 수 있다. 그러므로 이 속성은 자명하게 거짓이다. 우리가 실제로 검사하고 싶었던 더 흥미로운 속성은 [](x' # x => x' + 1)이었다. 아니면 이를 x' > x \/ UNCHANGED x로 쓸 수도 있다.

여기에 문법 설탕을 하나 더 얹으면, [](x' = x + 1 \/ UNCHANGED x)를 [][x' = x + 1]_x로 쓸 수 있다. 이것을 박스 액션 공식(box action formula)이라고 부른다. 다음 장에서 보겠지만 박스 액션 공식은 TLA+에서 특별한 역할을 한다. TLC는 박스 액션 공식 형태의 액션 속성만 검사할 수 있다.

액션 속성 더 알아보기

“락은 한 스레드에서 다른 스레드로 곧바로 넘어갈 수 없다”는 속성을 하나 더 추가해 보자.

 define
   CounterOnlyIncreases ==
     [][counter' >= counter]_counter
+
+  LockCantBeStolen ==
+    [][lock # NULL => lock' = NULL]_lock
 end define;  
 
 process thread \in Threads
@@ -27,7 +30,7 @@
     tmp := counter;
 
   IncCounter:
-    counter := tmp + IF tmp = 0 THEN 1 ELSE -1;
+    counter := tmp + 1;
   
   ReleaseLock:
     lock := NULL; 

그리고 이제 이 속성을 깨뜨리는 변경을 가해 보자.

 variables tmp = 0;
 begin
   GetLock:
-    await lock = NULL;
     lock := self;
 
   GetCounter:

PROPERTY LockCantBeStolen으로 실행하면 이것이 실패하는 것을 볼 수 있다.

이 속성을 이렇게 쓸 수도 있었다.

 
   LockCantBeStolen ==
     [][lock # NULL => lock' = NULL]_lock
+
+  LockNullBeforeAcquired ==
+    [][lock' # NULL => lock = NULL]_lock
 end define;  
 
 process thread \in Threads

액션 속성에서 헬퍼 액션(helper action)을 쓸 수 있으므로, 이런 식으로도 할 수 있다.

BecomesNull(x) == x' = NULL

LockCantBeStolen ==
   [][lock # NULL => BecomesNull(lock)]_lock

한정자를 쓰는 액션 속성

앞에서 TLC는 최상위 액션 속성만 검사할 수 있다고 했다. 이 때문에 어떤 일은 조금 번거로워진다. 독립적인 카운터가 여러 개 있는 간단한 스펙을 하나 써 보자.

---- MODULE counters ----
EXTENDS Integers

Counters == {1, 2}
(* --algorithm counters
variables 
  values = [i \in Counters |-> 0];

define
end define;  

macro increment() begin
  values[self] := values[self] + 1;
end macro

process counter \in Counters
begin
  A:
    increment();
  B:
    increment();
end process;
end algorithm; *)
=====

앞에서처럼 카운터들이 단조적이라는 액션 속성을 원한다. 앞에서와 달리 이번에는 한정자(quantifier)로 묶어야 할 카운터가 여러 개다.

   values = [i \in Counters |-> 0];
 
 define
+  CounterOnlyIncreases == 
+      \A c \in Counters:
+        [][values[c]' >= values[c]]_values[c]
 end define;  
 
 macro increment() begin

안타깝게도 모델 체커(model checker)의 한계 때문에 TLC는 이것을 검사하지 못한다.

[] followed by action not of form [A]_v.

(에러 메시지가 조금 헷갈리지만, 액션 속성을 한정자 안에 넣으면 언제나 이 에러가 난다.)

이럴 때는 한정자를 액션 속성 안으로 끌어들이면 된다. 알고 보니 []는 \A와 교환 가능하다! 다시 말해 \A x: []P(x)로 쓴 식은 어느 것이든 다음 식과 동치다: [](\A x: P(x)).

 
 define
   CounterOnlyIncreases == 
+    [][
       \A c \in Counters:
-        [][values[c]' >= values[c]]_values[c]
+        values[c]' >= values[c]
+      ]_values
 end define;  
 
 macro increment() begin