동시성

지역 변수

writer가 한 번이 아니라 두 번 쓸 수 있도록 수정하자.

 variables
   queue = <<>>;
   total = 0;
-
+  i = 0;
 
 process writer = 1
 begin
   AddToQueue:
-    queue := Append(queue, 1);
+    while i < 2 do
+      queue := Append(queue, 1);
+      i := i + 1;
+    end while;
 end process;
 
 process reader = 0

상태가 얼마나 늘었는지 보라. while 루프는 원자적(atomic)이지 않아서, 반복 한 번 한 번을 별개의 Write 액션으로 친다. 그래서 이제 가능한 순서는 Read-Write-Write, Write-Read-Write, Write-Write-Read 세 가지다.

i는 writer에서만 쓰이므로 굳이 reader에게 노출할 필요는 없다. 다음과 같이 변수를 프로세스의 지역 변수(local variable)로 만들 수 있다:

 variables
   queue = <<>>;
   total = 0;
-  i = 0;
 
 process writer = 1
+variables
+  i = 0;
 begin
   AddToQueue:
     while i < 2 do

전역 변수(global variable)와 마찬가지로 지역 변수도 시작값을 여러 개 가질 수 있다— i \in 1..3도 유효하다.

실무에서는 지역 변수를 그리 자주 쓰지 않는데, define 블록의 연산자(operator)가 지역 변수를 쓸 수 없기 때문이다. 즉 지역 변수에 대해서는 타입 검사를 하거나 헬퍼 연산자를 작성하는 등의 일을 하기가 쉽지 않다. 보통 지역 변수는 루프 반복 횟수나 모델 경계 설정처럼 보조 변수 또는 “장부 기록용” 변수로 쓴다.

일단은 while 루프를 빼고 이전 버전으로 돌아가자.

프로세스 집합

프로세스가 하나 있으면 이를 프로세스 집합(process set)으로 확장할 수 있다. process name = val이라고 쓰는 대신 process name \in val이라고 쓴다. 그러면 PlusCal이 집합의 각 값마다 별개의 프로세스를 하나씩 만든다.

 ---- MODULE reader_writer ----
 EXTENDS Integers, Sequences, TLC
+
+Writers == {1, 2, 3}
 
 (* --algorithm reader_writer
 variables
   queue = <<>>;
   total = 0;
 
-
-process writer = 1
+process writer \in Writers
 begin
   AddToQueue:
     queue := Append(queue, 1);

동시성은 상태 공간 폭발(state space explosion)의 주요 원인 중 하나다. writer 셋과 reader 하나가 있으면, 이들의 액션 네 개를 순서 짓는 방법은 4! = 24가지다. 다섯 번째 writer를(또는 두 번째 reader를) 추가하면 순서는 120가지로 뛴다.

이제 큐에 값을 최대 세 개까지 넣는데, 읽는 값은 하나뿐이다. reader가 영원히 돌도록 하자.

       total := total + Head(queue);
       queue := Tail(queue);
     end if;
+    goto ReadFromQueue;
 end process;
 end algorithm; *)
 ====

이는 레이블을 while TRUE 루프 안에 넣는 것과 같다.

self

프로세스 집합에는 특별한 키워드 self가 있는데, 이것은 프로세스의 “값”을 가져온다. 그러니 writer들의 경우 프로세스 값은 1과 2가 된다. writer들에게 1 대신 self를 넣으라고 하면, 최종 합계는 6이 되리라 기대할 수 있다.

 process writer \in Writers
 begin
   AddToQueue:
-    queue := Append(queue, 1);
+    queue := Append(queue, self);
 end process;
 
 process reader = 0

이것을 돌려 보면 상태 공간은 조금 늘고 고유 상태는 두 배 넘게 늘어난다(상태 69개 / 고유 상태 38개). 왜 그런지 보려면 writer 1과 2가 어떤 순서로든 실행된 뒤에 무슨 일이 생기는지 생각해 보자. 전에는 어느 writer가 먼저 실행되든 큐는 <<1, 1>>였을 것이다. 하지만 이제는 서로 다른 값을 넣으므로 가능한 큐가 <<1, 2>>와 <<2, 1>> 두 가지다.

macro write() begin
  queue := Append(queue, self)
end macro;

- process P = val
+ process P \in {val}

await

실제 시스템에는 일정 크기를 넘으면 쓰기를 막는 제한된 큐가 흔하다. 가장 엄격한 제한은 “큐가 비어 있을 때만 쓸 수 있다”일 것이다. 이것을 추가하자:

 process writer \in Writers
 begin
   AddToQueue:
+    await queue = <<>>;
     queue := Append(queue, self);
 end process;
 

await는 레이블이 언제 실행될 수 있는지에 대한 제약이다. 레이블 안의 모든 await 문이 참으로 평가될 때에만 레이블이 실행될 수 있다— 굳이 말하자면 그때에만 상태가 “커밋”된다.

reader에도 await를 추가하면 어떨까? 흥미로운 일이 벌어진다:

 process reader = 0
 begin
   ReadFromQueue:
-    if queue # <<>> then
+    await queue # <<>>;
       total := total + Head(queue);
       queue := Tail(queue);
-    end if;
     goto ReadFromQueue;
 end process;
 end algorithm; *)

