전통적인 Rust 대여 검사기를 폴로니우스 스타일로 재구성하고, 라이브 오리진과 부분집합 그래프, 활성 대여 데이터플로 분석을 통해 동작을 설명하며, 예제를 통해 현재 동작과 한계, 그리고 폴로니우스가 개선하는 지점을 보여준다.
lqd가 polonius의 진척을 멋지게 이끌고 있습니다. 그는 Inside Rust를 위한 업데이트 글을 작성하고 있는데, 요약하면 최신 PR로 기존 Rust 대여 검사기(borrow checker)를 더 폴로니우스다운 스타일로 재구현했다는 점입니다. 우리는 남아 있는 몇 가지 성능 문제를 해소하고, 사용자 입장에서는 사실상 변화가 없는(성능도 포함) 이 재구현으로 기존 대여 검사기를 교체하는 것을 검토하고 있습니다. 이 글은 그 작업을 훑어보며, 새로운 분석이 높은 수준에서 어떻게 동작하는지 설명합니다. 이어지는 글들에서는 이 분석을 더 정밀하게(가능하면 효율성도 유지하면서) 확장하는 방법을 파고들 계획입니다.
Polonius는 오랫동안 진행되어 오다 다시 움직이기 시작한 프로젝트 중 하나입니다. 최종 사용자의 관점에서 핵심 목표는 문제 사례 #3 같은 함수를 허용하는 것입니다. 이는 원래 NLL의 목표였지만 결국 초기 전달물에서는 제외되었죠. 제 관점에서는, Polonius가 내부 참조와 self borrow를 지원할 수 있는 분석으로 가는 디딤돌이라는 점이 가장 흥미롭습니다.
Polonius는 Datalog로 정의된 대여 검사기 규칙의 대안적 정식화로 시작했습니다. 핵심 아이디어는 분석 방식을 전환하는 것입니다. NLL이 'r을 프로그램 지점 집합으로 이루어진 하나의 "수명(lifetime)"으로 생각하는 반면, polonius에서는 'r을 여러 "대여(loan)"의 집합을 담는 "오리진(origin)"으로 부릅니다. 즉, 참조가 사용될 프로그램의 부분들을 추적하는 대신, 그 참조가 어디에서 왔을 수 있는지를 추적합니다. Polonius를 더 깊이 다루는 자료로는 2019년 Rust Belt Rust 발표와 슬라이드를 추천합니다.
분석을 설명하기 위해 다음 예제를 계속 사용하겠습니다. 하나 주목할 점은 예제에서 수명/오리진이 '0, '1처럼 숫자로 쓰인다는 것입니다. 이는 대여 검사를 시작할 때 우리는 아직 수명/오리진을 계산하지 않았기 때문입니다 — 그게 대여 검사의 일입니다! 그래서 먼저 계산 내내 사용할 자리표시자로 합성된 추론 변수(대수학의 변수처럼)를 만듭니다. 모든 계산이 끝나면 거기에 실제 값을 대입할 수 있게 되는데 — polonius의 경우 그 값은 대여들의 집합입니다(각 대여는 대략 프로그램 어딘가에 등장하는 & 표현식 하나입니다).
예제는 다음과 같습니다. 여기에는 x와 y에 대한 두 개의 대여 L0, L1이 있습니다. 또한 네 개의 대입이 있습니다:
let mut x = 22;
let mut y = 44;
let mut p: &'0 u32 = &x; // 대여 L0, `x`를 대여
y += 1; // (A) `y`를 변경 — 괜찮을까?
let mut q: &'1 u32 = &y; // 대여 L1, `y`를 대여
if something() {
p = q; // 이제 `p`는 `y`를 가리킨다
x += 1; // (B) `x`를 변경 — 괜찮을까?
} else {
y += 1; // (C) `y`를 변경 — 괜찮을까?
}
y += 1; // (D) `y`를 변경 — 괜찮을까?
read_value(p); // 여기서 다시 `p`를 사용
오늘날의 Rust에서는 두 개의 에러(C와 D)가 발생합니다. 하지만 MiniRust로 이 예제를 실행해 보면 실제로는 D만 Undefined Behavior를 유발할 수 있다는 것을 알 수 있습니다. C 지점에서는 y를 변경하지만 y를 참조하는 변수는 q뿐이고 다시는 사용되지 않습니다. 현재 대여 검사기는 과도하게 보수적이라 에러를 보고합니다. 반면 Polonius는 그 경우를 올바르게 통과시킵니다.
| 위치 | 기존 대여 검사기 | Polonius | MiniRust |
|---|---|---|---|
| A | ✔️ | ✔️ | OK |
| B | ✔️ | ✔️ | OK |
| C | ❌ | ✔️ | OK |
| D | ❌ | ❌ | true 분기가 선택되면 UB를 유발할 수 있음 |
이 글에서는 기존 대여 검사기를 폴로니우스 스타일로 재정식화하여 설명합니다. 이렇게 하면 다음 글에서 폴로니우스가 어떻게 다른지 더 쉽게 볼 수 있습니다. 이 재정식화 아이디어는 a-mir-formality1에서 대여 검사기를 구현하면서 나왔습니다. 처음에는 동등한지 확신할 수 없었지만, lqd가 rustc 테스트 모음에 대해 실험적으로 검증했고 100% 동일한 동작을 보였습니다(lqd는 crater에 대해서도 테스트할 예정입니다).
대여 검사 분석은 다음 세 가지의 조합으로 구성되며, 차례로 살펴보겠습니다:
flowchart TD ConstructMIR --> LiveVariable ConstructMIR --> OutlivesGraph LiveVariable --> LiveLoanDataflow OutlivesGraph --> LiveLoanDataflow ConstructMIR["MIR 구성"] LiveVariable["라이브 변수 계산"] OutlivesGraph["outlives 그래프 계산"] LiveLoanDataflow["지점별 활성 대여 계산"]
요즘 대여 검사기는 MIR2 위에서 동작합니다. MIR는 Rust를 매우 단순화한 형태로, 각 문장을 기초적인 문장들로 쪼갠 것입니다. 우리의 프로그램은 이미 충분히 단순해서 MIR가 원본과 거의 같아 보이지만, 제어 흐름 그래프로 구조화되어 있다는 점이 다릅니다. MIR는 대략 다음과 같습니다(단순화):
flowchart TD Intro --> BB1 Intro["let mut x: i32\nlet mut y: i32\nlet mut p: &'0 i32\nlet mut q: &'1 i32"] BB1["p = &x;\ny = y + 1;\nq = &y;\nif something goto BB2 else BB3"] BB1 --> BB2 BB1 --> BB3 BB2["p = q;\nx = x + 1;\n"] BB3["y = y + 1;"] BB2 --> BB4; BB3 --> BB4; BB4["y = y + 1;\nread_value(p);\n"]
classDef default text-align:left,fill-opacity:0;
MIR는 모든 변수의 타입으로 시작합니다. if 같은 제어 흐름 구성요소는 기본 블록이라 불리는 그래프 노드로 변환되며, 각 기본 블록은 단순한 직선형 문장만 담습니다.
첫 단계는 각 프로그램 지점에서의 "라이브 오리진" 집합을 계산하는 것입니다. 이것은 NLL RFC에서 설명된 내용과 정확히 동일합니다. 이는 전형적인 컴파일러 강의에서 배우는 고전적 라이브니스 계산과 매우 비슷하지만, 한 가지 중요한 차이가 있습니다. 우리는 라이브 "변수"가 아니라 라이브 "오리진"을 계산합니다 — 대략적으로 말해 라이브 오리진은 라이브 변수들의 타입에 등장하는 오리진들의 집합과 같습니다:
LiveOrigins(P) = { O | O는 지점 P에서 라이브한 어떤 변수 V의 타입에 등장 }
실제 계산은 약간 더 미묘합니다. 변수들이 스코프를 벗어날 때, RFC #1327의 규칙을 고려해 해당 변수의 Drop 구현이 접근할 수 있는 오리진이 정확히 무엇인지 판단합니다. 하지만 이 글에서는 그 부분은 건너뛰겠습니다.
예제로 돌아가서, 관심 지점마다 어떤 오리진이 라이브한지를 주석으로 달았습니다:
let mut x = 22;
let mut y = 44;
let mut p: &'0 u32 = &x;
y += 1;
let mut q: &'1 u32 = &y;
// 여기서는 `p`와 `q`가 모두 나중에 사용될 수 있으므로
// 그 타입에 있는 오리진(`'0`과 `'1`)이 라이브하다.
if something() {
// 여기서는 변수 `q`만 라이브하다.
// `p`는 곧 덮어써질 예정이어서 현재 값은 죽었다.
// 결과적으로 라이브 오리진은 `'1` 하나뿐이며,
// 이는 `q`의 타입에 등장한다.
p = q;
x += 1;
} else {
y += 1;
}
// 여기서는 변수 `p`만 라이브하다
// (`q`는 다시 사용되지 않는다),
// 따라서 오리진 `'0`만 라이브하다.
y += 1;
read_value(p);
다음 단계는 MIR 전체에 걸친 타입 검사입니다. MIR는 문장이 크게 설탕 걷힘(desugaring) 되었고 타입 추론도 훨씬 적은, 매우 단순화된 Rust라 할 수 있습니다. 하지만 "수명" 추론은 여전히 많습니다 — 기본적으로 NLL이 시작할 때는 모든 수명이 추론 변수입니다.
예를 들어, 예제의 p = q 대입을 보겠습니다:
...
let mut p: &'0 u32 = &x;
y += 1;
let mut q: &'1 u32 = &y;
if something() {
p = q; // <-- 이 대입
...
} else {
...
}
...
이를 타입 검사하려면 q의 타입(&'1 u32)이 p의 타입(&'0 u32)의 부분형식(subtype)이어야 합니다:
&'1 u32 <: &'0 u32
NLL RFC에서 설명했듯, 이 부분형식 관계는 '1: '0일 때 성립합니다. NLL에서는 이를 outlives 관계라고 불렀습니다. 하지만 polonius에서는 '0과 '1이 "대여들의 집합"을 나타내는 오리진이므로 이를 "부분집합 관계"라고 부릅니다. 즉 '1: '0은 '1 ⊆ '0으로 쓸 수 있고, '1이 참조할 수 있는 대여는 '0도 참조할 수 있음을 뜻합니다. 최종적으로 '0과 '1에 어떤 값이 대입되든 이 제약을 만족해야 합니다.
이러한 부분집합 관계는 그래프로 볼 수 있습니다. '1: '0은 '1 --⊆--> '0이라는 간선이 존재함을 의미합니다. 현재의 대여 검사기에서 이 그래프는 "흐름 비민감적"이며, 함수 전체에 대해 하나의 그래프만 있습니다. 결과적으로 다음과 같은 그래프를 얻게 됩니다:
flowchart LR L0 --"⊆"--> Tick0 L1 --"⊆"--> Tick1 Tick1 --"⊆"--> Tick0
L0["{L0}"] L1["{L1}"] Tick0["'0"] Tick1["'1"]
classDef default text-align:left,fill:#ffffff;
보시다시피 p에 등장하는 오리진 '0은 대여 L0와 L1에서 모두 도달 가능합니다. 즉, '0은 x나 y 어느 쪽을 참조할 수도 있다는 뜻입니다. 반면 q에 해당하는 '1은 L1에서만 도달 가능하므로 y만 참조할 수 있습니다.
대여 검사를 완성하려면 한 가지가 더 필요합니다. 바로 "활성 대여(active loans)"를 계산하는 것입니다. 활성 대여는 어떤 에러를 보고할지 결정합니다. 아이디어는, 어떤 장소(place) a.b.c의 활성 대여가 있다면, 그 a.b.c에 접근하는 것이 대여의 종류/접근의 종류에 따라 에러가 될 수 있다는 것입니다.
활성 대여는 라이브니스 분석과 부분집합 그래프 위에 구축됩니다. 기본 아이디어는 다음과 같습니다. 대여 L이 어떤 지점 P에서 활성이라는 것은, L을 만든 대여 표현식에서 P까지의 경로가 존재하고, 그 경로의 각 지점마다…
대여를 참조할 수 있는 라이브 변수가 있다
O가 있고 L ∈ O이다. 여기서 L ∈ O는 대여 L에서 오리진 O로 가는 경로가 부분집합 그래프에 존재함을 의미한다.대여했던 장소 표현식(여기서는 x)이 다시 대입되어 덮어써지지 않았다
&mut *tmp처럼 포인터의 지시 대상을 대여할 수 있다는 점을 의미합니다. 이후 tmp를 다른 곳을 가리키도록 바꾸면, 이전의 *tmp 대여는 더 이상 관련이 없습니다. 현재 *tmp가 가리키는 데이터와 예전 대여가 가리키는 데이터가 달라졌기 때문입니다.컴파일러에서는 위 개념을 데이터플로 분석으로 구현합니다. 임의의 지점에서의 값은 활성 대여들의 집합입니다. 대여가 발급되는 지점에서 그 대여를 생성(gen)하고, 지점 P에서 다음 중 하나라도 참이면 그 대여를 소멸(kill)합니다: (1) 라이브한 어떤 변수의 오리진에도 그 대여가 속하지 않는다; (2) 그 대여가 빌린 경로가 덮어써졌다.
예제를 따라가 봅시다. 먼저 첫 번째 기본 블록을 보겠습니다:
flowchart TD Start["..."] BB1["// 활성 대여: {} p = &x; // 생성(Gen): L0 -- 대여 발급 // 활성 대여: {L0} y = y + 1; q = &y; // 생성 Gen L1 -- 대여 발급 // 활성 대여 {L0, L1} if something goto BB2 else BB3 "] BB2["..."] BB3["..."] BB4["..."]
Start --> BB1 BB1 --> BB2 BB1 --> BB3 BB2 --> BB4 BB3 --> BB4
classDef default text-align:left,fill:#ffffff; classDef highlight text-align:left,fill:yellow; class BB1 highlight
이 블록은 함수의 시작이므로 활성 대여 집합은 빈 집합에서 시작합니다. 이어서 &x 형태의 문장을 두 번 만나는데, 각 문장은 각각 하나의 대여(L0, L1)의 생성 지점입니다. 블록이 끝날 때 활성 대여 집합은 {L0, L1}입니다.
다음 흥미로운 지점은 if의 참 분기입니다:
flowchart TD Start[" ... let mut q: &'1 i32; ... "] BB1["..."] BB2[" // L0 소멸(Kill) -- 어떤 라이브 오리진에도 속하지 않음 // 활성 대여 {L1} p = q; x = x + 1; "] BB3["..."] BB4["..."]
Start --> BB1 BB1 --> BB2 BB1 --> BB3 BB2 --> BB4 BB3 --> BB4
classDef default text-align:left,fill:#ffffff; classDef highlight text-align:left,fill:yellow; class BB2 highlight
여기서 흥미로운 점은, 블록에 들어올 때 L0에 대한 소멸(Kill)이 있다는 것입니다. 이 시점에서 라이브한 참조는 q 하나뿐입니다. p는 곧 덮어써질 예정이죠. q의 타입이 &'1 i32이므로, 블록 진입 시 라이브 오리진은 {'1}입니다. 앞서 본 부분집합 그래프를 보면…
flowchart LR L0 --"⊆"--> Tick0 L1 --"⊆"--> Tick1 Tick1 --"⊆"--> Tick0
L0["{L0}"] L1["{L1}"] Tick0["'0"] Tick1["'1"]
class L1 trace class Tick1 trace
classDef default text-align:left,fill:#ffffff; classDef trace text-align:left,fill:yellow;
…'1의 추이적 선행자를 따라가면 그 안에 {L1}만 포함됨을 볼 수 있습니다(그래프에서 노란색으로 강조). 이는 L0을 포함하는 오리진을 가진 라이브 변수가 없다는 뜻이므로, L0를 소멸합니다.
활성 대여가 L1 하나뿐이고 L1은 y를 대여했으므로, x = x + 1 문장은 허용됩니다. 이는 매우 흥미로운 결과입니다! "활성 대여"라는 아이디어가 대여 검사에 어느 정도 흐름 민감성을 되살려준다는 것을 보여줍니다.
왜 흥미로울까요? 이 시점에서 변수 p는 라이브합니다. 변수 p에는 오리진 '0이 들어 있고, 부분집합 그래프를 보면 '0에는 L0과 L1이 모두 포함됩니다. 따라서 순전히 부분집합 그래프만 보면, x는 L0에 의해 대여 중이므로 x를 수정하는 것은 에러여야 할 것 같습니다. 그런데 실제로는 에러가 아닙니다!
이는 활성 대여 분석 덕분입니다. 이 분석은, 이론상 p가 L0을 참조할 수 있더라도, 바로 이 시점에는 그렇지 않다는 것을 알아낸 것입니다.
반대로 if의 거짓 분기를 보면:
flowchart TD Start[" ... let mut p: &'0 i32; ... "] BB1["..."] BB2["..."] BB3[" // 활성 대여 {L0}, {L1} y = y + 1; "] BB4["..."]
Start --> BB1 BB1 --> BB2 BB1 --> BB3 BB2 --> BB4 BB3 --> BB4
classDef default text-align:left,fill:#ffffff; classDef highlight text-align:left,fill:yellow; class BB3 highlight
이 경로도 흥미롭습니다. 라이브한 변수는 p 하나뿐입니다. 코드를 손으로 추적해 보면, 이 시점의 p는 L0(x)만을 가리킬 수 있습니다. 그럼에도 분석은 활성 대여가 L0과 L1 두 개라고 결론 내립니다. 이는 p가 무엇을 참조할 수 있는지 결정할 때 부분집합 그래프를 보기 때문인데, 이 그래프는 흐름 비민감적입니다. 따라서 프로그램 어딘가에서 p가 L1을 참조할 수도 있고, 아직 L1에 대한 참조가 완전히 사라지지 않았으므로, 여기서도 p가 L1을 참조할 수 있다고 가정합니다. 이로 인해 사용자가 y = y + 1을 할 때 허위 오류가 보고됩니다.
이제 마지막 블록을 봅시다:
flowchart TD Start[" ... let mut p: &'0 i32; ... "] BB1["..."] BB2["..."] BB3["..."] BB4[" // 활성 대여 {L0}, {L1} y = y + 1; read_value(p); "]
Start --> BB1 BB1 --> BB2 BB1 --> BB3 BB2 --> BB4 BB3 --> BB4
classDef default text-align:left,fill:#ffffff; classDef highlight text-align:left,fill:yellow; class BB4 highlight
이 시점에서는 라이브한 변수(p)가 하나이고, 따라서 라이브 오리진도 하나('0)입니다. 부분집합 그래프는 p가 L0과 L1 모두를 참조할 수 있음을 알려주므로, 활성 대여 집합은 {L0, L1}입니다. 이는 올바릅니다. 어떤 경로를 택했는지에 따라 p는 L0 또는 L1을 가리킬 수 있으며, 따라서 사용자가 y를 수정하려 할 때(그리고 이어 p를 사용하려 할 때) 적절히 오류를 보고합니다.
예제에서는 라이브한 참조가 사라졌을 때 대여가 소멸되는 이유 중 하나를 보았습니다. 이는 보통 수명이 짧은 참조를 만들고 더 이상 사용하지 않을 때 발생합니다. 하지만 대입(재할당)으로 인한 소멸도 있습니다. 다음 예를 보세요:
struct List {
data: u32,
next: Option<Box<List>>
}
fn print_all(mut p: &mut List) {
loop {
println!("{}", p.data);
if let Some(n) = &mut p.next {
p = n;
} else {
break;
}
}
}
여기서 대여 검사가 어떻게 동작하는지 자세히 설명하지는 않겠습니다만, 흥미로운 점을 짚어 보겠습니다. 이 루프에서 코드는 먼저 p에서 빌린 다음 그 결과를 p에 다시 대입합니다. 부분집합 그래프만 본다면, 루프의 다음 반복 시점에는 p에 대한 활성 대여가 있을 것입니다. 그런데 이 코드는 컴파일됩니다. 어떻게 가능할까요? 답은 p = n을 할 때 우리가 p를 변경한다는 점에 있습니다. 즉 다음 반복에서 p로부터 다시 빌릴 때, 첫 번째 반복에서 빌렸던 노드가 아닌 "다른 노드"로부터 빌리게 됩니다. 그래서 문제가 없습니다. 대여 검사기가 이를 결론지을 수 있는 이유는 p가 대입되는 것을 보면 p.next의 대여를 소멸시키기 때문입니다. 이 내용은 NLL RFC에서 더 자세히 다룹니다.
1부는 여기까지입니다! 이 글에서는 기존 대여 검사를 더 폴로니우스다운 스타일로 서술할 수 있는 방법을 다뤘습니다. 또한 대여 검사기가 형성된 방식의 흥미로운 특징도 발견했습니다. 분석은 "위치(지점) 비민감" 별칭 분석(부분집합 그래프)을 사용하지만, 여기에 활성 대여를 추적하는 데이터플로 전파를 결합합니다. 이 둘을 함께 쓰면 더 표현력이 좋아집니다. 하지만 이는 NLL의 원래 계획은 아니었습니다. 애초에 부분집합 그래프는 흐름 민감적으로 만들려 했습니다. 부분집합 그래프를 흐름 민감적으로 확장하는 것이 곧 폴로니우스의 핵심입니다. 이를 어떻게 할 수 있을지 생각이 좀 있고, 다음 글들에서 다뤄 보겠습니다. 덧붙여, 이런 정식화를 하다 보니 이런 생각도 듭니다 — 정말 타입 검사와 데이터플로 검사를 결합해야만 할까요? 대여 검사기를(아마도 앞으로 다룰 더 정밀한 변형들도) 더 통합적인 방식으로 정식화할 수 없을까요? 아직은 잘 모르겠습니다!