💻 computer science

Building Extensible Program Logics through Effect Handlers

이 논문은 동시성과 충돌 복구와 같은 복잡한 동작을 모델링하기 위해 기본 로직 내에 이펙트 핸들러(effect handlers)를 구현함으로써 확장 가능한 프로그램 로직을 구축하는 접근 방식을 제안하며, 이를 통해 표현력이 풍부한 추론 규칙과 관계적 정교화(relational refinements)를 모듈식이고 재사용 가능한 방식으로 도출할 수 있게 한다.

원저자: Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti

게시일 2026-07-15

📖 5 분 읽기🧠 심층 분석

CC BY 4.0

원저자: Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

당신은 디지털 성을 보호하기 위해 초강력 보안 요새를 구축하려고 한다고 상상해 보십시오. 컴퓨터 과학의 세계에서 이러한 요새는 **프로그램 논리(program logics)**라고 불립니다. 이는 수학자와 프로그래머가 소프트웨어가 절대 충돌하거나, 비밀을 유출하거나, 이상한 행동을 하지 않도록 증명하기 위해 사용하는 엄격한 규칙들의 집합입니다.

오랫동안 이러한 요새를 짓는 것은 마치 모든 벽돌을 일일이 손으로 깎아 만드는 것과 같았습니다. 만약 당신이 새로운 기능(예를 들어, 전원 차단 상황을 처리하는 방식(장애 복구)이나 다른 컴퓨터와 통신하는 방식(분산 시스템))을 추가하고 싶다면, 처음부터 다시 시작해야 했습니다. 당신에게는 단순히 요새를 사용하는 기술과는 완전히 다른 종류의 "벽돌 쌓기" 기술이 필요했습니다. 그것은 어렵고 느렸으며, 예전 요새에서 쓰던 벽돌을 새 요서지를 짓는 데 쉽게 재사용할 수 없었습니다.

핵심 아이디어: "이펙트 핸들러(Effect Handler)" 도구 상자

Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti가 작성한 이 논문은 이러한 요새를 만드는 새로운 방법을 제안합니다. 벽돌을 손으로 깎는 대신, 그들은 **이펙트 핸들러(effect handlers)**라는 마법 같은 도구를 사용합니다.

이펙트 핸들러를 게임의 커스터마이징 가능한 규칙책이라고 생각해 보십시오. 표준 비디오 게임에서는 점프하거나 사격하는 규칙이 엔진에 이미 하드코딩되어 있습니다. 하지만 이펙트 핸들러를 사용하면, 게임 엔진은 "나는 아직 '점프'가 무엇인지 모르지만, 누군가 나에게 알려줄 때까지 기다리겠다"라고 말합니다. 그러면 프로그래머는 "알았어, 플레이어가 점프하려고 하면, 1초 동안 공중에 떠 있게 만들게"라고 말하는 작은 스크립트(핸들러)를 작성할 수 있습니다.

저자들은 아무런 규칙도 없지만, 이 "지침을 기다리는" 기능만 있는 아주 작은 빈 언어인 FicusLang을 만들었습니다. 그런 다음 그들은 다음과 같은 것들을 만들어내기 위한 핸들러를 작성했습니다:

메모리(Memory): 프로그램이 무언가를 기억하는 방식 (예: 포스트잇).
동시성 스레드(Concurrent Threads): 프로그램이 동시에 여러 일을 하는 방식 (예: 여러 개의 팬을 돌리며 요리하는 요리사).
충돌(Crashes): 전원이 나가고 다시 들어왔을 때 발생하는 일.
분산 시스템(Distributed Systems): 컴퓨터들이 불안정한 네트워크를 통해 서로 통신하는 방식.

마법의 기술: 쌓아 올리기

가장 멋진 부분은 그들이 단순히 이 규칙들을 만든 것이 아니라, 그것들을 증명했다는 것입니다. 그들은 빈 언어에서 시작하여 "메모리"를 위한 핸들러를 작성했고, 그 메모리 핸들러가 올바르게 작동한다는 것을 증명하기 위해 Ficus라는 논리 시스템을 사용했습니다. 일단 이 메모리 핸들러가 증명되면, 이를 사용하여 "동시성" 핸들러를 구축할 수 있습니다.

