Zeta의 차세대 빌림 검사기 — Rust 메모리 관리 모델을 대체하려는 실험

AI 요약

Zeta의 작성자는 Rust의 소유권과 &·&mut 규칙이 메모리 안전성을 보장하지만, 서로 다른 메모리 영역을 빌리는 코드까지 거부하거나 런타임 검사와 unsafe 우회로를 요구한다고 주장합니다. 글은 이 제약을 줄이는 차세대 빌림 검사기 모델을 제시합니다. 다만 Zeta는 실험 단계이며, 작성자는 실제 프로그램을 구축해 모델을 검증하지 못했다고 밝힙니다.

비중첩 영역 추론

모델의 중심은 비중첩(disjointness) 증명입니다. Rust에서는 Vec의 서로 다른 인덱스를 동시에 가변 빌리려면 get_disjoint_mut 같은 API를 써야 합니다. 글은 이 API가 인덱스 범위와 중복 여부를 검사하고, 이후 unsafe 코드로 접근한다고 설명합니다. Zeta는 get_mut(i)와 get_mut(j)가 접근하는 주소의 관계를 추적해 i != j를 증명하면 두 가변 참조를 허용합니다. 서로 다른 필드, 루프 인덱스, 조건문 검사, 산술 관계도 근거로 듭니다. 증명에 필요한 사실을 찾지 못하면 보수적으로 거부하며, 아직 구현하지 않은 unsafe 컴파일러 단언으로 검사기에 가정을 전달하는 방안도 소개합니다.

이 추론은 함수 구현도 분석합니다. get_mut의 본문을 보고 반환 참조가 인덱스 인자에 어떻게 의존하는지 알아내는 식입니다. 따라서 단순히 함수 시그니처만으로 호출을 검사하지 않습니다. 작성자는 나중에 시그니처에 this.{&mut x, &mut y}처럼 필요한 메모리 영역을 명시하는 방법도 설명합니다. 이 방식은 구현 변경이 호출자의 빌림 가능성에 영향을 주고, 동적 디스패치나 독립적인 컴파일과 충돌할 수 있다는 지적을 받았습니다. 토론에서 작성자는 함수 본문을 분석해 필요한 빌림을 추론하는 기능을 재검토하겠다고 밝혔습니다. 이어 공개 함수에서는 추론을 없애고, 시그니처로 접근 영역을 명시하는 기능은 유지하겠다는 계획을 제시했습니다.

세 번째 참조 종류와 출처

Zeta는 일반 참조 &와 가변 참조 &mut 외에 &alias를 둡니다. &alias는 여러 참조가 같은 값을 공유하면서 변경도 허용하는 별칭 참조입니다. 배타성을 요구하지 않으므로 LLVM의 noalias 최적화 보장은 받지 못하고, 스레드 사이에서 쓰려면 Send와 Sync 조건을 요구한다고 작성자는 설명합니다. 참조 대상의 메모리가 해제되거나 재할당돼 낡은 참조가 생기는 경우는 비중첩 추론과 무효화 검사로 막는다는 주장입니다. 이를 이용해 Rust에서 Rc<RefCell<T>>와 런타임 참조 세기를 쓰는 이중 연결 리스트를 Zeta에서는 소유 포인터 ^와 &alias로 구현합니다. 작성자는 Zeta 쪽은 별도 Drop 구현 없이 노드와 내부 값을 정리하고, RefCell의 런타임 검사도 피한다고 보여줍니다.

수명 대신 provenance, 즉 참조나 소유 포인터가 어떤 메모리 영역에서 왔는지를 추적하는 개념도 소개합니다. 예컨대 list.get_mut(0)이 list 전체가 아니라 list.data에서 비롯했다는 사실을 추론해, 참조가 유효한 범위와 무효화 조건을 연결합니다. 글은 이를 Rust의 명시적 수명 표기보다 구체적인 진단으로 이어질 수 있다고 설명합니다. 또 서로 겹치지 않는 슬라이스 네 개를 스레드에 나눠 병렬 처리하는 예를 제시하고, 범위가 한 칸 겹치도록 바꾸면 컴파일 오류가 난다고 보여줍니다.

안전성과 설계에 관한 쟁점

댓글에서는 함수 본문을 분석하는 방식이 공개 API를 불안정하게 만들고, 컴파일 경계를 넘어서는 호출이나 동적 라이브러리에서 작동하기 어렵다는 우려가 나왔습니다. 작성자도 이 문제를 인정하고 추론을 제한하거나 명시적 시그니처로 대체하는 방안을 검토했습니다. 또 &alias가 UnsafeCell과 어떻게 다른지, 별칭 참조가 가리키는 값의 모양이나 내부 불변식을 어떻게 지키는지 질문이 이어졌습니다. 동시 접근에서 여러 필드를 갱신할 때 관찰자가 중간 상태를 볼 수 있다는 지적도 나왔습니다. 작성자는 이 모델이 Send와 Sync 조건을 요구하고 참조 무효화를 검사한다고 답했지만, 세부 규칙과 형식적인 안전성 증명은 더 설명해야 한다는 의견이 있었습니다. 실제로 작성자는 Rust의 Polonius와 비슷한 사례를 시험하다 잠재적 UB가 가능한 오류를 발견해 수정했다고 밝혔습니다. 토론에는 테스트만으로 안전성 증명이 되지는 않는다는 지적도 포함됐습니다.

Reddit 반응

