모든 음악가가 작고 독립적인 로봇인 거대한 오케스트라를 상상해 보십시오. 그들에게는 지휘봉을 흔드는 지휘자가 없습니다. 대신, 그들은 서로 조화를 유지하기 위해 서로 대화해야 합니다. 만약 한 로봇이 너무 빨리 음을 연주하거나, 결코 오지 않을 신호를 기다리며 머뭇거린다면, 전체 노래는 혼란스러운 비명 소리로 변하거나, 최악의 경우 모두가 악기를 든 채 아무런 신호도 오지 않아 멍하니 멈춰 서 버릴 것입니다. 이것이 바로 병렬 컴퓨팅의 세계입니다. 수천 개의 컴퓨터 프로세서가 기상 예측이나 핵폭발 시뮬레이션과 같은 거대한 문제를 해결하기 위해 함께 협력하는 곳이죠. 이들이 사용하는 언어는 MPI(Message Passing Interface)라고 불립니다. 이는 강력하지만, 동시에 지뢰밭이기도 합니다. 만약 당신이 10대의 로봇을 위한 프로그램을 작성한다면 완벽하게 작동할 수도 있습니다. 하지만 동일한 코드를 1만 대의 로봇에서 실행하려고 하면, 프로그램이 충돌하거나, 데드락(deadlock, 교착 상태)에 빠지거나, 엉터리 결과를 만들어낼 수도 있습니다. 과학자들이 던져온 핵심 질문은 이것입니다: "우리가 모든 가능한 로봇의 숫자를 일일이 테스트하지 않고도, 어떤 수의 로봇을 투입하더라도 프로그램이 올바르게 작동할 것이라는 것을 어떻게 증명할 수 있을까?"

여기서 스티븐 F. 시겔(Stephen F. Siegel)의 논문이 기발한 트릭을 들고 등장합니다. 그는 특정 유형의 컴퓨터 프로그램, 즉 로봇들이 결정론적(deterministic)인 경우, 즉 엄격하고 예측 가능한 스크립트를 따르며 누구와 대화할지에 대해 무작위적인 선택을 하지 않는 경우의 "매개변수화된 검증(parameterized verification)" 문제를 다룹니다. 시겔과 그의 팀은 C 언어(흔히 쓰이는 프로그래밍 언어)와 MPI로 작성된 복잡한 병렬 프로그램을, 컴퓨터가 오류를 체크할 수 있는 단순한 순차적 이야기로 마법처럼 변환하는 방법을 개발했습니다. 이것은 마치 모두가 동시에 달리고 있는 복잡한 다중 스레드 미로를 가져와서, 이를 하나의 직선 형태의 복도로 평평하게 펼치는 것과 같습니다. 이렇게 함으로써, 그들은 기존의 강력한 도구들을 사용하여 해당 프로그램이 프로세스 개수가 1개든 무한대이든 상관없이 데드락이나 논리적 오류로부터 자유롭다는 것을 증명할 수 있습니다. 그들은 단순히 추측한 것이 아니라, 이 단순화된 버전이 올 আর바르다면 원래의 혼란스러운 병렬 버전도 반드시 올바를 것이라는 점을 수학적으로 증명했습니다. 그들은 열 확산(heat diffusion) 및 데이터 브로드캐스트(broadcast)를 시뮬레이션하는 프로그램을 포함하여 다섯 가지의 실제 프로그램에 이 방법을 테스트했으며, 도구들은 이들을 모두 성공적으로 검증하여 이 방법이 실제로 작동함을 입증했습니다.

"유령" 번역가의 마법

이것이 어떻게 작동하는지 이해하기 위해, 컴퓨터 프로세스들을 교실에서 쪽지를 주고받으려는 친구들의 모임이라고 상상해 봅시다. 일반적인 병렬 프로그램에서는 친구 A가 친구 B에게 쪽지를 보내는 동안, 동시에 친구 C가 친구 D에게 쪽지를 보낼 수 있습니다. 만약 친구 A가 쪽지를 보내기 전에 B의 답장을 기다리고 있는데, B 또한 A의 답장을 기다리고 있다면, 그들은 "데드락(deadlock)" 상태, 즉 아무도 움직이지 않는 침묵의 대치 상태에 빠지게 됩니다. 이를 확인하는 것은 보통 악몽과 같은 일인데, 왜냐하면 친구들이 늘어남에 따라 그들이 상호작용할 수 있는 방식이 폭발적으로 증가하기 때문입니다.