이것은 집을 짓는 것과 같습니다. 먼저 기초가 튼튼한지 증명합니다. 그다음, 그 튼튼한 기초를 사용하여 1층을 만듭니다. 일단 1층이 안전하다고 증명되면, 그 1층을 사용하여 2층을 만듭니다. 이 방식으로 구축했기 때문에 그들은 기능을 쉽게 섞거나 조합할 수 있었습니다. 만약 당신이 수영장과 차고가 모두 있는 집을 원한다면, 전체 기초를 다시 지을 필요 없이 "수영장 핸들러"와 "차고 핸들러"를 결합하기만 하면 됩니다.

더 강력한 규칙과 새로운 기술들

핸들러를 사용하여 밑바닥부터 규칙을 구축했기 때문에, 그들은 이전 방법들보다 더 강력한 규칙을 만들 수 있다는 것을 발견했습니다.

"일시 정지(Pause)" 기술: 표준 동시성 프로그래밍에서 컴퓨터는 다른 작업으로 전환하기 위해 아주 미세한 순간에도 작업을 멈출 수 있습니다. 이는 추적하기 어려운 거대한 가능성의 혼란을 야기합니다. 저자들의 핸들러는 특정 "이펙트"가 발생할 때(예: 파일을 읽으라는 요청)만 작업을 전환합니다. 이 방식은 "언제든 멈출 수 있는" 방식만큼 안전하면서도, 훨씬 더 다루기 쉽다는 것을 그들은 증명했습니다.
"수정구슬(Prophecy Variables)": 때때로 프로그램을 안전하다고 증명하려면, 어떤 무작위 사건이 어떻게 일어날지 미리 알아야 할 때가 있습니다. 저자들은 "수정구슬" 이펙트 핸들러를 만들었습니다. 이것은 증명이 "이 무작위 숫자가 5가 될 것이라고 예측한다"라고 말한 뒤, 나중에 실제로 맞았는지 확인하게 해줍니다. 그들은 거대한 글로벌 수정구슬으로부터 로컬 수정구슬(특정 변수에 대한 것)을 만들 수 있으며, 심지어 프로그래머가 추가 코드를 작성하지 않아도 메모리 작업에 대해 자동으로 나타나게 할 수 있음을 보여주었습니다.

"관계적(Relational)" 논리: 쌍둥이 테스트

이 논문은 또한 RelFicus라는 새로운 도구를 소개합니다. 당신에게 똑같이 생긴 쌍둥이인 프로그램 A와 프로그램 B가 있다고 상상해 보십시오. 당신은 만약 동일한 입력을 준다면, 한쪽이 다른 쪽과 약간 다르더라도 두 프로그램이 항상 똑같이 행동할 것임을 증명하고 싶습니다.

RelFicus는 당신이 머릿속에서 이 두 프로그램을 나란히 실행하여(고스트 상태나 가상의 자원을 사용하여) 그들이 쌍둥이임을 증명할 수 있게 해주는 논리입니다. 이는 그들의 새로운 "요청 시에만 일시 정지하는" 동시성 핸들러가 실제로 안전하다는 것을 증명하는 데 매우 중요합니다. 그들은 이 쌍둥이 테스트를 사용하여 추가적인 "일시 정지 지점(preemption)"을 넣는 것이 프로그램의 결과에 영향을 주지 않는다는 것을 증명했으며, 이는 그들의 더 단순하고 사용하기 쉬운 모델을 정당화합니다.

그들이 하지 않은 것 (그리고 거부한 것)

이 논문이 무엇이 아닌지 아는 것도 중요합니다.

