An alias-based formulation of the borrow checker (2018)

This post from 2018 introduces an experimental, alternative formulation of the Rust borrow checker. The author's goal is to address limitations of the Non-Lexical Lifetimes (NLL) proposal and potentially achieve faster computation. A prototype has been implemented, successfully passing the full NLL test suite and even handling certain complex cases, like issue #47680, that the NLL analysis could not. Although currently slower, the author expresses optimism for significant performance improvements as optimizations are yet to be applied.

• User Impact: The proposed system aims to be transparent to end-users, with the borrow checker functioning largely the same as under NLL, though subtle internal shifts might influence future language features.
• Core Concept - Regions as Loans: The most significant change redefines a region (e.g., 'a in &'a i32). Instead of corresponding to a portion of the source code or control-flow graph, a region now represents a set of loans (borrow expressions). If a reference r has type &'a i32, then invalidating any loan within 'a would invalidate r.
• Subtyping with Loan Sets: Under this new model, subtyping works by enlarging the set of loans. If 'a is a subset of 'b ('a ⊆ 'b), then &'a u32 is a subtype of &'b u32.
• Methodology - Datalog: The analysis is defined using Datalog, a declarative logic programming language, which is well-suited for expressing relations and rules. The prototype implementation leverages Frank McSherry's differential-dataflow crate for efficient execution.
• Abstract Region Variables: Initially, the analysis uses abstract, numbered region variables (e.g., '0, '1) to represent regions throughout the program.
• Relations between Regions: Type system rules establish 'base subset' relationships (e.g., '4: '5) between these abstract regions. These relations signify that one region must 'outlive' or be a 'subset' of another.
• Control-Flow Graph: The analysis operates on the Rust Intermediate Representation (MIR) control-flow graph, defining 'points' as Start(Statement) or Mid(Statement).
• Tracking Subset Relationships: Datalog rules propagate subset relationships transitively and across control-flow graph edges. These relationships accumulate throughout the program, reflecting data flow.
• Borrow Regions: An input borrow_region(R, L, P) relates a region R to an abstract loan L created by a borrow expression at a specific program point P.
• Live Regions and Loans: A region R is region_live_at(R, P) if a reference of that type might be dereferenced later. A loan L is loan_live_at(L, P) if a live region R 'requires' it.
• The 'Requires' Relation: requires(R, L, P) indicates that region R depends on the terms of loan L being enforced at point P. These requirements propagate across control-flow edges unless the loan L is killed (e.g., by reassignment).
• Defining an Error: An error occurs when an action at point P invalidates(P, L) a loan L, and that loan_live_at(L, P) at that point.
• Refined Constraint Propagation: A crucial refinement involves propagating subset and 'requires' relations only for regions that are live at the successor point in the control flow. This allows the analysis to accept more programs by dropping constraints associated with dead regions, as demonstrated by the resolution of issue #47680.
• Error Reporting: The Datalog-based approach offers a promising path for generating detailed error messages in the 'three-point form' (borrow, use, invalidation), which is crucial for user experience.

The author concludes by acknowledging the invaluable contributions of Frank McSherry's differential-dataflow crate and discussions with various researchers that inspired this alias-based approach to borrow checking.