A Lightweight Formalism for Reference Lifetimes and Borrowing in Rust
Abstract
Rust is a relatively new programming language that has gained significant traction since its v1.0 release in 2015. Rust aims to be a systems language that competes with C/C++. A claimed advantage of Rust is a strong focus on memory safety without garbage collection. This is primarily achieved through two concepts, namely, reference lifetimes and borrowing. Both of these are well-known ideas stemming from the literature on region-based memory management and linearity/uniqueness. Rust brings both of these ideas together to form a coherent programming model. Furthermore, Rust has a strong focus on stack-allocated data and, like C/C++ but unlike Java, permits references to local variables.
Type checking in Rust can be viewed as a two-phase process: First, a traditional type checker operates in a flow-insensitive fashion; second, a borrow checker enforces an ownership invariant using a flow-sensitive analysis. In this article, we present a lightweight formalism that captures these two phases using a flow-sensitive type system that enforces “type and borrow safety.” In particular, programs that are type and borrow safe will not attempt to dereference dangling pointers. Our calculus core captures many aspects of Rust, including copy- and move-semantics, mutable borrowing, reborrowing, partial moves, and lifetimes. In particular, it remains sufficiently lightweight to be easily digested and understood and, we argue, still captures the salient aspects of reference lifetimes and borrowing. Furthermore, extensions to the core can easily add more complex features (e.g., control-flow, tuples, method invocation). We provide a soundness proof to verify our key claims of the calculus. We also provide a reference implementation in Java with which we have model checked our calculus using over 500B input programs. We have also fuzz tested the Rust compiler using our calculus against 2B programs and, to date, found one confirmed compiler bug and several other possible issues.
추상
Rust는 2015년 v1.0이 출시된 이후 상당한 관심을 받고 있는 비교적 새로운 프로그래밍 언어입니다. Rust는 C/C++와 경쟁하는 시스템 언어를 목표로 합니다. Rust의 장점은 쓰레기 수거 없이 메모리 안전에 중점을 둔다는 것입니다. 이는 주로 기준 수명과 차입이라는 두 가지 개념을 통해 달성됩니다. 이 두 가지 모두 지역 기반 메모리 관리와 선형성/고유성에 관한 문헌에서 비롯된 잘 알려진 아이디어입니다. Rust는 이 두 가지 아이디어를 모두 결합하여 일관된 프로그래밍 모델을 형성합니다. 또한 Rust는 스택 할당 데이터에 중점을 두고 있으며 C/C++와 마찬가지로 로컬 변수에 대한 참조를 허용합니다.
Rust의 유형 확인은 2단계 프로세스로 볼 수 있습니다: 첫째, 기존 유형 검사기는 흐름에 민감하지 않은 방식으로 작동하고, 둘째, 차입 검사기는 흐름에 민감한 분석을 사용하여 소유권 불변량을 강제합니다. 이 글에서는 "유형 및 차입 안전"을 강제하는 흐름에 민감한 유형 시스템을 사용하여 이 두 단계를 캡처하는 가벼운 형식주의를 제시합니다. 특히 유형 및 차입 안전한 프로그램은 달링 포인터를 참조 해제하려고 시도하지 않습니다. 우리의 미적분 코어는 복사 및 이동 시맨틱, 돌연변이 차입, 재융자, 부분 이동, 수명 등 Rust의 많은 측면을 캡처합니다. 특히, 쉽게 소화하고 이해할 수 있을 만큼 충분히 가볍고 여전히 참조 수명과 차입의 두드러진 측면을 캡처한다고 주장합니다. 또한 코어 확장은 더 복잡한 기능(예: 제어 흐름, 튜플, 방법 호출)을 쉽게 추가할 수 있습니다. 우리는 미적분에 대한 주요 주장을 검증하기 위한 건전성 증명을 제공합니다. 또한 500B 이상의 입력 프로그램을 사용하여 미적분을 모델링한 Java의 참조 구현을 제공합니다. 또한 2B 프로그램에 대해 미적분을 사용하여 Rust 컴파일러를 퍼지 테스트했으며, 현재까지 하나의 확인된 컴파일러 버그와 기타 몇 가지 가능한 문제를 발견했습니다.