Reachability Types with Destructive Effects

Fine-grained control and safety are often opposing choices in managing resources such as memory and I/O, with a particular concern being the timely deallocation of resources. Low-level languages like C generally prioritize control but do not provide safety; while garbage collected languages prioritize safety by prohibiting manual deallocation, at least in the case of memory. But after decades of research on regions, uniqueness, linearity, and ownership, and fueled by the success of Rust, mainstream languages are finally starting to embrace substructural type systems that promise to provide the best of both worlds: fine grained control with static safety. However, even advanced type systems such as Rust’s, whose chief design goal is to reconcile the tension between safety and control, rely on global invariants that are too rigid to uphold in practice. Specifically, even though Rust is designed around the core principle of “shared-XOR-mutable” data, Rust does not actually enforce this invariant, and allows rather uncontrolled sharing of mutable data via reference-counted variables. To ensure the safety of this abstraction, Rust has to prohibit any form of explicit destructive operations, such as closing files, sockets, or deallocating memory, and instead relies solely on static lifetime information to invoke destructor methods, which may lead to delays and/or leaks in the case of shared values. Providing advanced type systems that track lifetimes and allow controlled sharing of resources while at the same time providing explicit control over deallocation thus remains an open challenge. To fill this gap, we present the 𝜆𝜀∗-calculus, a type-and-effect system for higher-order and imperative languages. Notably, 𝜆𝜀∗ provides an explicit “free” operation, and statically guarantees the absence of “useafter-free” errors. We achieve this by building 𝜆𝜀∗ on top of reachability types, combined with flow-sensitive destructive effects to model a wide range of behaviors, such as move semantics, memory deallocation, and uniqueness. We present a formal model of 𝜆𝜀∗, prove its type safety and memory safety in Coq, and demonstrate use cases in building complex circular data structures. To our knowledge, our system is the first of its kind that can model circular, nested references in higher-order languages while statically ensuring the absence of use-after-free errors.

About David Deng

David is a third year Ph.D. student in Computer Science at Purdue University.