시겔의 접근 방식은 마치 학급 전체를 지켜보며 실제 타이밍에 상관없이 무엇이 일어나야 하는지에 대한 "스크립트"를 작성하는 매우 똑똑한 번역가를 두는 것과 같습니다. 번역가는 현실 세계의 혼돈에는 관심이 없습니다. 대신 프로그래머에게 몇 가지 구체적인 단서를 요청합니다:

1. 메시지 개수: 친구 A가 친구 B에게 보낼 쪽지는 총 몇 개인가?
2. 메시지 내용: 그 쪽지들에 무엇이 적혀 있는가? (예: "숫자 5" 또는 "우리 점수의 합계")
3. 타임라인: 모든 송신 및 수신 메시지에 대한 "레벨(level)" 번호를 부여하여, 이벤트의 타임라인이 절대 역순으로 루프를 형성하지 않도록 보장합니다.

이 단서들을 가지고 번역가는 마법을 부립니다. 번젝트는 send와 receive 명령이 있는 원래의 프로그램을 가져와서 그것들을 제거합니다. 그 자리에 "유령(ghost)" 변수들, 즉 메시지가 얼마나 송신되고 수신되었는지를 추적하는 가상의 카운터를 삽입합니다. 쪽지를 보내는 행위는 "이 쪽지가 스크립트와 일치하는가?"라는 단순한 확인 작업으로 대체되며, 받는 행위는 "스크립트와 일치하는 쪽지를 선택하라"는 선택 작업으로 대체됩니다.

갑자기, 프로그램은 더 이상 수천 명의 친구들이 벌이는 혼란스러운 춤이 아닙니다. 그것은 한 사람이 스크립트를 따라가며 체크박스를 채워 나가는 단일한 선형적 이야기입니다. 만약 이 단일한 선형 이야기가 완벽하다면(데드락이 없고 수학적으로 정확하다면), 원래의 혼란스러운 버전도 반드시 완벽할 것이라는 점이 보장됩니다. 이는 마치 레시피가 하나의 케이크에 적합하다는 것을 증명함으로써, 그 천만 번째 케이크를 직접 굽지 않고도 백만 개의 케이크를 굽는 데에도 그 논리가 유효하다는 것을 아는 것과 같습니다.

"레벨" 시스템: 시계 없이 시간을 관리하기

이 방법의 가장 뛰어난 부분 중 하나는 "발생 전(happens-before)" 관계를 처리하는 방식입니다. 병렬 세계에서 만약 앨리스가 밥에게 쪽지를 보내고, 밥이 찰리에게 쪽지를 보낸다면, 우리는 앨리스의 쪽지가 찰리의 쪽지보다 먼저 일어났음을 압니다. 하지만 만약 앨리스와 밥이 동시에 서로에게 쪽지를 보낸다면 어떻게 될까요? 누가 먼저일까요?

논문은 "레벨(levels)"이라는 개념을 도입합니다. 모든 프로세스가 메시지를 보내거나 받을 때마다, 그것은 시계 시간(clock time)이 아닌, 단순히 올라가는 숫자 형태의 타임스탬프를 얻는다고 상상해 보십시오. 규칙은 간단합니다. 메시지를 보낼 때마다 레벨이 올라갑니다. 메시지를 받을 때마다 레벨은 훨씬 더 높게 올라갑니다. 만약 당신이 레벨을 낮추어야 하는 메시지를 받으려고 시도한다면, 시스템은 "정지! 이것은 불가능합니다!"라고 외칩니다.

이것은 타임라인이 루프를 형성하지 않도록 보장합니다. 만약 A가 B를 기다리고, B가 C를 기다리며, C가 다시 A를 기다리는 루프가 있다면, 레벨은 올라갔다가 다시 내려가야 원을 완성할 수 있습니다. 레벨은 오직 올라갈 수만 있으므로, 이러한 루프는 불가능합니다. 이 수학적 트릭은 프로세스가 몇 개가 참여하든 프로그램이 데드락에 빠지지 않을 것임을 증명합니다.

