A Synthesis Method of Safe Rust Code Based on Pushdown Colored Petri Nets

1. 연구 배경 및 문제 정의 (Problem)

Safe Rust는 소유권 (ownership), 빌림 (borrowing), 수명 (lifetime) 의 세 가지 핵심 규칙을 통해 컴파일 시점에 메모리 안전성을 보장합니다. 그러나 이러한 엄격한 규칙은 자동화된 코드 생성 (Synthesis) 에 있어 큰 장벽이 됩니다.

• 주요 문제: 자동 생성된 코드 후보가 타입 시스템상으로는 유효해 보일지라도, 소유권 이동 후 사용, 빌림의 중첩 충돌, 또는 수명 영역 (lifetime region) 의 위배 등으로 인해 컴파일러에 의해 거부될 수 있습니다.
• 기존 접근법의 한계: 기존의 Place/Transition Petri Net 은 토큰을 식별 불가능한 단위로 취급하여, Rust 의 제네릭 타입, 유동적인 빌림 권한 (read-only vs mutable), 그리고 계층적인 수명 관계 (outlives) 를 모델링하기에 부족합니다.
• 목표: 컴파일러가 검증하는 소유권, 빌림, 수명 제약 조건을 직접 모델링하여, 컴파일 가능한 안전한 Rust 코드 시퀀스를 자동으로 생성하는 방법론을 제시하는 것입니다.

2. 제안된 방법론 (Methodology)

저자들은 **Pushdown Colored Petri Net (PCPN, 푸시다운 컬러 페트리 넷)**을 기반으로 한 새로운 합성 방법을 제안했습니다. 이 방법은 컴파일러가 추출한 시그니처 환경 ($\Sigma(C)$) 을 기반으로 페트리 넷을 구성하고, 이를 통해 유효한 API 호출 시퀀스를 탐색합니다.

2.1 PCPN 구조 및 핵심 요소

• 플레이스 (Places): 구체적인 타입 (Ground Types) 과 권한 능력 (Capabilities: 소유권, 잠김, 블록됨) 으로 인덱싱됩니다. 이는 토큰의 상태를 구조적으로 제어합니다.
• 토큰 컬러 (Token Colors): 값 식별자, 타입 인스턴스, 수명 변수 할당을 포함합니다. 토큰 내부에 동적 리소스 상태와 유효한 빌림 영역 (Scope) 을 인코딩합니다.
• 푸시다운 스택 (Pushdown Stack): 빌림 (Borrow) 의 중첩 구조를 관리합니다. 빌림 생성 시 스택에 푸시 (Push), 빌림 종료 시 팝 (Pop) 하여 LIFO(후입선출) 순서를 강제함으로써 수명 영역의 중첩 규칙을 준수합니다.
• 전이 (Transitions):
  1. API 호출 전이: 추출된 함수/메서드 시그니처에서 유래.
  2. 구조적 전이: 소유권 이동, 복사 (Copy/Clone), 빌림 생성/해제, 필드 접근, 재빌림 (Reborrow) 등을 모델링하는 고정된 규칙 집합.
• 가드 (Guard) 및 활성화 조건: 전이가 활성화되려면 입력 토큰의 타입이 시그니처와 일치해야 하며 (Unification), 트레이트 바운드 (Trait bounds), 연관 타입 (Associated types), 수명 관계 (Outlives) 등 모든 인터페이스 의무가 환경 $\Sigma(C)$에서 충족되어야 합니다.

2.2 이론적 기반: 동형성 (Bisimulation)

• 저자들은 Rust 의 시그니처 기반 리소스 의미론 (Symbolic Rust Semantics, SRS) 과 제안된 PCPN 의 실행 의미론 사이에 **강한 동형성 (Strong Bisimulation)**을 증명했습니다.
• 이는 PCPN 에서의 유효한 실행 시퀀스가 정확히 컴파일 가능한 Rust 코드에 대응하며, 반대로 컴파일 가능한 코드는 PCPN 에서 탐색 가능함을 의미합니다.

2.3 합성 알고리즘

