메시지 큐 모델링

메시지 큐는 분산 시스템에서 가장 흔한 “패턴”이다.

Reader 프로세스(process)와 Writer 프로세스로 이루어진 집합이 큐 하나를 공유한다고 가정하자. 이를 여러 큐로 확장하는 방법은 나중에 다룬다.

큐

일단은 새 메시지를 푸시(push)하는 연산과 오래된 메시지를 팝(pop)하는 연산을 갖춘 완벽한 FIFO 큐를 생각해 보자.

queue 변수는 일반적으로 시퀀스(sequence)이고, 그 원소는 메시지 구조체(struct)다. 새 메시지를 쓰려면 그냥 queue := Append(queue, msg)(또는 queue' = ...)를 하면 된다. 큐에서 읽는 데는 쉬운 방법과 어려운 방법이 있다.

쉬운 방법은 큐를 파괴적으로 갱신해서 최신 메시지가 항상 Head(queue)가 되게 하는 것이다. 개념적으로 단순하고, 큐가 비었는지 확인하거나 타입 불변식(type invariant)을 작성하는(아래 참고) 등의 일이 쉽다. 유일한 단점은 “같은 메시지가 두 번 큐에 들어가는 일은 절대 없다”처럼 큐의 히스토리에 의존하는 속성(property)을 작성할 수 없다는 것이다. 중복된 메시지들이 동시에 큐에 들어 있는지는 알 수 있지만, 원본이 팝된 뒤에 중복이 푸시되었는지는 알 수 없다. 적어도 히스토리 큐 없이는 그렇다.

어려운 방법은 큐를 불변(immutable)으로 만드는 것이다. 평소처럼 큐에 추가하되, 다음에 읽을 메시지를 나타내는 i 변수를 따로 둔다. 메시지를 “팝”하려면 i를 증가시킨다. 이 방법은 다루기가 더 어렵고, 변수를 불어나게 하며, (길이 구하기 같은) 간단한 큐 검사 상당수를 더 번거롭게 만든다. 유일한 장점은 큐의 히스토리 전체가 보존되어 일반화된 속성을 작성하기가 더 쉬워진다는 것이다.

경고

불변 큐에서는 경계 없는 모델(unbound model)을 조심하라! 읽지 않은 메시지의 최대 개수를 제한하더라도, 오래된 메시지를 계속 읽어 나가는 한 큐는 여전히 끝없이 자랄 수 있다.

경험칙상, 나는 추가할 계획이 없는 큐, 예컨대 여러 초기 상태로 초기화되는 큐에는 불변 큐를 즐겨 쓴다.

두 방식의 기본 연산을 간단히 표로 정리하면 다음과 같다:

연산	가변 큐	불변 큐
현재 메시지 가져오기	`Head(queue)`	`queue[i]`
현재 메시지 삭제	`queue' = Tail(queue)`	`i' = i + 1`
큐 크기	`Len(queue)`	`Len(queue) - i + 1`
큐가 비었는가?	`queue = <<>>`	`Len(queue) = i + 1`

메시지

구조체의 집합을 쓴다.

\* Seq comes from EXTENDS Sequences
QueueType == Seq(MessageType)
MessageType == [id: Nat, from: Writer, data: DataType]

id 필드를 두면 내용이 같은 서로 다른 메시지를 구별할 수 있으므로 좋은 습관이다(MaxId 상수(constant)를 꼭 두자!). DataType도 구조체일 수 있다. 서로 다른 종류의 메시지를 여러 개 두고 싶다면 msg 필드를 추가하고, 데이터의 세부 내용은 data 구조체로 밀어 넣는다. 그런 다음 MessageType을 가능한 하위 타입들의 합집합으로 만든다:

AlphaMsg == [id: Nat, from: Writer, msg: {"alpha"}, data: AlphaData]
BravoMsg == [id: Nat, from: Writer, msg: {"bravo"}, data: BravoData]
Messagetype == AlphaMsg \union BravoMsg

추가적인 복잡성

여러 리더 큐

일반 팁에서 다뤘듯이, 프로세스별로 복잡한 데이터를 표현하는 가장 좋은 방법은 변수를 별도의 함수(function)들로 분해하는 것이다. 다시 말해 리더(reader)마다 큐가 하나씩 있다면, 적절한 표현은 다음과 같다:

queues \in [Reader -> QueueType]

그러면 각 리더는 queues[self]에서 읽는다. 모든 큐에 같은 메시지를 쓰려면 queues 변수를 다시 정의한다:

\* PlusCal
  queues := [r \in Reader |-> Append(queues[r], msg)]
\* TLA+
  queues' = [r \in Reader |-> Append(queues[r], msg)]

리더의 부분집합에만 푸시하고 싶다면 함수 병합(function merge)으로 할 수 있다:

\E readers \in SUBSET Reader:
  queues' = [r \in readers |-> Append(queues[r], msg)] @@ queues

팁

최대 한 번 전달(at-most-once delivery)은 유효한 수신자들의 부분집합에 전달하는 것으로 모델링할 수 있다. 부분집합에 들지 않은 쪽은 모두 의도된 메시지를 받지 못한다.

여러 라이터 큐

여러 리더 큐와 같되, 이번에는 큐에서 어떻게 비결정적으로(nondeterministically) 읽느냐가 문제라는 점이 다르다.

\* PlusCal
  with w \in Writer:
    msg := Head(queue[w]);
    queue[w] := Tail(queue[w]);

\* TLA+
  \E w \in Writer:
  /\ msg' = Head(queue[w])
  /\ queue' = [queue EXCEPT ![w] = Tail(@)]