개발자로서 가장 두려운 순간은 시스템이 완전히 죽어버렸을 때가 아니라, 살아있는 것처럼 보이는데 아무런 일도 하지 않는 '좀비 상태'에 빠졌을 때입니다. 10년 넘게 백엔드 시스템을 다루면서 수없이 겪었던 교착 상태(Deadlock)나 기아 상태(Starvation)가 바로 그런 경우죠. 이를 전문 용어로는 Liveness(활동성) 문제라고 부릅니다. Safety(안전성)가 "나쁜 일이 발생하지 않는다"는 것을 보장한다면, Liveness는 "좋은 일이 결국에는 발생한다"는 것을 보장합니다. 자동차로 비유하자면, Safety는 사고가 나지 않는 것이고, Liveness는 목적지에 실제로 도착하는 것입니다. 차고에만 박혀 있는 자동차는 절대 사고가 나지니 Safety는 완벽하지만, Liveness는 빵점인 셈이죠. 오늘은 제가 과거 Xen 가상 머신 간 통신 프로토콜인 vchan을 설계하며 겪었던 Liveness 증명에 대한 이야기를 해보려 합니다.
사실 저는 꽤 오래전인 2018년에 이 vchan 프로토콜의 명세를 TLA+라는 정형 명세 언어로 작성한 적이 있습니다. 당시에는 Integrity(무결성), 즉 수신한 데이터가 전송한 데이터와 일치한다는 Safety 속성은 기계적으로 증명해 냈습니다. 하지만 Availability(가용성), 즉 전송된 데이터가 '결국' 도착한다는 Liveness 속성을 증명하는 데는 실패했습니다. 당시 TLA+ 증명 시스템인 TLAPS가 시간 논리(Temporal Logic)를 제대로 처리하지 못했기 때문입니다. 그저 종이에 끄적이며 "이론상 맞다"고 위안 삼을 수밖에 없었죠. 그런데 최근 TLAPS 도구들이 업데이트되면서 드디어 이 묵은 과제를 해결할 수 있게 되었습니다. 도구가 발전하여 이제는 '언젠가 일어날 일'을 수학적으로 보증할 수 있게 된 것입니다.
Liveness를 증명하기 위해 가장 먼저 해야 할 일은 시스템을 단순화한 모델을 만드는 것입니다. 발신자(Sender)와 수신자(Receiver), 그리고 그 사이의 버퍼(Buffer)만 남겨두고 생각해 봅시다. 여기서 중요한 변수는 지금까지 보낸 총바이트 수(Sent)와 받은 총바이트 수(Got)입니다. 우리가 증명하고 싶은 Liveness 속성은 Sent = n ~> Got >= n이라는 수식으로 표현됩니다. 해석하자면 "n 바이트를 보냈다면, 결국에는(~) n 바이트 이상을 받게 된다"는 뜻입니다. 여기서 물결 화살표(~>)는 시간 논리 연산자로, "지금 당장은 아니더라도 미래의 어느 시점에는 반드시"라는 의미를 내포하고 있습니다. 이것이 일반적인 프로그래밍의 조건문과 가장 큰 차이점입니다.
이 증명을 성공시키기 위해서는 시스템의 동작(Action)뿐만 아니라 공정성(Fairness)을 명시해야 합니다. 단순히 "수신자는 데이터를 읽을 수 있다"라고만 정의하면, 수학적으로는 수신자가 평생 아무것도 안 하고 놀고 있는 상태도 유효한 동작으로 간주해 버립니다. 그래서 우리는 약한 공정성(Weak Fairness, WF)이라는 개념을 도입해야 합니다. "수신자가 데이터를 읽을 수 있는 상태가 계속된다면, 결국에는 읽는 동작을 수행한다"는 조건을 명세에 추가하는 것이죠. TLA+에서 Spec == ... /\ WF_vars(Recv) 같은 형태가 바로 이런 의미입니다. 이 한 줄이 들어가야만 시스템이 영원히 멈춰 있지 않음을 보장할 수 있습니다.
하지만 실제 증명 과정은 생각보다 까다롭습니다. TLA+의 기반이 되는 시간 논리(Temporal Logic)는 우리가 흔히 쓰는 1차 논리(First Order Logic)와는 세계관이 다르기 때문입니다. 예를 들어 [](Sent = 4)라는 명제는 "현재도 Sent가 4이고, 앞으로 펼쳐질 모든 미래의 세계에서도 Sent는 4이다"를 의미합니다. TLAPS와 같은 증명 도구는 숫자 계산에는 능숙하지만, 이런 '시간의 흐름'을 다루는 모달 논리(Modal Logic)에는 취약했습니다. 그래서 증명 전략을 영리하게 짜야 합니다. 먼저 시간 개념이 없는 불변식(Invariants)들을 일반 논리로 증명하고, 시간의 흐름이 필요한 부분만 최소화하여 PTL(Propositional Temporal Logic)이라는 별도의 솔버에게 맡기는 식입니다.
결국 제가 이 복잡한 수식과 씨름하며 얻은 깨달음은 단순합니다. 엔지니어링에서 '믿음'은 위험하다는 것입니다. "코드를 잘 짰으니 멈추지 않겠지"라고 막연히 믿는 것과, 수학적으로 "이 시스템은 멈출 수 없다"고 증명하는 것은 차원이 다른 문제입니다. 물론 모든 비즈니스 로직에 TLA+를 도입할 수는 없습니다. 리소스 낭비일 수 있죠. 하지만 데이터 손실이 치명적이거나, 분산 시스템의 코어 로직을 다룰 때라면 Liveness를 증명하려는 시도는 충분히 가치 있습니다. 여러분도 해결되지 않는 버그나 교착 상태 때문에 막막함을 느낀다면, 한 번쯤은 코드를 떠나 시스템의 논리적인 뼈대를 점검해 보시길 권합니다. 도구는 계속 발전하고 있고, 우리가 증명할 수 있는 영역도 그만큼 넓어지고 있으니까요.
