一句话：提出流敏感轻量级类型系统与演算，统一形式化 Rust 的引用生命周期和借用安全。
Rust 通过引用生命周期和借用，在不使用垃圾回收的情况下追求内存安全，但其类型检查可分为流不敏感的类型检查和流敏感的借用检查两个阶段。本文提出一个轻量级形式化，用流敏感类型系统统一刻画这两个阶段，并保证“类型与借用安全”，使程序不会解引用悬垂指针。演算核心涵盖拷贝/移动语义、可变借用、再借用、部分移动和生命周期，同时保持足够简洁；作者给出可靠性证明，并提供 Java 参考实现，对超过 5000 亿个输入程序进行模型检测，还用该演算对 Rust 编译器进行 20 亿个程序的模糊测试，发现一个已确认的编译器错误及若干可能问题。
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.
@article{paperbot1220,
title = {A Lightweight Formalism for Reference Lifetimes and Borrowing in Rust},
author = {David J. Pearce},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {43},
number = {1},
year = {2021},
doi = {10.1145/3443420}
}