Fully-Automatic Type Inference for Borrows with Lifetimes
We present a new pure functional language and type system with borrows with lifetimes, and a corresponding fully-automatic type inference procedure. Inference provides users the performance benefits of borrows with lifetimes without requiring user annotation. If the user's program cannot be typed, inference inserts a handful of reference count operations so that it can be typed. We provide a heap semantics for our borrowing language and prove a soundness theorem, guaranteeing that well-typed programs do not violate memory safety. We implement our memory management strategy as part of the Morphic language stack and compare it to Perceus, a state-of-the-art reference-counting technique based on linear type inference. We find that our system is able to eliminate almost all reference count operations across a range of programs, reducing reference count increments by 75-100% on all benchmarks with reference count increments under the baseline. As a result, we achieve a 1.48x geomean speedup overall on all benchmarks.
Wed 7 OctDisplayed time zone: Pacific Time (US & Canada) change
10:30 - 12:00 | Ownership, Lifetimes and RegionsOOPSLA at Junior Ballroom 1&2 Chair(s): Jenna DiVincenzo (Wise) Purdue University | ||
10:30 18mTalk | Tracking Borrows with Regular Expressions OOPSLA Todd Nowacki Mysten Labs, Sam Blackshear Mysten Labs, John Mitchell Stanford University, Shaz Qadeer Microsoft, Ilya Sergey National University of Singapore DOI | ||
10:48 18mTalk | When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking OOPSLA Siyuan He Purdue University, Songlin Jia Purdue University, Yuyan Bao Augusta University, Tiark Rompf Purdue University DOI | ||
11:06 18mTalk | Fully-Automatic Type Inference for Borrows with Lifetimes OOPSLA William Brandon Massachusetts Institute of Technology, Benjamin Driscoll Stanford University, Frank Dai Unaffiliated, Jonathan Ragan-Kelley Massachusetts Institute of Technology, Mae Milano Princeton University, Alex Aiken Stanford University DOI | ||
11:24 18mTalk | Scylla: Translating an Applicative Subset of C to Safe RustDistinguished Paper OOPSLA DOI | ||