Mechanizing Asynchronous Distributed Algorithms in Rocq: The Echo Algorithm as a Case Study

현대 세계를 움직이는 거대하고 보이지 않는 네트워크 속에서, 컴퓨터들은 문제를 함께 해결하기 위해 끊임없이 정보를 교환합니다. 분산 알고리즘이라고 알려진 이 시스템들은 글로벌 금융 거래부터 인터넷 트래픽 라우팅에 이르기까지 모든 것의 배후에 있는 보이지 않는 엔진입니다. 엄격하고 선형적인 지침을 따르는 단일 컴퓨터와 달리, 분산 시스템은 중앙의 관리자 없이도 서로 협력해야 하는 독립적인 기계들의 집합체입니다. 이들은 비동기 환경에서 작동하는데, 이는 이들을 동기화할 수 있는 단일한 시계가 없음을 의미합니다. 메시지는 예측 불가능한 속도로 이동하며, 메시지가 도착하는 순서는 매우 다양할 수 있습니다. 이러한 전역적 스케줄의 부재는 독특한 과제를 안겨줍니다. 즉, 이벤트의 타이밍이 혼란스럽고 예측 불가능할 때 어떻게 시스템이 올바르게 작동할 것이라고 확신할 수 있는가 하는 점입니다. 수십 년 동안 수학자와 컴퓨터 과학자들은 시스템이 대부분의 경우에 잘 작동하는지 테스트하는 것을 넘어, 논리를 사용하여 시스템이 실패할 수 없음을 증명하는 엄격한 방법인 형식 검증(formal verification)에 의존해 왔습니다.

한 연구팀은 이제 이 엄격한 논리를 컴퓨터 과학의 고전적인 문제인 에코(Echo) 알고리즘에 적용했습니다. 이 알고리즘은 네트워크의 컴퓨터들이 구조에 합의하기 위한 근본적인 방법으로, 본질적으로 연결 구조의 지도를 구축하여 중앙 컴퓨터인 개시자(initiator)가 다른 모든 노드와 통신할 수 있도록 합니다. 과정은 개념적으로 단순합니다. 개시자가 이웃들에게 신호, 즉 '토큰(token)'을 보냅니다. 그 후 이웃들은 자신의 이웃에게 토큰을 전달하며, 결국 신호는 네트워크 전체로 퍼져 나갑니다. 노드가 토큰을 받고 모든 이웃으로부터 응답을 받으면, 출발지를 향해 답장, 즉 '에코(echo)'를 보냅니다. 개시자는 모든 이로부터 에코를 받을 때까지 기다린 후 작업이 완료되었음을 선언합니다. 아이디어 자체는 직관적으로 보이지만, 메시지 지연과 재정렬의 모든 가능한 시나리오 하에서 이 과정이 올바르게 작동함을 증명하는 것은 매우 어렵기로 유명합니다. 연구진은 Rocq라는 전문 증명 보조 도구를 사용하여, 만약 개시자가 작업이 끝났다고 결정한다면 네트워크가 실제로 완전히 탐색되었음을 보여주는 신뢰성 있는 정식 증명을 성공적으로 구축했습니다.

이 연구의 핵심은 모호함을 남기지 않을 만큼 정밀한 알고리즘의 디지털 트윈을 만드는 데 있습니다. 연구진은 전체 네트워크를 하나의 진화하는 상태(evolving state)로 모델링했습니다. 이 상태에는 각 컴퓨터의 현재 상태와 그들 사이를 이동 중인 모든 메시지의 집합이 포함됩니다. 이 모델에서 메시지의 이동은 시계에 의해 제어되는 것이 아니라, 비동기 네트워크의 혼란스러운 현실을 반영하여 어떤 메시지든 언제라도 전달될 수 있도록 허용하는 규칙 세트에 의해 제어됩니다. 그런 다음 연구진은 메시지가 섞이더라도 항상 유효해야 하는 일련의 논리적 규칙, 즉 불변량(invariants)을 정의했습니다. 이 규칙들은 가드레일 역할을 하여, 일부 네트워크가 여전히 대기 중인 상황에서 컴퓨터가 작업을 마쳤다고 착각하는 상태에 빠지지 않도록 보장합니다.

