Rust All Hands 이후로 실험해 온, NLL 제안의 몇 가지 한계를 넘고 잠재적으로 더 빠를 수 있는 ‘별칭 기반’ 빌림 검사기 정식화를 소개합니다. MIR 위에서 Datalog 규칙으로 분석을 정의하고, 영역(region)을 대여(loan)들의 집합으로 보며, 부분집합 전파와 라이브니스 기반 정제, requires/killed/invalidates 관계, 오류 보고까지 다룹니다. 프로토타입은 NLL 테스트를 모두 통과하고 기존 NLL이 다루지 못한 사례도 처리하지만, 성능 최적화 여지는 큽니다.
Rust All Hands 이후로 나는 Rust 빌림 검사기에 대한 또 다른 정식화를 실험해 왔다. 목표는 현재 제안의 몇 가지 단점을 극복하면서도 계산이 더 빨라질 수 있는 정식화를 찾는 것이다. 나는 이 분석의 프로토타입을 구현했다. 이 프로토타입은 전체 NLL 테스트 모음을 통과하며, #47680 같은 현재 NLL 분석이 다루지 못하는 몇몇 사례도 처리한다. 다만 성능은 아직 갈 길이 멀다(현재 분석보다 느리다). 그렇지만 아직 최적화는 시작도 하지 않았고, 확실히 더 잘할 수 있는 순진하고 비효율적인 부분들이 있음을 알고 있으니, 성능에서도 큰 진전을 낼 수 있으리라 낙관하고 있다.
또한 어제 4월 26일이 빌림 검사의 여섯 번째 “생일”이라는 지적을 들었다 – 그 시절 내 커밋을 보면 그 당시 Rust가 어땠는지 잘 알 수 있어 재미있다.12
첫 번째로 짚고 갈 점은, 이 제안은 Rust 최종 사용자 관점에서는 아무 차이가 없다는 것이다. 즉, 빌림 검사기는 대체로 NLL 제안에서와 동일하게 동작해야 한다.
다만, 이 제안에서는 컴파일러가 프로그램을 바라보는 방식에 미묘한 변화가 있으며, 이는 잠재적으로 미래의 언어 기능에 영향을 줄 수 있다.
분석은 MIR 상에서 동작하지만, 여기서는 단순한 Rust 예시로 설명하겠다. 다음은 첫 번째 예시로, 예시 A라 부르겠다. 보시다시피 이 예시는 컴파일되면 안 된다:
fn main() {
let mut x: i32 = 22;
let mut v: Vec<&i32> = vec![];
let r: &mut Vec<&i32> = &mut v;
let p: &i32 = &x; // 1. 여기서 `p`를 만들기 위해 `x`가 대여(borrow)됨
r.push(p); // 2. `p`가 `r`을 통해 `v`에 저장됨
x += 1; // <-- 오류! 대여 중인 `x`는 변경할 수 없음
take(v); // 3. 나중에 여기서 `x`에 대한 참조가 사용됨
}
fn take<T>(p: T) { .. }
이 새로운 접근에서 가장 큰 변화는 &'a i32 같은 타입을 가질 때 'a의 의미가 바뀐다는 것이다:
'a(수명, lifetime)는 궁극적으로 소스 프로그램의 일부나 제어 흐름 그래프의 일부에 대응했다.'a를 – 여기서는 영역(region)3이라 부르겠다 – 대여(loan)들의 집합에 대응시키고자 한다. 즉, 참조 r의 타입이 &'a i32라면, 'a에 들어 있는 어느 대여의 조건이라도 무효화되면 r도 무효화된다는 뜻이다.대여의 조건을 무효화한다는 것은 그 대여가 빌린 경로(path)에 대해 불법 접근을 수행한다는 뜻이다. 예를 들어 r = &mut v 같은 가변 대여가 있으면, 값 v에는 참조 r을 통해서만 접근할 수 있다. v에 직접 접근하는 것 – 읽기, 쓰기, 이동 – 은 모두 그 대여를 무효화한다. p = &x 같은 공유 대여의 경우 x(또는 p)를 통해 읽는 것은 허용되지만, x를 쓰거나 변경하면 대여의 조건이 무효화된다(그리고 p를 통해 쓰는 것은 애초에 불가능하다).
이제 영역이 프로그램 지점이 아니라 대여들의 집합이 되었으므로, 참조에 대한 서브타이핑 규칙도 조금 달라진다. 지점(point) 기반에서는 수명을 줄여서 참조를 근사할 수 있었지만, 집합 기반에서는 집합을 키워서 근사할 수 있다. 다시 말해:
'a ⊆ 'b
------------------
&'a u32 <: &'b u32
Rust 문법에서 'a ⊆ 'b는 'a: 'b 표기에 대응하고, 나머지 글에서도 이 표기를 쓰겠다. 우리는 전통적으로 이를 _outlives 관계_라 불렀지만, 영역의 새로운 의미에 더 잘 어울리도록 이제는 _부분집합 관계_라 부르겠다4.
영역을 대여들의 집합으로 보는 직관을 더 얻기 위해 다음 프로그램을 보자:
let x = vec![1, 2];
let p: &'a i32 = if random() {
&x[0] // Loan L0
} else {
&x[1] // Loan L1
};
여기서 영역 'a는 집합 {L0, L1}에 대응한다. 왜냐하면 'a는 대여 L0가 만든 데이터에 해당할 수도 있고, 대여 L1의 데이터에 해당할 수도 있기 때문이다.
이 글 전반에서, 나는 Datalog 규칙을 사용해 분석을 정의하겠다. Datalog은 어떤 의미에서 효율적 실행을 위해 설계된 Prolog의 부분집합이다. 대략 Souffle 프로젝트의 문법을 써서 다음과 같은 규칙에 대응한다:
.decl cfg_edge(P:point, Q:point)
.input cfg_edge
.decl reachable(P:point, Q:point)
reachable(P, Q) :- cfg_edge(P, Q).
reachable(P, R) :- reachable(P, Q), cfg_edge(Q, R).
보듯이 Datalog 프로그램은 사물들 간의 관계를 정의한다; 여기서는 .decl로 선언했다5. .input으로 선언된 관계는 입력이며, 그 값은 사용자에 의해 사전에 주어진다(이들을 fact라고도 한다). 위 프로그램에서는 cfg_edge가 그렇다. reachable 같은 다른 관계는 규칙으로 정의되어, 그 사실들(facts)에서 새로운 것들을 합성한다. Prolog와 마찬가지로 대문자 식별자는 변수이며, 동일한 변수가 두 번 나타나면 같은 값을 가져야 한다.
부분집합이기 때문에, Datalog은 Prolog의 보다 ‘프로그래밍 언어’스러운 성질들을 많이 회피한다. 예를 들어, Datalog 프로그램은 유한한 fact 집합에 대해 항상 종료한다(위처럼 재귀가 있어도). 또한 Datalog에서는 부정을 써도 된다. 부정 순환을 허용하지 않기 때문에 – “논리적 not”과 “실패에 의한 부정”의 미묘한 차이를 신경 쓸 필요가 없다6.
이 규칙들을 구현하는 데 나는 Frank McSherry의 훌륭한 differential-dataflow 크레이트를 써 왔다. 꽤 훌륭한 경험이었다: 한 번 손에 익으면 Datalog 규칙을 아주 직선적으로 옮길 수 있고, 덕분에 새로운 설계를 한두 시간 안에 빠르게 프로토타이핑할 수 있었다. 게다가 결과 실행도 꽤 빠르다(물론 최신 설계에서는 아직 성능을 많이 측정하지 않았다).
영역을 대여들의 집합으로 설명했지만, 이제 그 모든 것을 잠시 잊어달라. 내가 정의한 분석은 적어도 처음에는 그 집합들을 직접 다루지 않는다. 대신 프로그램의 모든 영역을 표현하기 위해 “영역 변수”를 사용한다. 나는 이를 '0, '1처럼 “번호가 붙은” 영역으로 표기하겠다.
이제 프로그램을 이 추상 영역들(대체로 MIR에 영역이 있을 법한 모든 곳에 번호 영역을 둔다)을 이용해 다시 쓰면 다음과 같다:
fn main() {
let mut x: i32 = 22;
let mut v: Vec<&'0 i32> = vec![];
let r: &'1 mut Vec<&'2 i32> = &'3 mut v;
let p: &'5 i32 = &'4 x;
r.push(p);
x += 1;
take::<Vec<&'6 i32>>(v);
}
fn take<T>(p: T) { .. }
이 추상 영역들은 Datalog 규칙 전반에 등장하며, 나는 이를 “region”의 약자로 R로 표기하겠다.
앞서 본 추상 영역들은 아직 아무 의미를 갖지 않는다. 다음으로는 표준 방식으로 타입 시스템 규칙을 적용한다. 그 결과 영역들 사이에 우리가 앞서 본 “부분집합” 관계가 생긴다. 예를 들어 예시 A의 다음 줄을 보자:
let p: &'5 i32 = &'4 x;
여기서 식 &'4 x는 &'4 i32 타입의 값을 만들어낸다. 이 타입은 p의 타입인 &'5 i32의 서브타입이어야 하므로 다음을 얻는다:
&'4 i32 <: &'5 i32
이는 곧 '4: '5를 요구한다. 프로그램 전체를 보면 여러 서브타입 관계가 생긴다. 각 관계와 그로부터 나오는 부분집합 관계를 함께 적어보면 다음과 같다.
fn main() {
let mut x: i32 = 22;
let mut v: Vec<&'0 i32> = vec![];
let r: &'1 mut Vec<&'2 i32> = &'3 mut v;
// requires: &'3 mut Vec<&'0 i32> <: &'1 mut Vec<&'2 i32>
// => '3: '1, '0: '2, '2: '0
let p: &'5 i32 = &'4 x;
// requires: &'4 i32 <: &'5 i32
// => '4: '5
r.push(p);
// requires: &'5 i32 <: &'2 i32
// => '5: '2
x += 1;
take::<Vec<&'6 i32>>(v);
// requires: Vec<&'0 i32> <: Vec<&'6 i32>
// => '0: '6
}
fn take<T>(p: T) { .. }
궁극적으로 이러한 부분집합 관계들은 시스템의 입력 fact가 된다. 이후에 분명해지겠지만, 나는 이를 “기본(base) 부분집합” 관계라 부른다:
.decl base_subset(R1:region, R2:region, P:point)
.input base_subset
다시 말해 base_subset(R1, R2, P)는 지점 P에서 R1: R2가 참이어야 함을 뜻한다.
곧 보겠지만 이 base_subset 입력은 시작점에 불과하다 – 이는 어떤 관계들이 처음에 직접 요구되었는지를 알려줄 뿐이며, 어느 지점에서의 관계 전체를 알려주진 않는다. 부분집합 관계는 반복(iteration)하면서 “축적”되므로, 이전 관계와 새로운 관계를 모두 유지해야 하기 때문이다. 우리는 이를 포함하는 보다 완전한 subset 관계를 정의할 텐데, 그 전에 제어 흐름 그래프를 어떻게 정의하는지 먼저 살펴보자.
이 분석에서 쓰는 제어 흐름 그래프는 MIR에 기반해 정의된다. 흐름 그래프의 지점들은 다음과 같이 정의한다:
Point = Start(Statement) | Mid(Statement)
Statement = BBi '/' j
여기서 Statement는 특정 문장을 식별한다(기본 블록 i의 j번째 문장). 그리고 시작 지점(start point) 과 중간 지점(mid point) 을 구분한다. 시작 지점은 기본적으로 “아직 아무 것도 하지 않은” 지점이고, 중간 지점은 문장이 실행되는 위치다. 따라서 앞 절의 기본 부분집합 관계들은 해당 문장의 중간 지점에서 발생한다고 본다.
흐름 그래프의 간선은 다음 cfg_edge 입력으로 정의한다:
.decl cfg_edge(P:point, Q:point)
.input cfg_edge
자연스럽게 모든 시작 지점은 그에 대응하는 중간 지점으로의 간선을 갖는다. 중간 지점은 다음 문장의 시작으로(또는 종료자(terminator)의 경우 뒤따르는 기본 블록들의 시작으로) 간선을 갖는다.
(대부분의 경우 지금은 중간 지점을 무시해도 된다. 하지만 라이브니스를 통합할 때 매우 중요해진다.)
이제 분석에서 가장 흥미로운 부분, 즉 부분집합 관계를 계산하는 부분에 도달했다. 직관을 쌓기 위해 최종 분석보다 단순한 형태를 먼저 제시하고, 그 다음에 좀 더 복잡하게 만들겠다.
핵심 아이디어는 분석이 각 영역 변수의 값을 직접 계산하지 않는다는 것이다. 대신 제어 흐름 그래프의 각 지점에서 영역 변수들 사이에 유지되어야 하는 부분집합 관계를 계산한다. 이 관계들은 타입 검사에서 나온 “기본 부분집합” 관계로 도입되고, 다음 규칙에 따라 제어 흐름 간선으로 전파된다:
'a: 'b라는 기본 부분집합 관계가 도입되면, 그 관계는 계속 참이어야 한다.이를 Datalog으로 다음과 같이 정의할 수 있다. 먼저 subset 관계를 정의한다:
.decl subset(R1:region, R2:region, P:point)
subset(R1, R2, P)가 정의되어 있다면, 지점 P에서 R1: R2가 성립함을 뜻한다. 타입 검사기가 제공한 “기본 부분집합” 관계로부터 시작할 수 있다:
// 규칙 subset1
subset(R1, R2, P) :- base_subset(R1, R2, P).
부분집합은 추이적이므로, 이를 다음처럼 정의할 수 있다:
// 규칙 subset2
subset(R1, R3, P) :- subset(R1, R2, P), subset(R2, R3, P).
마지막으로 부분집합 관계를 제어 흐름 그래프 간선으로 전파하는 규칙을 정의한다7:
// 규칙 subset3 (버전 1)
subset(R1, R2, Q) :- subset(R1, R2, P), cfg_edge(P, Q).
우리 딸이 좋아하는 말로 하자면, 식은 죽 먹기다. 이 규칙들을 예시 A에 적용하면 각 문장 사이에서 다음과 같은 부분집합 관계를 얻게 된다(여기서는 각 “start” 지점에서의 관계만 보여주고, 완전한 추이 폐쇄는 생략한다). 보시다시피 관계는 계속 증가한다:
fn main() {
let mut x: i32 = 22;
// (없음)
let mut v: Vec<&'0 i32> = vec![];
// (없음)
let r: &'1 mut Vec<&'2 i32> = &'3 mut v;
// '3: '1, '0: '2, '2: '0
let p: &'5 i32 = &'4 x;
// '3: '1, '0: '2, '2: '0, '4: '5
r.push(p);
// '3: '1, '0: '2, '2: '0, '4: '5,
// '5: '2,
x += 1;
// '3: '1, '0: '2, '2: '0, '4: '5,
// '5: '2,
take::<Vec<&'6 i32>>(v);
// '3: '1, '0: '2, '2: '0, '4: '5,
// '5: '2, '0: '6
}
fn take<T>(p: T) { .. }
마지막 관계 집합을 보자. 이를 바탕으로 흥미로운 사실을 볼 수 있다. 예를 들어 영역 '4(즉 x를 대여한 곳에서 나온 영역)와 영역 '0(즉 벡터 v 안의 데이터에 대한 영역) 사이의 관계를 볼 수 있다:
'4: '5: '2: '0
이는 기본적으로 프로그램의 데이터 흐름을 반영한다. 각 영역을 “대여들의 집합”으로 생각하면, 이는 '0(즉 벡터)이 그 &x 문장에서 유래한 참조들을 담고 있을 수 있음을 말해준다. 이는 다음 분석 요소로 이어진다.
지금까지는 영역 변수들 사이의 부분집합 관계를 소개하고, 그것을 제어 흐름 그래프에 확장하는 방법을 보았다. 이제는 어떤 영역이 어떤 대여에 의존하는지 추적하기 위해서도 같은 일을 하겠다.
우선 borrow_region이라는 새로운 입력을 도입한다:
.decl borrow_region(R:region, L:loan, P:point)
.input borrow_region
이 입력은 프로그램의 각 대여 식(예: &x, &mut v)에 대해 정의된다. 이는 대여로부터 나온 영역과 생성된 추상 대여를 연결한다. 예시 A에 각 지점에서 생성되는 대여-영역을 주석으로 표시하면 다음과 같다:
fn main() {
let mut x: i32 = 22;
let mut v: Vec<&'0 i32> = vec![];
let r: &'1 mut Vec<&'2 i32> = &'3 mut v;
// borrow_region('3, L0)
let p: &'5 i32 = &'4 x;
// borrow_region('4, L1)
r.push(p);
x += 1;
take::<Vec<&'6 i32>>(v);
}
fn take<T>(p: T) { .. }
base_subset 관계와 마찬가지로, borrow_region은 해당 대여 문장의 중간 지점에서 생성된다.
일반적인 컴파일러 용어로, 제어 흐름 그래프의 어느 지점 P에서 변수 X가 라이브(live) 라는 것은 그 현재 값이 나중에 사용될 수 있음을 의미한다(좀 더 형식적으로는, P에서 Q로 가는 어떤 경로가 있고 Q에서 X를 사용하며, 그 경로에서 X가 다시 할당되지 않는 경우를 말한다).
영역에 대해서도 유사한 정의를 내릴 수 있다: 영역 'a가 지점 P에서 라이브 라는 것은, 타입 &'a i32를 가진 어떤 참조가 나중에 역참조될 수 있음을 의미한다. 대부분의 경우 이는 라이브한 변수 X가 있고 'a가 X의 타입에 등장한다는 뜻이다. 다만 drop에 관해 약간 미묘함이 있다. 파괴자가 어떤 영역을 사용할지, 사용하지 않을지를 이해하려고 똑똑하게 굴기 때문이다(예: Vec<&'a u32> 타입의 값은 drop될 때 'a에 접근하지 않는다는 것을 안다). 그 동작 방식의 자세한 내용은 여기서 다루지 않겠다. NLL RFC와 동일하다.
Datalog 관점에서는 다음처럼 region_live_at 입력을 정의할 수 있다:
.decl region_live_at(R:region, P:point)
.input region_live_at
여기서 초기 값은 NLL RFC와 동일하게 계산된다.
이제 borrow_region 관계를 제어 흐름 그래프 전체로 확장할 수 있다. 앞서처럼 requires라는 새 관계를 도입한다:
.decl requires(R:region, L:loan, P:point)
이는 다음처럼 읽을 수 있다.
영역 R은 지점 P에서 대여 L의 조건을 강제할 것을 요구한다.
다시 말해:
지점 P에서 대여 L의 조건이 위반되면, 영역 R은 무효화된다.
(“requires”라는 이름이 아주 마음에 드는 건 아니지만, 아직 더 나은 이름을 못 찾았다.)
첫 번째 규칙은 어떤 대여의 영역은 항상 그에 대응하는 대여에 의존한다는 것이다:
// 규칙 requires1
requires(R, L, P) :- borrow_region(R, L, P).
다음 규칙은 R1: R2이면 R2는 R1이 의존하는 모든 대여에 의존한다는 뜻이다:
// 규칙 requires2
requires(R2, L, P) :- requires(R1, L, P), subset(R1, R2, P).
마지막으로, 앞서 부분집합과 마찬가지로 이러한 요구를 제어 흐름 간선으로 전파할 수 있다. 하지만 여기에는 한 가지 트위스트가 있다:
// 규칙 requires3 (버전 1)
requires(R, L, Q) :-
requires(R, L, P),
!killed(L, P),
cfg_edge(P, Q).
이 규칙은 영역 R이 지점 P에서 대여 L을 요구한다면, 후속 지점 Q에서도 L을 요구한다는 뜻이다 – 단, L이 P에서 “killed(죽음 처리)”되지 않은 경우에 한해. 그렇다면 이 !killed(L, P)는 무엇인가? killed 입력 관계는 다음처럼 정의된다:
.decl killed(L:loan, P:point)
.input killed
killed(L, P)는 지점 P가, 대여 L이 빌린 피대상(referent) 참조들 중 하나를 덮어쓰는 할당일 때 정의된다. 다음을 생각해 보자:
let p = 22;
let q = 44;
let x: &mut i32 = &mut p; // `x`는 `p`를 가리킴
let y = &mut *x; // 대여 L0, `y`도 `p`를 가리킴
// ...
x = &mut q; // 이제 `x`는 `q`를 가리킴; L0이 kill됨
여기서 x는 처음에 p를 가리키고, 그 값이 y로 복사된다. 이 시점(...이 있는 곳)에서는 *x에 접근하는 것이 불법인데, y가 그것을 빌렸기 때문이다. 하지만 이어서 x를 다시 q를 가리키도록 재할당하면 – 이제 *x에 접근해도 *y와 별개가 된다. 이는 대여 L0을 kill 함으로써 반영되며, 그 결과 *x에 접근해도 이제 y는 무효화되지 않는다.
이제 예시 A에서 각 지점에 subset 관계와 requires 관계를 함께 주석으로 표시할 수 있다. 앞서와 마찬가지로 전체 추이 폐쇄가 아니라 “기본 fact”만을 보여준다. 프로그램을 진행하면서 이들이 계속 축적되는 것을 볼 수 있다:
fn main() {
let mut x: i32 = 22;
// (없음)
let mut v: Vec<&'0 i32> = vec![];
// (없음)
// 대여 L0
let r: &'1 mut Vec<&'2 i32> = &'3 mut v;
// '3: '1, '0: '2, '2: '0
// requires('3, L0)
// 대여 L1
let p: &'5 i32 = &'4 x;
// '3: '1, '0: '2, '2: '0, '4: '5
// requires('3, L0)
// requires('4, L1)
r.push(p);
// '3: '1, '0: '2, '2: '0, '4: '5,
// '5: '2,
// requires('3, L0)
// requires('4, L1)
x += 1;
// '3: '1, '0: '2, '2: '0, '4: '5,
// '5: '2,
// requires('3, L0)
// requires('4, L1)
take::<Vec<&'6 i32>>(v);
// '3: '1, '0: '2, '2: '0, '4: '5,
// '5: '2, '0: '6
// requires('3, L0)
// requires('4, L1)
}
fn take<T>(p: T) { .. }
특히 x += 1 문장 진입 시점의 fact 집합을 보자:
// '3: '1, '0: '2, '2: '0, '4: '5,
// '5: '2,
// requires('3, L0)
// requires('4, L1)
대여 L1은 x에 대한 공유 대여이고, '4는 L1을 요구한다. 게다가 변수 v는 타입 &'0 i32의 참조를 담고 있으며, '4가 '0의 부분집합임을 볼 수 있다:
'4: '5: '2: '0
이는 x를 변경하면(그렇게 하면 L1의 조건이 무효화된다) 벡터 v 안의 참조들이 무효화됨을 의미한다. 그리고 v는 다음 줄에서 사용될 것이므로, 문제가 된다 – 이것이 마지막 규칙, 오류의 정의로 이어진다.
이제 마침내 빌림 검사 오류가 무엇인지 정의할 수 있다. invalidates(P, L)이라는 입력을 정의하는데, 이는 지점 P에서 어떤 접근이나 동작이 대여 L의 조건을 무효화함을 의미한다:
.decl invalidates(P:point, L:loan)
.input invalidates
다음으로, 라이브니스 개념을 영역에서 대여로 확장한다. 대여 L이 지점 P에서 라이브하다는 것은 어떤 라이브한 영역 R이 그것을 요구함을 의미한다:
.decl loan_live_at(R:region, P:point)
// 규칙 loan_live_at1
loan_live_at(L, P) :-
region_live_at(R, P),
requires(R, L, P).
마지막으로, 지점 P가 라이브한 대여 L을 무효화하면 오류다:
.decl error(P:point)
// 규칙 error1
error(P) :-
invalidates(P, L),
loan_live_at(L, P).
지금까지가 내가 구현한 분석과 거의 동일하지만, 한 가지 점이 다르다. 라이브니스를 고려해 제약 전파를 약간 정제할 수 있으며, 이를 통해 훨씬 더 많은 프로그램을 수용할 수 있다. 다음 예시를 보자. 각 지점에서 도입되는 핵심 fact를 주석으로 표시했다(이 fact들은 제어 흐름을 따라 앞으로 전파된다는 점을 기억하자):
let x = 22;
let y = 44;
let mut p: &'0 i32 = &'1 x; // 대여 L0
// '1: '0
// requires('1, L0)
p = &'3 y; // 대여 L1
// '3: '0
// requires('3, L1)
x += 1;
// invalidates(L0)
print(*p);
이 프로그램을 수용할 수 있으면 좋겠다: p가 처음에는 x를 가리키지만, 나중에 y를 가리키도록 다시 할당되므로, x += 1을 실행할 때쯤이면 그 대여는 해제되었어야 한다. 하지만 지금까지 제시한 규칙대로라면 이를 거부한다. 우리는 정보를 꾸준히 축적하고 있기 때문에, x += 1 시점에서는 requires('0, L0)를 아주 쉽게 도출해 버리기 때문이다.
문제는 기존 변수 p를 새로 선언하지 않고 재할당 했기 때문이다. 같은 영역 '0을 재사용한다. 그러니 프로그램을 다음처럼 바꾸면 해결할 수는 있다:
let x = 22;
let y = 44;
let p: &'0 i32 = &'1 x;
let q: &'4 i32 = &'3 y;
x += 1;
print(*q);
하지만 그다지 만족스러운 답은 아니다. 또 다른 가능성으로는 SSA 형식을 사용하는 것이다. 이는 위의 변환을 자동화해 준다. 그 방법도 여전히 선택지이지만, 내가 선택한 길은 아니다 – 다른 이유도 있지만, MIR에서 변수는 “place”이고 SSA를 쓰면 그 점이 좀 복잡해진다(즉, 변수들은 간접적으로 빌릴 수도, 할당될 수도 있다).
내가 대신 한 일은 지점 사이에서 부분집합과 requires 관계를 전파하는 규칙을 수정한 것이다. 이전에는 그 규칙들이 무차별적으로 전파되도록 정의했다. 이제는 후속 지점에서 라이브한 영역에 대해서만 관계를 전파하도록 수정한다:
// 규칙 subset3 (버전 2)
subset(R1, R2, Q) :-
subset(R1, R2, P),
cfg_edge(P, Q),
region_live_at(R1, Q), // 추가
region_live_at(R2, Q); // 추가
// 규칙 requires3 (버전 2)
requires(R, L, Q) :-
requires(R, L, P),
!killed(L, P),
cfg_edge(P, Q),
region_live_at(R, Q). // 추가
이 규칙들을 사용하면 원래 프로그램이 허용된다. 핵심은 p = &y 줄에 진입할 때 변수 p가 죽었다는 점(그 값이 곧 덮어쓰기 때문)이고, 따라서 그 영역 '0도 죽었다는 것이다. 그러므로 그에 영향을 주는 requires(및 subset) 제약은 앞으로 전파되지 않는다.
이 개선은 현재 NLL 분석이 거부하는 #47680의 예시를 수용하는 데에도 결정적이다:
struct Thing;
impl Thing {
fn maybe_next(&mut self) -> Option<&mut Self> {
..
}
}
fn main() {
let mut temp = &mut Thing;
loop {
match temp.maybe_next() {
Some(v) => { temp = v; }
None => { }
}
}
}
여기서 문제는 temp.maybe_next()가 *temp를 대여한다는 점이다. 이 대여는 – 때때로 – 변수 v를 통해 반환되고, 이어서 다시 temp에 저장된다(temp의 값을 치환한다). 즉, 이를 추적해 보면, 그 대여는 루프 전체에서 라이브하다. temp를 재할당하므로 대여가 “kill”될 것이라고 생각할 수도 있다(실제로 그래야 한다). 하지만 기존 규칙에서는 None이 반환될 때 temp가 재할당되지 않기 때문에 kill되지 않았다. 기본적으로 분석이 루프에서 꼬여 버린 것이다.
하지만 새로운 규칙에서는 Some 경로에서 대여가 kill되는 것을 볼 수 있다. temp가 재할당되기 때문이다. 한편 None 경로에서는 그 시점에 죽은 영역에만 관련된 requires 관계가 떨어져 나간다. 그래서 프로그램이 허용된다.
물론 실제 컴파일러에서는 오류가 있는지 여부만으로는 충분치 않다. 사용자에게 오류를 보기 좋게 보고해야 한다. NLL RFC는 내가 three-point form(3점 형식)이라고 부른 오류 보고 기법을 제안했다:
가능하면 모든 오류를 세 지점으로 설명하려 한다:
- 대여가 발생한 지점(B).
- 그로부터 생긴 참조가 사용된 지점(U).
- 그 사이에서 참조를 무효화했을지도 모를 지점(A).
흥미롭게도, 분석을 일련의 Datalog 규칙으로 구성하면, 각 오류를 어떻게 도출했는지를 살펴봄으로써 이 세 지점을 추출할 수 있다. 즉, 예시 A에서 x += 1이 불법인 오류를 생각해 보자. 그 증가가 지점 P에서 발생했다면, error(P)를 질의하여 오류를 찾았을 것이다. “목표에서 시작하는” 하향식으로 실행하는 Prolog를 쓴다면, 다음과 같은 증명 트리를 마주칠 수 있다:
error(P) :-
invalidates(P, L1), // 입력 fact
loan_live_at(L1, P) :- // 규칙 loan_live_at1
region_live_at('0, P), // 입력 fact
requires('0, L1, P) :- // 규칙 requires2
requires('4, L1, P) :- // 규칙 requires3
...
subset('4, '0, P) :- // 규칙 subset3
...
이 트리를 훑어보면 알아야 할 모든 것이 들어 있다. 지점 P에서 오류가 나는 이유는 (a) P가 L1을 무효화하고 (b) L1이 라이브하기 때문이다. L1이 라이브한 이유는 '0이 라이브하고 '0이 L1을 요구하기 때문이다. '0이 L1을 요구하는 이유는 '4 때문이고… 계속된다. 무엇을 뽑아 보여줄지 약간의 휴리스틱만 정하면 된다.
전통적으로 Datalog은 상향식으로 실행한다 – 즉, 모든 기본 fact를 계산하고, 그로부터 도출되는 fact를 계산하고, 계속해서 진행한다. 이는 더 효율적일 수 있지만, 결국 필요하지 않은 fact들을 잔뜩 계산하는 낭비를 낳을 수 있다. 상향식과 하향식 전파를 결합하는 기법들(예: magic sets)이 있으며, Datalog에서 “설명(explanations)”을 얻는 기법 – 즉, 주어진 튜플(예: error(P))을 도출하는 데 필요한 최소 fact 집합을 얻는 기법 – 도 있다. 그런 기법 중 하나는 구현되었고 differential-dataflow로 정의되기도 했다. 멋지다.
나는 아직 이 방향으로 많은 일을 하지는 않았다 – 여전히 우리가 원하는 분석이 맞는지 확인 중이다 – 하지만 이 길을 따른다면 좋은 오류 정보를 끌어낼 수 있을 것이 분명해 보인다.
논의를 위해 Rust internals 게시판에 스레드를 열어두었다.
이 아이디어에 영향을 준 몇몇 사람들과 프로젝트에 감사를 전하고 싶다. 먼저 Frank McSherry의 훌륭한 differential-dataflow 크레이트 덕분에 훨씬 더 빠르게 반복(iterate)할 수 있었다. 정말 훌륭한 물건이다.
둘째, 나는 한동안 컴파일러의 타입 시스템이 전통적인 별칭 분석(alias analysis)과 꽤 다르게 동작하는 이유를 궁금해했다. 얼마 전 Lionel Parreaux와, 영역을 프로그램 경로의 정규식으로 보는 Rust 빌림 검사에 대한 흥미로운 대안 접근법에 관해 아주 흥미로운 대화를 나눴다. 그 뒤 Rust All Hands에서 Vytautas Astrauskas, Federico Poli와 Rust를 Viper 정적 검증기와 통합하려는 그들의 노력을 이야기했는데, 그 과정에서 여기서 말한 부분집합 관계와 매우 비슷한 별칭 관계를 재구성해야 했다고 한다. 이런 작업들을 곱씹으며, 나는 대규모 C 프로그램에 대한 최신 별칭 분석 논문들을 다시 읽었다. 이것이 많은 실험과 반복과 결합되어 여기까지 오게 만들었다. 모두 고맙다!
우리는 아직 match 팔에 =>를 쓰지 않고 여전히 alt와 ret 키워드를 쓰고 있었다! 멋지다. 그리고 여전히 내게는 좀 난해하다.↩︎
그리고 매크로는 foo!(..)가 아니라 #foo[..] 같은 모양이었다. pcwalton이 코드에 “짓눌린 거미”들이 널려 있다고 투덜대던 게 기억난다.↩︎
영역(region)은 학계에서 표준 용어라 기본적으로 따르지만, 여기서 원하는 “직관”을 꼭 담지는 못할 수도 있다. 더 나은 용어를 찾아봐야 할지도.↩︎
흥미롭게도 이는 &'a u32 타입이 'a에 대해 공변(covariant) 임을 의미하는데, 이전에는 반공변(contravariant) 으로 정의하는 것이 자연스러웠다 – 즉, 서브타입 이 더 작은 집합 에 대응한다(하지만 더 긴 수명 에 대응한다). Rust 사용자에게 중요한 일은 아니지만, 타입 시스템을 파고드는 이들에게는 멋진 성질이다.↩︎
이 .foo 지시문들은 내가 알기로 souffle 고유의 것이다.↩︎
우리는 이 규칙들에서 부정을 쓰지만, 특히 사소한 방식 – 부정된 입력 – 에 한정한다.↩︎
이 부분집합 전파 규칙은 나중에 정제할 규칙이다.↩︎