이것을 돌리면 TLC가 “데드락(deadlock)”을 에러로 보고한다. 모든 writer가 실행을 마치고 나면, reader는 다시는 일어나지 않을 조건을 기다리며 ReadFromQueue에 영원히 갇힌다. 어떤 프로세스도 더 진행할 수 없으므로(writer는 끝났기 때문에, reader는 기다리는 상태에 갇혔기 때문에) 데드락이 된다. 보통 이것은 에러이지만, 여러분의 스펙에서는 에러가 아니라면 여기서 끌 수 있다:

프로시저

참고: 이 내용은 꽤 복잡하면서도 꽤 틈새적이니, 건너뛰었다가 나중에 다시 와도 좋다.

서로 다른 두 프로세스가 스펙 일부를 공유하게 하고 싶다면, 공통 부분을 매크로로 뽑아낼 수 있다. 하지만 레이블이 들어간, 더 복잡한 것을 뽑아내고 싶다면? 이럴 때는 매크로 대신 프로시저(procedure)를 쓴다. 프로시저는 매크로와 비슷하지만 레이블을 담을 수 있고, 작성하고 쓰기가 조금 더 복잡하다.

프로시저를 쓰려면 Sequences를 EXTENDS해야 한다. 변환기가 제어 흐름을 위해 호출 스택을 저장해야 하는데, 이를 튜플(tuple)에 저장하기 때문이다.

procedure Name(arg1, ...)
variables var1 = ...
begin
  Label1:
    \* stuff
  Label2:
    \* more stuff
    return;
end procedure;

return에 도달하면 프로시저가 종료되고 제어가 호출한 프로세스로 돌아간다. 프로그래밍에서 말하는 의미로 무언가가 “반환”되지는 않는다. 프로시저가 return에 도달하지 않고 종료되면 TLC가 에러를 낸다. return은 그저 프로시저를 끝낼 뿐이다. 프로시저가 끝내 거기에 도달하지 못하면 TLC가 에러를 낸다.

프로시저를 호출하려면 call Name(val1, ...);이라고 써야 한다. 프로시저 호출 뒤에는 반드시 goto, 레이블, 또는 (다른 프로시저에서 호출했다면) 또 다른 return이 와야 한다.

process p = "process"
begin
  A:
    call my_procedure(a, b);
    \* Must be followed by a label
  B:

프로시저는 모든 매크로보다 뒤에, 모든 프로세스보다 앞에 정의해야 한다.

불변식 더 찾기

내가 가르치는 사람들과 즐겨 하는 연습이 하나 더 있다. 이 시스템에는 다른 속성(property)이 무엇이 있을까?

항상 생각해야 할 것 하나는 타입 불변식(type invariant)이다. 타입 불변식은 느슨하고 단순해야 하며, 그저 각 값이 가질 수 있는 대략적인 집합이면 된다.

\* Needs to be below translation
TypeInvariant ==
  /\ counter \in 0..NumThreads
  /\ tmp \in [Threads -> 0..NumThreads]
  /\ lock \in Threads \union {NULL}

좀 더 복잡한 속성은 counter가 어떤 스레드의 tmp 값보다도 결코 작지 않다는 것이다. 이것은 몇 가지 방법으로 쓸 수 있다:

CounterNotLtTmp1 ==
  tmp \in [Threads -> 0..counter]

\* or

CounterNotLtTmp2 ==
  \A t \in Threads:
    tmp[t] <= counter

편한 쪽을 쓰면 된다.

이게 프로덕션 스펙이었다면, 스레드가 락을 해제하기 전에 실제로 락을 가지고 있는지 확인하는 간단한 에러 검사도 assert 형태로 추가했을 것이다.

     counter := tmp + 1;
   
   ReleaseLock:
+    assert lock = self;
     lock := NULL; 
 end process;
 end algorithm; *)

불변식의 한계

지금 내 눈에 보이는 흥미로운 불변식은 이게 전부다. 하지만 불변식이 아닌 속성도 몇 가지 보인다. 첫째, counter와 tmp는 증가만 할 수 있다는 점에 주목하라. 모델 체커가 이것도 검사해 주면 좋을 것이다. 둘째, 한 스레드가 다른 스레드의 락을 “훔치는” 일은 불가능해야 한다. 어떤 스레드가 락을 가지고 있다면, 다른 스레드가 락을 얻기 전에 그 스레드가 먼저 락을 해제해야 한다. 이 둘은 모두 불변식이 아니다. 이를 위반하는 것은 잘못된 상태가 아니라, 올바른 상태 사이의 잘못된 전이이기 때문이다.

이런 이유만으로도 불변식은 시스템의 속성을 온전히 모델링하기에 부족하다. 하지만 여기에는 더 깊은 문제가 있다. AllDone은 프로세스들이 끝나면 올바른 결과가 나온다는 것만 말한다. 스레드가 아무것도 하지 않는 루프를 영원히 돌 수 있도록 스펙을 바꾸면, 이 불변식은 자명하게 통과해 버린다. 우리가 정말로 말하고 싶은 것은, 무슨 일이 있어도 언젠가는 올바른 결과가 나온다는 것이다.

이것은 완전히 다른 부류의 요구 사항이다! 시스템이 잘못된 일을 한다는 것을 말하는 대신, 시스템이 항상 올바른 일을 한다는 것을 보이고 싶은 것이다. 다음 장에서는 이런 종류의 속성을 작성하고 검사하는 방법을 배운다.