이 연구의 가장 중요한 발견은 결정의 순간에 관한 조건부 증명입니다. 연구진은 개시자 컴퓨터가 작업이 완료되었다고 믿는 상태에 도달하면, 네트워크의 다른 모든 컴퓨터는 개시자로 연결되는 명확하고 유한한 경로를 가지고 있어야 함을 증명했습니다. 즉, 네트워크는 루프나 끊어진 섬 없이 개시자를 루트로 하는 트리 형태의 구조를 성공적으로 형성했다는 것입니다. 이 증명은 놀라운데, 왜냐하면 메시지가 도착하는 순서와 관계없이 성립하기 때문입니다. 이는 메시지가 동일한 연결 경로에서 서로 교차하거나, 컴퓨터가 이미 작업을 시작한 후에 두 번째 신호를 받는 등의 복잡하고 무질서한 시나리오까지 고려한 것입니다. 연구진은 이러한 얽힌 상황에서도 알고리즘의 논리가 개시자의 성급한 결정을 방지한다는 것을 보여주었습니다. 만약 아직 시작하지 않은 컴퓨터를 향해 네트워크를 떠도는 메시지가 하나라도 있다면, 개시자의 내부 카운터가 승리를 선언하는 것을 막아줍니다.

이를 달ern하기 위해 팀은 문제를 별도의 논리 계층으로 분리해야 했습니다. 먼저, 모든 연결이 유효하고 어떤 컴퓨터도 자기 자신을 가리키지 않음을 보장하는 구조적 사실을 확립했습니다. 그다음으로는 인과 계층(causal layer)을 증명하여, 만약 어떤 컴퓨터가 신호를 보냈다면 반드시 그 이전에 신호를 보낸 부모 컴퓨터가 존재하여 시작점까지 이어지는 사슬을 만든다는 것을 보여주었습니다. 마지막으로 연구진은 메시지 송수신 횟수를 추적하는 회계 계층(accounting layer)을 다루었습니다. 이 회계가 증명의 핵심입니다. 이는 단일 컴퓨터의 로컬 상태를 전체 네트워크의 글로벌 상태와 연결합니다. 연구진은 컴퓨터가 모든 이웃으로부터 답장을 받기 전까지는 작업을 마칠 수 없으며, 이 요구 사항이 연결된 체인을 따라 개시자까지 파동처럼 전달된다는 것을 입와했습니다. 단 한 대의 컴퓨터라도 메시지를 기다리고 있다면, 개시자의 카운터에 그것이 반영되어 최종 결정을 막게 됩니다.

이 작업은 특정 네트워크 크기에 대한 시뮬레이션이나 테스트가 아닙니다. 이는 특정 가설을 만족하는 임의의 유한 리스트 그래프에 적용되는 수학적 증명입니다. 연구진은 공식 증명 보조 도구인 Rocq를 사용하여 논리의 모든 단계를 검증했습니다. 140개 이상의 별도 논리 선언을 포함하는 결과 코드는 컴퓨터에 의해 오류가 없음이 검증되었습니다. 이는 이 증명이 숨겨진 결함이 있을 수 있는 인간의 논증이 아니라, 기계에 의해 확인된 보증임을 의미합니다. 연구진은 알고리즘이 항상 결국 끝날 것이라는 점을 증명하려 하지 않았는데, 그러기 위해서는 메시지가 결국 전달될 것이라는 가정이 필요하기 때문이며, 이 조건은 증명의 초점을 안전성(safety)에 맞추기 위해 의도적으로 제외되었습니다. 대신, 그들은 만약 알고리즘이 종료된다면, 올바르게 종료될 것임을 증명했습니다.

이 성과는 복잡한 시스템을 검증하는 방식의 변화를 강조합니다. 문제를 재사용 가능한 구성 요소로 분해함으로써, 연구진은 향후 다른 분산 알고리즘에도 적용될 수 있는 방법을 만들어냈습니다. 다만 현재의 산출물은 임의의 알고리즘을 위한 플러그인 검증 프레임워크는 아니며 다른 사례를 위해서는 재설계가 필요합니다. 현재의 작업은 에코 알고리즘에 특화되어 있지만, 구조적 규칙과 회계 논리를 분리하는 방식은 타이밍이 불확실한 다른 문제들을 다루기 위한 청사진을 제공합니다. 이 증명은 예측 불가능한 지연이 존재하는 세상에서도, 수학적으로 의도한 대로 동작할 것이라고 확신할 수 있는 시스템을 구축하는 것이 가능하다는 것을 확인시켜 줍니다. 연구진은 자신들의 코드와 증명을 다른 이들이 검토하고 활용할 수 있도록 공개하여, 현대 사회를 뒷받침하는 디지털 네트워크의 신뢰성을 확보하기 위한 미래 연구의 견고한 토대를 마련했습니다.