당신은 매우 효율적인 컴퓨터 프로그램을 만들려고 노력 중이지만, 도구를 관리하는 두 가지 매우 다른 방식 사이에서 고민에 빠졌다고 상상해 보세요. 한편에는 **가비지 컬렉션(Garbage Collection)**이 있습니다. 이는 도움이 되지만 느린 로봇으로, 당신의 작업 공간을 끊임없이 돌아다니며 당신이 떨어뜨린 오래된 도구들을 주워 담아 버림으로써 당신이 공간 부족 문제에 직면하지 않도록 해줍니다. 이것은 안전하지만, 실제 작업 시간을 뺏어갑니다. 다른 한편에는 **리전 기반 메모리(Region-Based Memory)**가 있습니다. 이는 엄격한 시스템으로, 특정 작업(리전)을 위해 하나의 "상자"를 만들고 그 안에 모든 도구를 넣은 다음, 작업이 끝나면 그 상자와 그 안의 모든 것을 즉시 으스러뜨려 버립니다. 이것은 믿을 수 없을 정도로 빠르지만, 한 가지 엄격한 규칙을 따라야만 합니다. 바로 작업을 마치고, 도구를 정리하고, 다음 작업을 시작하기 전에 반드시 상자를 떠나야 한다는 것입니다.

이제, 여기에 **대수적 효과(Algebraic Effects)**를 더한다고 상상해 보세요. 이것은 "일시 정지 및 재개" 버튼과 같은 마법입니다. 이 버튼은 작업을 중간에 멈추고, 문제를 처리하기 위해 누군가에게 작업을 넘긴 다음, 다시 원래 있던 자리에서 정확히 작업을 이어갈 수 있게 해줍니다. 문제는 이 마법 버튼이 메모리 상자의 엄격한 "완료 후 떠나기" 규칙을 깨뜨린다는 점입니다. 만약 당신이 작업을 일시 정지하고, 이를 다른 사람에게 넘겼는데, 그 사람이 다시 작업을 일시 정지한다면, 당신은 이미 으스러진 상자에서 도구를 꺼내려 할 수도 있습니다. 이는 위험한 난장판을 만듭니다. 오랫동안 컴퓨터 과학자들은 프로그램 안에 메모리 상자의 속도와 일시 정지 버튼의 유연성을 동시에 가질 수 없다고 생각했습니다.

이 논문은 이 두 친구를 드디어 화해시키는 새로운 프로그래밍 언어인 Yarrow를 소개합니다. 저자들인 Anders Alnor Mathiasen, Amin Timany, Lars Birkedal은 (Yarrow Logic이라는) 논리 체계를 만들어냈습니다. 이 체계는 일시 정지 및 재개 마법을 사용하면서도 메모리 상자를 깨뜨리지 않도록 관리하는 일종의 안전 검사관 역할을 합니다. 그들은 이것이 수학적으로 작동함을 증명하여, 프로그램이 시간 여행하듯 이리저리 움직이는 중에도 빠르고 즉각적인 삭제가 가능한 메모리 상자를 사용할 수 있음을 보여주었습니다. 그들은 게임 상태 저장(체크포인팅)이나 여러 작업을 동시에 처리하는 것과 같은 여러 사례로 이를 테스트했으며, 느린 가비지 컬렉션 로봇 없이도 프로그램이 더 빠르고 안전하게 실행될 수 있음을 입증했습니다.

Yarrow의 이야기: 시간 여행하는 메모리를 길들이기

Yarrow가 이 퍼즐을 어떻게 해결했는지 그 이야기를 깊이 파헤쳐 봅시다. 승리를 이해하려면 먼저 악당인 **스택 규율(stack discipline)**과 경계 지정된 연속체(delimited continuations) 사이의 갈등을 먼저 보아야 합니다.

컴퓨터 메모리의 세계에서, 접시 더미를 상상해 보세요. 작업을 시작할 때 당신은 맨 위에 새 접시(리전)를 놓습니다. 작업을 수행하고, 작업이 끝나면 접시를 치웁니다. 이것이 "스택 규율"입니다. 단순하고, 안전하며, 빠릅니다. 그런데 **효과 핸들러(Effect Handler)**라는 마법의 일시 정지 버튼이 등장합니다. 이 버튼을 누르면 컴퓨터는 멈추고, 현재 상태를 저장한 뒤, 문제를 처리하기 위해 프로그램의 다른 부분으로 점프합니다. 다시 돌아올 때, 그것은 마치 시간 여행과 같습니다.

