A Lightweight Formalism for Reference Lifetimes and Borrowing in Rust
- 31 March 2021
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 43 (1), 1-73
- https://doi.org/10.1145/3443420
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.Keywords
This publication has 90 references indexed in Scilit:
- FeatACM SIGPLAN Notices, 2012
- A time-aware type system for data-race protection and guaranteed initializationACM SIGPLAN Notices, 2010
- Tribal ownershipACM SIGPLAN Notices, 2010
- Verification of Object-Oriented Programs with Invariants.The Journal of Object Technology, 2004
- A region inference algorithmACM Transactions on Programming Languages and Systems, 1998
- Flexible alias protectionLecture Notes in Computer Science, 1998
- Elements of style: analyzing a software design feature with a counterexample detectorIEEE Transactions on Software Engineering, 1996
- Extending typestate checking using conditional liveness analysisIEEE Transactions on Software Engineering, 1993
- Polymorphic type, region and effect inferenceJournal of Functional Programming, 1992
- A theory of type polymorphism in programmingJournal of Computer and System Sciences, 1978