1. 경계 설정: 무한한 상태 공간을 제한하기 위해 토큰 수, 스택 깊이, 타입 인스턴스 수에 대한 명시적 경계 (Bounds) 를 설정합니다.
2. 정규화 (Canonicalization): $\beta$-리네이밍 (값 식별자 및 레이블의 재명명) 에 동형인 상태들을 하나의 대표 상태로 묶어 유한한 탐색 공간을 구성합니다.
3. 작업 목록 탐색 (Worklist Exploration): 목표 상태 (예: 특정 타입의 객체 생성) 에 도달하는 경로를 탐색합니다.
4. 스택 정리 (Stack Closure): 탐색이 중첩된 빌림 상태 (스택이 비어있지 않음) 에서 끝날 경우, 유효한 drop 연산을 추가하여 스택을 비우고 문법적으로 올바른 코드를 생성합니다.

3. 주요 기여 (Key Contributions)

1. 시그니처 기반 의미론 정립: 함수 본문을 inspect 하지 않고도 시그니처만으로 소유권 이동, 빌림, 수명 순서를 포착하는 Rust 의 새로운 의미론을 제안했습니다.
2. PCPN 직접 구성: 타입과 권한으로 인덱싱된 플레이스와 전용 빌림 스택을 사용하여 컴파일러 환경 $\Sigma(C)$로부터 PCPN 을 직접 구성하는 방법을 제시했습니다.
3. 통합된 제약 해결 메커니즘: 타입 매칭, 트레이트 바운드 검증, 연관 타입 해결, 수명 관계를 하나의 가드 활성화 (Guarded Enabling) 판정 로직으로 통합했습니다.
4. 정확성 증명: 리소스 의미론과 PCPN 간의 단계 대응 및 강한 동형성을 증명하여, 합성된 코드가 컴파일러 검증과 정확히 일치함을 이론적으로 입증했습니다.
5. 유효한 코드 생성 도구: 명시적 경계 하에서 유한한 도달 가능 그래프를 구성하고, 이를 통해 신뢰할 수 있는 문법적으로 유효한 Rust 스니펫을 추출하는 프로토타입 도구를 개발했습니다.

4. 실험 결과 및 성과 (Results)

• 도구 구현: 제안된 방법론을 기반으로 한 자동 합성 도구 (RustSynth) 를 구현하여 공개했습니다.
• 정확성: 실험 결과, 생성된 모든 코드가 Rust 컴파일러를 통과하여 100% 정확성을 보였습니다.
• 유효성: 소유권 이동, 빌림 충돌 방지, 수명 중첩 규칙 준수 등 Safe Rust 의 핵심 요구사항을 모두 충족하는 코드를 성공적으로 생성했습니다.

5. 의의 및 결론 (Significance)

이 연구는 형식적 모델 (Petri Net) 을 사용하여 프로그래밍 언어의 복잡한 정적 분석 규칙 (Rust 의 Borrow Checker) 을 자동화한 선구적인 사례입니다.

• 이론적 의의: Rust 의 컴파일 시간 검사를 페트리 넷의 도달 가능성 (Reachability) 문제로 매핑하여, 형식적 검증 기법을 코드 생성에 적용할 수 있음을 보였습니다.
• 실용적 의의: 복잡한 API 시그니처를 가진 라이브러리 사용법을 자동 생성하거나, 컴파일러 테스트 (Differential Compiler Testing) 를 위한 테스트 케이스 생성 등에 활용될 수 있습니다.
• 한계 및 향후 과제: 현재는 안전한 (Safe) Rust 에 국한되어 있으며, 복잡한 제네릭 의존성으로 인한 상태 폭발 (State Explosion) 문제가 발생할 수 있습니다. 향후 Unsafe Rust, 비동기 (Async) 기능 확장 및 탐색 최적화 (Heuristics) 가 필요하다고 결론지었습니다.

요약하자면, 이 논문은 Rust 의 까다로운 메모리 안전 규칙을 Pushdown Colored Petri Net이라는 수학적 모델을 통해 정밀하게 제어함으로써, 컴파일 가능한 안전한 Rust 코드를 자동으로 생성할 수 있는 새로운 패러다임을 제시했습니다.