그들은 기존의 논리 구축 방식("손으로 깎은 벽돌" 방식)이 쓸모없다고 말하는 것이 아닙니다. 단지 그것이 재사용하기 어렵고 기반을 쌓기 어렵다는 점을 말하는 것입니다.
그들은 이러한 논리를 구축하기 위해 복잡하고 추상적인 수학 구조(이전 연구에서 언급된 "ITrees"와 같은 것)를 이해해야 한다는 생각을 거부합니다. 그들은 자신들의 접근 방식이 개발자들에게 이미 친숙한 표준 프로그래밍 개념(핸들러)을 사용하기 때문에 더 접근하기 쉽다고 주장합니다.
그들은 컴퓨터 보안의 모든 문제를 해결했다고 주장하는 것이 아닙니다. 그들은 메모리, 동시성, 충돌, 분산 시스템을 위한 핸들러를 구체적으로 구축했지만, 다른 기능에는 새로운 핸들러가 필요할 수 있음을 인정합니다.

얼마나 확신하는가?

저자들은 매우 자신감이 있지만, 매우 정밀합니다. 그들은 단순히 이것이 작동할 수도 있다고 "제안"한 것이 아니라, 그것을 증명했습니다.

그들은 Rocq Prover(수학적 증명을 검증하는 컴퓨터 프로그램)라는 도구로 전체 논리 시스템을 작성했습니다.
그들은 **적절성(Adequacy)**이라는 정리를 증명했는데, 이는 그들의 논리가 어떤 프로그램이 안전하다고 말한다면 그 프로그램이 실제로 멈추지 않고 실행될 것임을 보장합니다.
그들은 그들의 새로운 동시성 모델이 표준적이고 더 복잡한 모델들과 동등함을 증명했습니다.
그들은 "수정구슬(prophecy)" 기능이 글로벌 버전으로부터 파생됨을 보여줌으로써 수학적 정당성이 유지됨을 증명했습니다.

핵째 (Takeaway)

이 논문은 컴퓨터 과학자들에게 젖은 진흙 더미 대신 레고 블록을 주는 것과 같습니다. 이전에는 새로운 종류의 성을 짓고 싶다면 직접 진흙을 반죽해야 했습니다. 이제 당신에게는 "메모리", "충돌", "네트워크"를 위한 미리 만들어지고 테스트된 벽돌이 있습니다. 그것들을 서로 끼워 맞출 수 있으며, 수학은 그 성이 무너지지 않을 것임을 보장합니다. 이는 복잡하고 안전한 소프트웨어를 만드는 일을 고독한 예술 프로젝트에서, 누구나 최고의 부품을 재사용할 수 있는 협력적인 건설 현장처럼 만들어 줍니다.

기술 요약: 이펙트 핸들러를 통한 확장 가능한 프로그램 로직 구축

문제 제로 (Problem Statement)

프로그램 로직은 동시성(concurrency), 약한 메모리(weak memory), 분산 실행(distributed execution), 크래시 복구(crash recovery)와 같은 복잡한 프로그램 기능을 검증하는 데 강력한 도구입니다. 그러나 기존의 프로그램 로직 개발 방식은 다음과 같은 상당한 장벽에 직면해 있습니다:

접근성: 새로운 프로그램 로직을 개발하는 것은 로직을 사용하는 데 필요한 기술과는 구별되는 전문적인 기술을 요구하며, 이는 새로운 로직의 생성을 어렵게 만듭니다.
재사용성 및 합성성: 기존 로직의 구성 요소를 재사용하거나 서로 다른 효과(예: 동시성과 크래시 복구의 결합)에 대한 지원을 결합하는 것이 어렵습니다.
운영 의미론 (Operational Semantics): 최근의 대안적 접근 방식(예: ITrees 사용)은 재사용성은 해결하지만, 실질적인 기계에서 실행 가능한지에 대한 의문을 제기하는, 즉 운영적 이해를 즉각적으로 제공하지 못하는 데노테이셔널 의미론(denotational semantics)에 의존합니다.

이펙트 핸들러를 위한 기존 로직들은 기본 언어가 이미 내장된 원시 이펙트(예: 가변 상태 또는 동시성)를 가지고 있다고 가정하는 경우가 많습니다. 이는 핸들러 로직을 효과를 부트스트래핑하는 주요 메커니즘으로 다루기보다, 원시 이펙트의 복잡성을 핸들러 로직과 혼합함으로써 사상 증명(soundness proofs)을 복잡하게 만듭니다.