여기 위험이 있습니다. 만약 당신이 작업을 일시 정지하면, 당신이 작업하던 "접시"(메모리 리전)는 작업이 끝난 것으로 간end되어 으스러질 수 있습니다. 하지만 당신이 시간 여행을 하여 다시 복귀했을 때, 당신은 으스러진 접시 위의 도구를 잡으려 하게 됩니다. 일반적인 프로그램에서 이것은 재앙입니다. 과거에는 이를 피하기 위해 프로그래머들이 느린 "가비지 컬렉션" 로봇을 사용해야 했습니다. 왜냐하면 로봇은 접시가 비어 있는 것처럼 보이더라도 어떤 도구가 여전히 사용 중인지 알아낼 만큼 똑똑하기 때문입니다.

저자들은 대담한 질문을 던졌습니다. 우리가 시간 여행하는 일시 정지 기능이 있음에도 불구하고, 빠른 리전 기반 메모리를 계속 사용할 수 있을까?

그들은 그렇다고 말합니다. 단, 우리가 어떻게 일시 정지하는지에 대해 매우 주의한다면 말이죠. 그들은 두 가지 유형의 일시 정지 사이의 결정적인 차이를 발견했습니다:

1. 원샷 효과 (One-Shot Effects, "단 한 번의" 일시 정지): 작업을 일시 정지하고 친구에게 넘겼는데, 친구가 그 일을 딱 한 번 수행하고 다시 돌려주는 상황을 상상해 보세요. 이 시나리오에서 메모리 상자는 안전합니다. 저자들은 일시 정지할 때 메모리 상자가 작업과 함께 "캡처"된다는 것을 보여줍니다. 다시 재개할 때, 상자는 이전과 똑같이 복구됩니다. 이는 영화의 한 장면을 얼려두는 것과 같습니다. 영화가 재개될 때 소품들은 여전히 그 자리에 있습니다.
2. 멀티샷 효과 (Multi-Shot Effects, "반복되는" 일시 정지): 이제 작업을 일시 정지했는데, 친구가 그 일시 정지 버튼을 사용하여 작업을 반복해서 여러 번 다시 시작할 수 있는 상황을 상상해 보세요. 여기서부터 까다로워집니다. 만약 일시 정지하면 메모리 상자가 캡처됩니다. 하지만 친구가 일시 정지를 다시 사용한다면, 그들은 본질적으로 동일한 상자를 두 번 사용하려고 하는 것입니다. 저자들은 이 경우, 첫 번째 사용 후에 메모리 상자가 "으스러진" 것으로 간주되어야 한다고 설명합니다. 만약 그 상자의 도구를 두 번째로 사용하려 한다면, 그것은 안전하지 않습니다. 논문은 이러한 멀티샷 일시 정지를 여전히 사용할 수 있지만, 엄격해야 함을 증명합니다. 즉, 상자 안의 도구는 오직 한 번만 사용할 수 있습니다.

이것을 가능하게 하기 위해 팀은 **Yarrow Logic (YL)**을 구축했습니다. 이 논리는 고도의 규칙 책이라고 생각하면 됩니다. 이것은 단순히 코드가 올바르게 작성되었는지 확인하는 것이 아니라, 실시간으로 메모리 스택의 "형태"를 추적합니다. 어떤 메모리 상자가 현재 활성화되어 있는지, 그리고 어떤 상자가 일시 정지 버튼에 의해 캡처되었는지를 정확히 알고 있습니다.

저자들은 단순히 추측한 것이 아니라, 이것이 작동함을 증명했습니다. 그들은 Iris(분리 논리 프레임워크)라는 강력한 수학적 도구와 Rocq Prover(수학적 증명을 검증하는 컴퓨터)를 사용하여 모든 단계를 검증했습니다. 그들은 Yarrow Logic의 규칙을 따른다면, 프로그램이 시간 여행하는 일시 정지 기능을 사용하더라도 메모리 오류로 인해 절대 충돌하지 않을 것임을 보여주었습니다.

사례 연구: Yarrow를 시험대에 올리다

Yarrow가 단순한 이론이 아님을 보여주기 위해, 저자들은 몇 가지 실제적인 예시를 구축하여 테스트했습니다.