이론에서 현실로: 다섯 가지 테스트 케이스

저자들은 이론에만 머물지 않았습니다. 그들은 아이디어를 실제 코드에 테스트하기 위해 VMFC(Verified MPI for Frama-C)라는 도구를 구축했습니다. 그들은 다섯 가지 서로 다른 C/MPI 프로그램을 가져와 이 변환 과정을 적용했습니다. 이 프로그램들은 다음을 포함합니다:

• Cyclic Sum: 숫자를 돌려가며 모두 더하기 위해 고리 형태로 연결된 프로세스들.
• Allsum: 중앙 프로세스가 다른 모든 이들로부터 데이터를 수집하는 별 모양 네트워크.
• Diffuse1d: 이웃 간에 "고스트(ghost)" 데이터를 교환하며 온도 변화를 계산하는 1차원 선 위의 열 확산 시뮬레이션.
• Broadcast: 한 프로세스가 모두에게 동일한 데이터를 전송함.
• Gather: 모두가 한 중앙 프로세스로 자신의 데이터를 전송함.

각 사례에 대해, 도구는 병렬 코드를 순차 버전으로 자동 변환했습니다. 그 후, 자동 정리 증명기(mathematical engines)를 사용하여 논리를 검사했습니다. 결과는 인상적이었습니다. 다섯 가지 프로그램 모두가 어떠한 수의 프로세스에 대해서도 올바르다는 것이 증명되었습니다. 검증 작업은 표준 노트북에서 프로그램당 1분도 걸리지 않았습니다.

이 방법이 하지 못하는 것 (그리고 그것이 중요한 이유)

이 방법이 하지 못하는 일을 아는 것도 중요합니다. 그곳에 실제 세계의 한계가 있기 때문입니다. 논문은 이 접근 방식이 오직 "결정론적(deterministic)" 프로그램에서만 작동한다고 명시합니다. 즉, 프로세스들이 "누구로부터든 메시지를 받겠다"와 같은 와일드카드(wildcard)를 사용할 수 없다는 뜻입니다. 만약 프로그램이 "누구든 먼저 보내는 사람의 메시지를 받겠다"라고 한다면, 깔끔하고 예측 가능한 스크립트는 깨지게 되며, 번역가는 타임라인을 보장할 수 없습니다. 저자들은 대부분의 과학 코드가 이러한 와일드카드 없이 작성될 수 있다고 주장하며, 이것이 큰 제한 사항은 아니지만 명확한 경계선임을 밝히고 있습니다.

또한, 이 논문은 모든 병렬 프로그램을 해결한다고 주장하지 않습니다. 이 방식은 특정 하위 집합의 MPI 연산(표준 블로킹 송신 및 수신)에 초점을 맞추고 있으며, 아직 비블로킹(non-blocking) 연산이나 복잡한 파생 데이터 타입을 다루지는 않습니다. 그러나 저자들은 병렬 검증을 순차 검증으로 변환하는 핵심 아이디어가 견고한 토대라는 점을 확신하고 있습니다. 그들은 이 접근 방식이 Frama-C뿐만 아니라 다른 도구와 언어로 확장될 수 있다고 제안합니다.

요약

결국, 이 논문은 거대한 병렬 프로그램을 작성할 때 안심하고 잠들 수 있는 방법을 제공합니다. 100개의 프로세스로 테스트를 통과했기 때문에 프로그램이 잘 작동할 것이라고 막연히 희망하는 대신, 당신은 그것이 10억 개의 프로세스에서도 작동할 것임을 수학적으로 증명할 수 있습니다. 혼란스러운 다차원 문제를 단순한 1차원 이야기로 바꿈으로써, 시겔과 그의 팀은 컴퓨터 과학자들에게 코드 속의 진실을 볼 수 있는 강력한 새로운 렌즈를 제공했습니다. 이는 때때로 전체의 복잡성을 이해하기 위해서는, 그 부분의 이야기를 단순화하는 것이 필요하다는 사실을 상기시켜 줍니다.