방법론 (Methodology)

저자들은 모든 프로그램 효과를 모델링하기 위해 이펙트 핸들러를 사용하는 방식, 즉 최소한의 상태가 없는 코어 언어인 FicusLang으로부터 시작하여 운영적으로 구축 가능한 확장형 프로그램 로직을 제안합니다.

핵심 구성 요소

FicusLang: 이펙트 핸들러를 포함하는 최소한의 ML 스타일 람다 계산법입니다. 여기에는 두 가지 원시 이펙트인 pick(비결정론적 불리언)과 observe(고스트 코드를 위한 레이블된 전이)가 포함됩니다. 저자들은 이러한 원시 기능조차 결국 핸들러를 통해 인코딩될 수 있음을 언급합니다.
Ficus (단항 로직 - Unary Logic): Iris 프레임워크 위에 구축되고 Hazel 로직을 변형하여 확장 가능한 분리 논리(separation logic)입니다.
- 프로토콜 (Protocols): Ficus는 이펙트 핸들러의 동작을 명시하기 위해 프로토콜( $\Psi$ )을 사용합니다. 최약 전제 조건(weakest precondition) 어설션 ewp e <Ψ> {Φ}는 만약 e가 $\Psi$ 를 만족하는 핸들러 아래에서 실행된다면, 중단되지 않고(not get stuck) 사후 조건 $\Phi$ 를 만족할 것임을 나타냅니다.
- 확장 가능한 월드 (Extensible Worlds): 동시성과 조정(coordination)을 지원하기 위해, Ficus는 "확장 가능한 월드"를 도입합니다. 불변량(invariants)이 고정된 표준 Iris와 달리, Ficus는 ewp와 fancy update modality를 커스텀 가능한 월드( $W$ )에 매개변수화합니다. 이를 통해 핸들러 구현자는 특정 효과를 모델링하는 데 적합한 자신만의 불변량 및 원자성 개념을 정의할 수 있습니다.
- 핸들러 구현: 저자들은 FicusLang 내에서 가변 상태, 공유 메모리 동시성, 분산 실행, 크래시 복구를 위한 핸들러를 구현합니다. Ficus를 사용하여 이러한 핸들러를 검증함으로써, 이러한 기능들을 위한 특화된 로직과 유사한 증명 규칙을 도출합니다.
RelFicus (관계 로직 - Relational Logic): 효과를 사용하는 프로그램 간의 문맥적 정제(contextual refinements)를 증명하기 위한 관계 로직입니다.
- 이는 두 번째 "명세(specification)" 프로그램을 고스트 상태로 인코딩함으로써 관계적 추론을 단항 로직에 임베딩합니다.
- RelFicus는 동일한 확장 가능한 월드와 프로토콜을 활용하여, 효과적인 프로그램의 관계적 속성에 대한 합성적 추론을 가능하게 합니다.

주요 기여 (Key Contributions)

본 논문은 다음과 같은 구체적인 기여를 합니다:

Ficus: 이펙트 핸들러를 기반으로 하는 확장 가능한 단항 프로그램 로직의 개발입니다. 이는 핸들러와 클라이언트 코드 간의 추론을 분해하기 위해 프로토콜을 사용하며, 클라이언트 코드가 리소스를 공유할 수 있도록 확장 가능한 월드를 도입합니다.
RelFicus: 이펙트 핸들러가 존재하는 상황에서 문맥적 정제를 증립하기 위한 관계 로직으로, Ficus 프로토콜을 관계적 설정에 적응시켜 재사용성과 확장성을 가능하게 합니다.
사례 연구 (Case Studies): 저자들은 기존 로직의 기능들을 재구성하고 확장함으로써 이 접근 방식을 입증합니다:
- 예언 변수 (Prophecy Variables): 전역 예언(global prophecies)으로부터 지역 예언을 도출하고, 예언 변수를 힙 위치와 암시적으로 연관시키는 "예언적 힙(prophetic heap)"을 구현하여, 명시적인 클라이언트 도구가 필요 없도록 합니다.
- 크래시 복구 (Crash Recovery): 비동기적 내구 저장소(asynchronous durable storage)를 가진 크래시 복구 로직으로, Perennial 로직의 특징을 유지하면서도 더 단순한 모델과 크래시 인식 예언 변수에 대한 새로운 지원을 제공합니다.
- 분산 시스템 (Distributed Systems): IronFleet 스타일의 원자적 블록을 특징으로 하는 분산 시스템을 위한 로직입니다.
더 강력한 증명 규칙: 핸들러 기반 접근 방식은 다음 두 가지 측면에서 기존 작업보다 더 강력한 추론 규칙을 제공합니다:
1. 계층적 효과 (Hierarchical Effects): 후속 효과가 이전 효과를 사용하여 구축될 수 있으므로(예: 전역 예언으로부터 지역 예언 도출), 증명 규칙을 재사용할 수 있습니다.
2. 비표준 의미론 (Non-Standard Semantics): 핸들러는 추론하기 쉬운 비표준 버전의 효과를 구현할 수 있습니다(예: 표준 선점형 의미론보다 적은 인터리빙을 생성하는 동시성 핸들러). 저자들은 RelFicus를 통해 이들이 표준 의미론과 문맥적으로 동등함을 증명함으로써 이를 정당화합니다.
에르고노믹스 (Ergonomics): Ficus는 서로 다른 프로토콜을 가진 경우에도 명세를 적용할 수 있게 해주는 유연한 택틱스(tactics) 시스템을 포함하여, 표준 Iris 기반 로직과 유사한 증명 경험을 제공합니다.

결과 및 검증 (Results and Validation)

기계화 (Mechanization): 전체 작업은 Iris 분리 논리 프레임워크와 Rocq Prover에서 기계화되었습니다.
적절성 정리 (Adequacy Theorems): 저자들은 Ficus와 RelFicus 모두에 대해 적절성 정리를 증명하여, 논리적 도출이 언어의 운영 의미론과 일치함을 보장합니다.
문맥적 동등성 (Contextual Equivalence): RelFicus를 사용하여, 효과가 발생할 때만 선점을 트리거하는 동시성 핸들러가 임의의 단계에서 선점이 발생할 수 있는 표준 선점형 의미론과 문맥적으로 동등함을 증명합니다. 이는 더 강력한 invariant-opening 규칙을 위해 이들의 "더 약한" 인터리빙 모델을 사용하는 것을 정당화합니다.
암시적 예언 (Implicit Prophecies): "예언적 힙" 사례 연구는 클라이언트 프로그램이 예언 작업을 수동으로 주석 달 필요 없이, 힙 연산이 예언 능력을 자동으로 확장할 수 있음을 보여줍니다.

의의 (Significance)

본 논문은 이 접근 방식이 프로그램 로직의 개발을 더욱 접근 가능하고 모듈식으로 만든다고 주장합니다. 이펙트 핸들러를 로직을 부트스트래핑하는 주요 메커니즘으로 취급함으로써, 개발자는 다음을 수행할 수 있습니다:

로직 합성: 단일한 로직을 처음부터 구축하는 대신, 핸들러를 중첩함으로써 다양한 효과(예: 동시성 + 크래시 복구)에 대한 지원을 조합하고 섞을 수 있습니다.
더 강력한 규칙 도출: RelFical 로직을 통해 표준 의미론과 동등함을 증명할 수 있다는 전제하에, 추론하기 쉬운 핸들러 특유의 비표준 의미론을 활용할 수 있습니다.
운영적 명확성: 프로그램 동작에 대한 운영적 이해를 유지하여, 결과적으로 도출된 로직이 실행 가능한 의미론에 근거하도록 보장합니다.

이 연구는 프로그램 로직을 사용하는 것의 접근성과 이를 개발하는 것의 복잡성 사이의 간극을 메우며, 복잡한 시스템을 위한 새로운 로직을 점진적이고 합성적으로 구축할 수 있는 프레임워크를 제공합니다.