• @u/adrian17 — get_mut의 시그니처만 보는 게 아니라 구현을 분석해 반환 참조와 인자의 관계를 추론하는 방식인가요? index % 8처럼 복잡한 식도 처리하나요? 그렇다면 어디까지가 한계인가요? 함수 내부를 바꾸면 호출자 코드의 유효성이 달라져 구현이 API 일부가 되는 점도 걱정됩니다.
  • @u/FlameyosFlow — 질문하신 것처럼 복잡한 식도 처리합니다. 다만 SMT 솔버를 쓰는 건 아니며, 조건문이나 안전하지 않은 단언, 분석 가능한 산술식에서 저장한 사실로 추론합니다. 증명할 수 없으면 보수적으로 오류를 냅니다. 동적 디스패치처럼 구현을 볼 수 없는 경우에는 시그니처에 필요한 메모리 영역을 명시해야 합니다.
• @u/loewenheim — 글에서 Rust가 같은 구조체의 서로 다른 필드도 동시에 가변 참조할 수 없다고 한 부분은 맞지 않습니다. 해당 코드로 직접 확인해 보세요.
  • @u/FlameyosFlow — 제가 완전히 놓쳤습니다. Rust가 허용하는 기본적인 필드 간 비중첩 증명과 Zeta가 주장하는 더 복잡한 증명을 구분하도록 문장을 고쳤습니다. 알려주셔서 감사합니다.
  • @u/Lucretiel — 함수의 정확성은 시그니처만 보고 알 수 있어야 한다는 점이 설계 의도입니다. 함수 본문에 제네릭 제약이 좌우되면 C++에서 겪는 문제를 다시 불러올 수 있습니다.
• @u/initial-algebra — 함수 본문에 의존하면 동적 라이브러리나 외부 코드의 콜백 같은 사용 사례에서 작동하지 않습니다.
  • @u/FlameyosFlow — 그런 경우 필요한 필드를 시그니처에 명시하거나 전체 구조체를 빌려야 합니다. 본문에서 &mut this의 범위를 추론하는 기능은 계속 둘지 재검토하겠습니다.
• @u/redlaWw — 이 모델은 컴파일러의 별칭 분석이 참조가 겹치지 않는다고 증명해야 코드가 유효하다는 뜻으로 보입니다. 프로그래머가 분석기의 한계를 알아야 하고, 함수 본문 변경이 API 호환성을 깨뜨릴 수도 있습니다.
  • @u/FlameyosFlow — 우려가 맞습니다. 필요한 빌림을 시그니처에 직접 적는 기능은 이미 가능하며, 본문에서 자동 추론하는 부분은 재검토하겠습니다.
• @u/initial-algebra — &alias의 규칙이 아직 모호합니다. 별칭 참조가 있는 Option<T>를 None으로 바꾸면 내부 값을 가리키는 참조가 낡을 수 있습니다. 여러 필드를 한 번에 쓰는 상황에서는 다른 스레드가 일부만 갱신된 상태를 볼 수도 있습니다.
  • @u/FlameyosFlow — 참조가 가리키는 내부 값이 유효한 동안 이를 무효화하는 변경은 검사기가 거부해야 합니다. 스레드 경계를 넘는 &alias에는 Send와 Sync 조건을 요구합니다. 두 필드 갱신 사례의 안전성은 아직 확인하지 못했으며 살펴보겠습니다.
• @u/WorldsBegin — &alias와 초기화되지 않은 메모리의 규칙에는 더 분명한 설명이 필요합니다. 특히 &mut T 인자가 초기화 여부를 어떻게 전달하는지, 함수 구현을 확인하지 않고 호출이 안전한지 판단할 수 있는지 궁금합니다.
  • @u/FlameyosFlow — 초기화되지 않은 값을 받는 함수는 해당 함수가 모든 경로에서 값을 초기화한다는 사실을 빌림 검사기가 알아내기 때문에 동작합니다. 이를 시그니처로 표현하는 방법은 아직 없습니다. 이 점은 타당한 우려라고 생각합니다.
• @u/insanitybit2 — 함수 본문 분석은 컴파일 시간과 공개 인터페이스가 내부 구현에 의존하는 문제를 일으킬 수 있습니다. 비공개 함수에만 적용하거나 최적화 목적으로만 쓰는 편이 나을 수 있습니다.
  • @u/FlameyosFlow — 공개 인터페이스가 구현 세부 사항에 의존하는 점이 더 큰 우려입니다. 본문에서 빌림을 추론하는 기능을 없애고 시그니처에 필요한 범위를 적도록 할지 재검토하고 있습니다.
• @u/SkiFire13 — 허용되는 예시는 많지만 새 문법이 안전한 이유를 규칙과 증명 관점에서 설명해야 합니다. 테스트는 형식적인 안전성 증명이 아닙니다.
  • @u/FlameyosFlow — 동의합니다. 의도적으로 오류를 만드는 테스트를 하고 있지만, Rust의 안전성에 관한 기계 검증 연구는 몰랐습니다. 알려주셔서 감사합니다.
• @u/Solumin — Polonius와 비교해 봤나요?
  • @u/FlameyosFlow — Polonius는 제어 흐름을 더 잘 분석하는 NLL 개선안이고, Zeta의 비중첩 증명과는 다른 문제를 다룹니다. 비슷한 사례를 시험하다 잘못된 코드를 허용하는 버그를 발견해 수정했습니다.

원문: GitHub Gist / 번역·요약: Trawling