이 글에서는 이전 글에서의 Polonius-유사 정식화를 흐름 민감하게 확장해, 원래 Polonius의 목표를 가능하게 하면서도 몇 가지 한계를 극복하는 방법을 살펴봅니다. 이 정식은 구현 효율 측면에서도 더 유리해 보이며, 끝부분에서 논하듯 여전히 더 개선의 여지가 있는지도 고민합니다.
이전의 Polonius 글에서, 원래의 빌림 검사기(borrow checker)를 Polonius-유사한 스타일로 정식화했습니다. 이번 글에서는 그 정식을 어떻게 흐름 민감(flow-sensitive)하게 확장할 수 있는지 탐구합니다. 그렇게 함으로써 원래 Polonius의 목표를 구현할 수 있을 뿐 아니라, 몇 가지 한계도 넘어설 수 있습니다. 또한 이 정식은 효율적인 구현에도 더 친화적이라고 믿습니다. 다만 글의 마지막에서 다루듯, 여전히 개선의 여지가 남아 있지 않은지 생각하게 됩니다.
원래 글과 같은 Rust 예제를 사용할 것이지만, 특히 false 분기에서의 변경에 초점을 맞추겠습니다1:
let mut x = 22;
let mut y = 44;
let mut p: &'0 u32 = &x;
y += 1;
let mut q: &'1 u32 = &y; // 여기서 `y`를 빌림(L1)
if something() {
p = q; // 빌림을 `p`에 저장
x += 1;
} else {
y += 1; // `false` 분기에서 `y` 변경
}
y += 1;
read_value(p); // `x` 또는 `y`를 가리킬 수 있음
이 줄에서 오류가 발생할 이유는 없습니다. y에 대한 빌림은 존재하지만, false 분기에서는 그 빌림이 q에만 저장되고 q는 다시 읽히지 않습니다. 따라서 정의되지 않은 동작(UB)은 일어날 수 없습니다.
그러나 기존 빌림 검사기는 그렇게 영리하지 못합니다. 마지막의 read_value(p)를 보고, 그 줄이 잠재적으로 x나 y를 읽을 수 있기 때문에, y += 1을 오류로 표시합니다. 이렇게 말하면 이 가엾은 빌림 검사기를 약간 동정할 수도 있겠지요 — 완전히 비합리적인 결론은 아닙니다! 하지만 틀렸습니다.
기존 빌림 검사기의 핵심 문제는 흐름 비민감 부분집합 그래프를 사용한다는 데서 비롯됩니다. 이는 타입 검사를 수행하는 방식과도 연관됩니다. 현재 Polonius에서는 각 변수에 단일 타입과 따라서 단일 오리진(origin)이 있습니다(예: q: &'1 u32). 이 때문에 실행 내내 변수가 가리킬 수 있는 모든 가능한 대여(loan)를 하나로 뭉뚱그리게 됩니다. 하지만 우리가 보았듯 그 정보는 실제로 흐름에 의존합니다.
오늘의 빌림 검사기는 MIR에 적용되는 꽤 표준적인 스타일의 타입 검사기에 기반합니다. 본질적으로 환경(environment) 이 있으며, 각 변수를 타입에 매핑합니다.
Env = { X -> Type }
Type = scalar | & 'Y T | ...
그 다음 이 동일한 환경을 전반에 걸쳐 전달하는 추론 규칙(inference rules)이 있습니다. 개념적으로 규칙의 구조는 다음과 같습니다:
로컬 변수 선언으로부터 Env 구성
Env |- 각 기본 블록이 타입 검사를 통과함
--------------------------
MIR 전체가 타입 검사를 통과함
place를 타입 검사하는 것은 이 Env를 사용하며, 다음과 같은 추론 규칙으로 바닥납니다:
Env[X] = T
-------------
Env |- X : T
빌림 검사기를 _흐름 비민감_하게 만드는 핵심은 모든 지점에서 동일한 환경을 사용하기 때문입니다. 대신 _프로그램 지점_마다 하나의 환경을 갖는다면 어떨까요:
EnvAt = { Point -> Env }
프로그램 지점 A의 문장을 타입 검사할 때는 그 환경으로 EnvAt[A]를 사용합니다. 지점 A에서 지점 B로 흐를 때, A의 환경은 B의 환경의 부분 환경(subenvironment) 이어야 하며, 이를 EnvAt[A] <: EnvAt[B]로 씁니다.
부분 환경 관계 Env1 <: Env2가 성립하려면 다음이 필요합니다.
Env2의 각 변수 X에 대해:
X가 Env1에도 등장하고,Env1[X] <: Env2[X]여야 합니다.여기서 흥미로운 점이 두 가지 있습니다. 첫째, 변수의 집합이 시간에 따라 변할 수 있다는 점입니다. 변수의 수명이 끝나면 환경에서 제거할 수 있다는 뜻입니다. 둘째, 부분형식(subtyping) 규칙에 따라 변수의 타입이 변할 수 있다는 점입니다.
흐름 민감 타입 검사를, 각 프로그램 변수(예: q)마다 프로그램 지점별 복사본이 있는 것으로 생각할 수도 있습니다. 즉 지점 A의 q@A, 지점 B의 q@B처럼요. 한 지점에서 다른 지점으로 흐를 때는 q@A에서 q@B로 대입이 일어납니다. 모든 대입과 마찬가지로, 이는 q@A의 타입이 q@B의 타입의 서브타입이어야 함을 요구합니다.
우리 예제에서 흐름 민감 타입 검사 아이디어가 어떻게 작동하는지 봅시다. 먼저, 이전 글의 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["BB1:\np = &x;\ny = y + 1;\nq = &y;\nif something goto BB2 else BB3"] BB1 --> BB2 BB1 --> BB3 BB2["BB2\np = q;\nx = x + 1;\n"] BB3["BB3\ny = y + 1;"] BB2 --> BB4; BB3 --> BB4; BB4["BB4\ny = y + 1;\nread_value(p);\n"]
classDef default text-align:left,fill-opacity:0;
원래의 흐름 비민감 타입 검사에서 첫 번째로 했던 일은 타입에 등장하는 각 오리진('0, '1)에 대해 오리진 변수를 만드는 것이었습니다. 위의 도표에서 그 변수를 볼 수 있습니다. 따라서 사실상 다음과 같은 환경을 갖고 있었습니다.
Env_flow_insensitive = {
p: &'0 i32,
q: &'1 i32,
}
하지만 이제는 프로그램 지점마다 하나의 환경을 갖게 됩니다. 각 MIR 문 사이에 하나의 프로그램 지점이 있습니다. 따라서 지점 BB1_0은 기본 블록 BB1의 진입점이고, BB1_1은 첫 번째 문 이후입니다. 그러므로 Env_BB1_0, Env_BB1_1 등등이 있으며, 각각에 대해 구분되는 오리진 변수를 만듭니다:
Env_BB1_0 = {
p: &'0_BB1_0 i32,
q: &'1_BB1_0 i32,
}
Env_BB1_1 = {
p: &'0_BB1_1 i32,
q: &'1_BB1_1 i32,
}
...
이제 BB1_3 지점을 봅시다. 이는 BB1의 마지막 줄이며, MIR 용어로는 terminator(종료자) 입니다. 이는 if 종료자입니다(if something goto BB2 else BB3). 이를 타입 검사하기 위해, 진입 환경(Env_BB1_3)을 가져와서, 참 분기 진입(Env_BB2_0)과 거짓 분기 진입(Env1_BB3_0)의 부분 환경이 되도록 요구합니다.
_참 분기_부터 시작해 봅시다. 여기서의 환경 Env_BB2_0은 다음과 같습니다:
Env_BB2_0 = {
q: &'1_BB2_0 i32,
}
여기서 이상한 점이 보일 겁니다 — 왜 p가 없을까요? 그 이유는 변수 p가 BB2 진입 시점에 죽어 있기(dead) 때문입니다. 곧 현재 값이 덮어써질 예정이거든요. 타입 검사기는 죽은 변수를 환경에 포함하지 않는다는 것을 알고 있습니다.
이는 다음을 의미합니다…
Env_BB1_3 <: Env_BB2_0이 성립하려면, BB1_3의 q 타입이 BB2_0의 q 타입의 서브타입이어야 하고…&'1_BB1_3 i32 <: &'1_BB2_0 i32가 성립해야 하며…'1_BB1_3 : '1_BB2_0이 성립해야 합니다.방금 우리는 BB1에서 BB2로의 엣지 때문에, BB1 종료 시점의 '1 버전이 BB2 진입 시점의 '1로 흐른다는 것을 알아냈습니다.
p = q 대입의 타입 검사이제 p = q 대입을 봅시다. 이는 문장 BB2_0에서 발생합니다. 앞서 본 진입 환경은 다음과 같았습니다:
Env_BB2_0 = {
q: &'1_BB2_0 i32,
}
대입에서는 좌변(p)의 타입을 이후 환경에서 가져옵니다. 그곳에 저장하기 때문입니다. 이후 환경은 Env_BB2_1입니다:
Env_BB2_1 = {
p: &'0_BB2_1 i32,
}
따라서 문장을 타입 검사하면 &'1_BB2_0 i32 <: &'0 BB2_1 i32, 즉 '1_BB2_0 : '0_BB2_1을 얻게 됩니다.
이 대입으로부터의 관계 외에도, Env_BB2_0이 이후 환경 Env_BB2_1의 부분 환경이 되도록 만들어야 합니다. 하지만 이 경우 살아있는 변수 집합이 서로소이므로, 그림에 추가되는 것은 없습니다.
마지막 예로, BB1에서 BB3로 가는 거짓 엣지를 봅시다. BB3 진입 시점에는 변수 q는 죽었지만 p는 아니므로, 환경은 이렇게 보입니다:
Env_BB3_0 = {
p: &'0_BB3_0 i32,
}
앞서와 같은 과정을 따르면, '0_BB1_3 : '0_BB3_0이라는 결론에 도달합니다.
이제 흐름 민감 버전의 부분집합 그래프를 어떻게 구축할 수 있는지 보이기 시작합니다. 오리진 변수당 하나의 노드를 갖는 대신, 이제는 프로그램 지점별 오리진 변수당 하나의 노드를 갖고, 타입 검사가 N1 : N2를 요구하면 두 노드 사이에 엣지 N1 -> N2를 생성합니다. 기본적으로 다른 점은 노드가 훨씬 많다는 것입니다.
지금까지 본 것을 종합하면, 이 프로그램에 대해 다음과 같은 부분집합 그래프를 구성할 수 있습니다. 죽은 변수에 해당하는 노드는 제외했습니다 — 예를 들어 '1은 변수 q에 나타나며, q는 프로그램 시작 시 죽어 있으므로 '1_BB1_0 노드는 없습니다.
flowchart TD subgraph "'0" N0_BB1_0["'0_BB1_0"] N0_BB1_1["'0_BB1_1"] N0_BB1_2["'0_BB1_2"] N0_BB1_3["'0_BB1_3"] N0_BB2_1["'0_BB2_1"] N0_BB3_0["'0_BB3_0"] N0_BB4_0["'0_BB4_0"] N0_BB4_1["'0_BB4_1"] end
subgraph "'1"
N1_BB1_2["'1_BB1_2"]
N1_BB1_3["'1_BB1_3"]
N1_BB2_0["'1_BB2_0"]
end
subgraph "Loans"
L0["{L0} (&x)"]
L1["{L1} (&y)"]
end
L0 --> N0_BB1_0
L1 --> N1_BB1_2
N0_BB1_0 --> N0_BB1_1 --> N0_BB1_2 --> N0_BB1_3
N0_BB1_3 --> N0_BB3_0
N0_BB3_0 --> N0_BB4_0 --> N0_BB4_1
N0_BB2_1 --> N0_BB4_0
N1_BB1_2 --> N1_BB1_3
N1_BB1_3 --> N1_BB2_0
N1_BB2_0 --> N0_BB2_1
이전과 마찬가지로, 특정 오리진 O에 대한 노드에서 거슬러 올라가 O에 포함된 모든 대여를 찾을 수 있습니다. 이번에는 오리진 O가 프로그램 지점도 나타냅니다.
특히, '0_BB3_0(if의 false 분기에서 p로부터 도달 가능한 데이터)와 '0_BB4_0(if가 끝난 뒤 도달 가능한 데이터)을 비교해 보세요. 첫 번째 경우 오리진은 L0만 참조할 수 있지만, 그 이후에는 L1도 참조할 수 있음을 볼 수 있습니다.
이전 글에서 설명한 것처럼, 분석을 완성하려면 활성 대여(active loans) 를 계산합니다. 활성 대여의 정의는 거의 동일하지만 한 가지 비틀림이 있습니다. 대여 L이 프로그램 지점 P에서 활성 이려면, L을 만든 빌림에서 P로 가는 경로가 존재하고, 그 경로의 각 지점에 대해…
P에서의 타입이 L을 참조할 수 있는 살아있는 변수가 있어야 하며, 그리고L이 빌린 place 표현식(여기서는 x)이 P에서 재할당되지 않아야 합니다.굵게 표시한 검사를 보셨나요? 이제 변수의 타입이 경로를 따라 변할 수 있다는 사실을 고려합니다. 특히 서로 다른 오리진을 참조할 수 있습니다.
이전 글과 마찬가지로, 데이터플로를 사용해서 활성 대여를 계산할 수 있습니다. 특히, 대여가 발급될 때 그 대여를 gen하고, 점 P에서 대여 L을 kill합니다. 그 조건은 (a) L을 포함하는 오리진을 가진 살아있는 변수가 없거나, (b) L이 빌린 경로가 P에서 할당되는 경우입니다.
실행 예제에 이를 적용하면, if의 false 분기에서 불필요한 오류가 사라집니다. 차근차근 살펴봅시다.
BB1에서, 두 빌림 지점 각각에서 L0와 L1을 gen 합니다. 그 결과, BB1 탈출 시점의 활성 대여는 {L0, L1}이 됩니다:
flowchart TD Start["..."] BB1["BB1: p = &x; // Gen: L0 y = y + 1; q = &y; // Gen: 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 BB3 highlight
if의 false 분기if의 false 분기(BB3)에서는, 나중에 BB4에서 사용될 유일한 살아있는 참조가 p입니다. 특히 q는 죽었습니다.
흐름 비민감 버전에서는, 빌림 검사기가 p의 타입을 볼 때 p: &'0 i32이고, '0의 값이 {L0, L1}이기 때문에 두 대여 모두 활성이라고 결론지었습니다.
하지만 지금 보고 있는 흐름 민감 버전에서는, BB3 진입 시점의 p 타입이 p: &'0_BB3_0 i32입니다. 그리고, 이 글 앞부분에 나온 부분집합 그래프를 보면, '0_BB3_0의 값은 {L0}뿐입니다. 따라서 이 블록 진입 시점에 L1에 대한 kill이 있습니다. 즉 유일한 활성 대여는 x를 빌린 L0이며, 따라서 y = y + 1은 오류가 아닙니다.
flowchart TD
Start["
...
"]
BB1["
BB1:
p = &x; // Gen: L0
...
q = &y; // Gen: L1
...
"]
BB2["
BB2:
...
"]
BB3["
BB3:
// L1 Kill (살아있는 참조 없음)
// 활성 대여: {L0}
y = y + 1;
"]
BB4["
BB4:
...
read_value(p); // 나중에 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 BB3 highlight
앞에서 강조하진 않았지만, 불변성(invariance)은 이 분석에서 정말 흥미로운 역할을 합니다. 또 다른 예를 봅시다. polonius의 vec-push-ref를 단순화한 버전입니다:
let v: Vec<&'v u32>;
let p: &'p mut Vec<&'vp u32>;
let x: u32;
/* P0 */ v = vec![];
/* P1 */ p = &mut v; // 대여 L0
/* P2 */ x += 1; // <-- 여기서는 오류가 없어야 함.
/* P3 */ p.push(&x); // 대여 L1
/* P4 */ x += 1; // <-- 💥 여기서는 오류가 나야 함!
/* P5 */ drop(v);
무엇이 흥미로울까요? P1에서 v를 가리키는 참조 p를 만듭니다. 그런 다음 그 참조 p 안에 x의 빌림을 삽입합니다. 그 시점 이후, 참조 p는 죽지만, 대여 L1은 여전히 활성입니다 — 이는 v에도 저장되어 있기 때문입니다. 이 예제의 핵심은 바로 p와 v의 이 연결입니다.
이 연결이 타입 시스템에서 반영되는 방식은 변성(variance) 을 통해서입니다. 특히 &mut T 타입은 T에 대해 불변(invariant) 입니다. 이는 한 참조를 다른 참조에 대입할 때, 그들이 가리키는 타입이 정확히 동일해야 함을 의미합니다.
부분집합 그래프 측면에서, 불변성은 오리진들 사이에 양방향 엣지를 만들게 됩니다. 무슨 뜻인지 결과 부분집합 그래프를 보며 살펴보죠. 단순하게 하기 위해 p에 대한 노드는 제외하겠습니다. 여기서 흥미로운 오리진은 'v(벡터 v 안의 데이터)와 'vp(참조 p가 가리키는 벡터 안의 데이터 — 역시 v)입니다.
flowchart TD subgraph "Loans" L1["L1 (&x)"] end
subgraph "'v"
V_P0["'v_P0"]
V_P1["'v_P1"]
V_P2["'v_P2"]
V_P3["'v_P3"]
V_P4["'v_P4"]
V_P5["'v_P5"]
end
subgraph "'vp"
VP_P1["'vp_P1"]
VP_P2["'vp_P2"]
VP_P3["'vp_P3"]
end
V_P0 --> V_P1 --> V_P2 --> V_P3 --> V_P4 --> V_P5
V_P1 <--> VP_P1
VP_P1 <--> VP_P2 <--> VP_P3
L1 --> VP_P3
여기서 핵심은 v_P1과 vp_P1 사이, 그리고 vp_P1과 vp_P3 사이의 양방향 화살표입니다. 이것이 어떻게 생겼을까요?
p = &mut v에서 비롯되었습니다. v의 타입(P1에서)은 Vec<&'v_P1 u32>이고, 이는 p의 피참조 타입(Vec<&'vp_P1 u32>)과 정확히 같아야 했습니다. 타입이 같아야 하므로 'v_P1: 'vp_P1이면서 그 역도 성립합니다. 따라서 양방향 화살표가 생깁니다.P1에서 P3로 흐름한 결과입니다. 변수 p는 그 엣지를 가로질러 살아 있으므로, 이전 타입(&'p_P1 mut Vec<&'vp_P1 u32>)이 이후 타입(&'p_P3 mut Vec<&'vp_P3 u32>)의 서브타입이어야 합니다. &mut 참조는 피참조 타입에 대해 불변이므로, 이는 'vp_P1과 'vp_P3가 같아야 함을 의미합니다.모두 합치면, L1은 이전 시점에만 흘러들었음에도 불구하고 'v_P4와 'v_P5에 도달할 수 있음을 봅니다. 멋지죠! 우리는 기대한 오류를 얻게 됩니다.
한편, 불변성으로 인해 일부 부정확함이 도입된 것도 볼 수 있습니다. 대여 L1은 P3에서 도입되지만, 부분집합 그래프만 보면 'vp_P3에서 시간 역방향으로 'vp_P2, 'vp_P1로 흐르고, 'v_P1로 넘어간 뒤 아래로 내려오는 것처럼 보입니다. 오직 부분집합 그래프만 본다면 이 프로그램의 두 x += 1 문 모두가 불법이라고 결론 내렸을 테지만, 실제로는 두 번째 것만 문제가 됩니다.
여기서 보이는 부정확함은 원래 Polonius에서 보았던 부정확함과 매우 유사합니다. 사실상 불변성이 흐름 민감성을 일부 빼앗아 가는 셈이지요. 흥미롭게도, 활성 대여 분석이 이전 글에서와 같은 방식으로 이를 보완해 줍니다. vec-push-ref에서 L1은 P3에서만 생성되므로, 부분집합 그래프를 통해 'v_P2에 도달할 수 있더라도 P2에서는 활성으로 간주되지 않습니다. 하지만 일단 생성되고 나면, p가 죽더라도 'v_P4로 흘러들 수 있으므로 kill되지 않습니다. 따라서 기대한 단 하나의 오류만 얻게 됩니다.
이번 글은 여기서 마무리하겠습니다. 각 프로그램 지점에서 변수에 구분되는 타입을 부여하고, 그 타입들을 서로 관련지어 개선된 부분집합 그래프를 만드는 Polonius의 한 버전을 설명했습니다. 이 그래프는 활성 대여 분석의 정밀도를 높여 불필요한 오류를 줄여 줍니다. 하지만 여전히 몇몇 방식에서는 정밀하지 않습니다.
이 정식이 흥미로운 이유는 몇 가지가 있습니다. 첫째, 가장 비용이 큰 부분은 노드와 엣지가 매우 많은 부분집합 그래프일 것입니다. 하지만 간단한 휴리스틱으로 크게 압축할 수 있습니다. 또한 그 그래프에서 수행하는 핵심 연산은 도달성이며, 이것 역시 매우 효율적으로 구현할 수 있습니다(그래프를 트리로 축소하기 위해 강연결 요소 계산을 한 뒤, 전위/후위 순서를 매겨 인덱스를 비교하면 됩니다). 따라서 실제로 확장 가능하리라 믿습니다.
더 고전적인 예제들을 몇 가지 더 살펴보았고, 나중에 글로 돌아올 수도 있겠지만, 지금까지는 이 분석이 기대한 결과를 내고 있습니다. 하지만 원래 Polonius 및 학계에서 나온 몇 가지 정식들과 더 깊이 비교해 보고 싶습니다. 데이터플로 검사에 기대는 부분이 여전히 어색하게 느껴집니다. 후속 글에서(혹은 독자 여러분과 함께 Zulip 등에서) 그에 대해 더 이야기해 보길 바랍니다!