• LIFO 데이터 구조 (스택): 그들은 "후입선출(Last-In, First-Out)" 스택(팬케이크 더미 같은 것)을 만들었습니다. 보통 이런 것들은 느린 가비지 컬렉션 메모리로 구축됩니다. Yarrow에서는 이를 빠른 리전 기반 메모리를 사용하여 구축했습니다. 결과는 어떠했을까요? 스택은 팬케이크를 치우기 위해 가비지 컬렉터를 필요로 하지 않기 때문에 더 안전하고 빠릅니다.
• 체크포인팅 (게임 저장): 비디오 게임을 하다가 진행 상황을 저장하고 나중에 불러오는 상황을 상상해 보세요. 저자들은 프로그램의 상태를 "저장(체크포인트)"하고 "로드"할 수 있는 시스템을 만들었습니다. 그들은 프로그램이 시간을 앞뒤로 넘나들더라도, 체크포인트를 위해 사용된 메모리가 안전하게 관리됨을 증명했습니다. 만약 이미 사용된 체크포인트(멀티샷 효과)를 다시 불러오려 한다면, 시스템은 그것이 안전하지 않음을 인지하고 오래된, 으스러진 메모리를 사용하는 것을 방지합니다.
• 비동기 계산 (멀티태스커): 웹 서버가 많은 사용자를 처리하는 것처럼 여러 작업이 동시에 발생하는 상황을 처리하는 방법을 보여주었습니다. 리전을 사용함으로써, 그들은 느린 가비지 컬렉터를 피하고 서버를 더 효율적으로 만들었습니다.

결론: 우리가 아는 것과 모르는 것

이 논문은 자신들이 무엇을 달성했는지에 대해 매우 명확하게 밝히고 있습니다. 그들은 대수적 효과(일시 정지 버튼)와 리전 기반 메모리(빠른 상자)를 결합하면서도 안전성을 깨뜨리지 않을 수 있음을 공식적으로 증명했습니다. 그들은 새로운 언어인 Yarrow와 논리 체계인 YL을 만들어 이를 가능하게 했습니다. 또한 컴퓨터 증명 보조 도구를 사용하여 이를 검증했으므로, 이 논리가 타당하다는 점을 매우 확신할 수 있습니다.

하지만 논문은 또한 명확한 선을 긋습니다. 그들은 멀티샷 일시 정지(반복되는 일시 정지)를 사용하여 동일한 메모리 상자를 여러 번 사용하는 것에 대해 명시적으로 반대합니다. 만약 당신이 멀티샷 일시 정지에 의해 "캡처된" 메모리 리전을 두 번 이상 사용하려고 시 한다면, 논문은 그것이 안전하지 않음을 증명합니다. 저자들은 메모리 상자를 "복사"하여 안전하게 만들 수 있다는 아이디어를 거부하며, 대신 메모리가 첫 번째 사용 후에 회수되도록 강제합니다.

또한 그들은 수학과 논리는 갖추었지만, 아직 실제 세계에서 얼마나 더 빠른지를 측정할 수 있는 완전한 실행 가능한 컴퓨터 프로그램(프로토타입 런타임)을 구축하지는 않았다고 언급합니다. 그들은 프로토타입을 구축하는 것이 실질적인 속도 향상을 확인하기 위한 훌륭한 다음 단계가 될 것이라고 제안합니다. 또한 그들의 접근 방식이 특정 유형의 메모리 관리에 적용되며, 이를 Java 가상 머신(JVM)과 같은 다른 복잡한 시스템과 결합하는 것은 까다로울 수 있으며 현재는 정의되지 않은 동작(undefined behavior)이라고 언급했습니다.

요약하자면, Yarrow는 큰 진전입니다. 이는 우리가 가비지 컬렉션의 안전함과 수동 메모리 관리의 속도 사이에서 하나를 선택할 필요가 없음을 보여줍니다. 적절한 규칙이 있다면, 시간 여행하는 일시 정지의 한계를 존중하는 한 우리는 두 세계의 장점을 모두 가질 수 있습니다. 저자들은 메모리와 시간의 이 복잡한 춤이 안전하게 수행될 수 있음을 수학적 토대를 마련해 두었으며, 미래의 엔지니어들이 빠르고 안전한 프로그램을 만들 수 있도록 길을 열어두었습니다.