The Rust language offers a promising approach to safe systems programming based on the principle of
aliasing XOR mutability
: a value may be
either
aliased
or
mutable, but not both at the same time. However, to implement pointer-based data structures with internal sharing, such as graphs or doubly-linked lists, we need to be able to mutate aliased state. To support such data structures, Rust provides a number of APIs that offer so-called
interior mutability
: the ability to mutate data via method calls on a shared reference. Unfortunately, the existing APIs sacrifice flexibility, concurrent access, and/or performance, in exchange for safety.
In this paper, we propose a new Rust API called GhostCell which avoids such sacrifices by
separating permissions from data
: it enables the user to safely synchronize access to a
collection
of data via a single permission. GhostCell repurposes an old trick from typed functional programming:
branded types
(as exemplified by Haskell’s ST monad), which combine phantom types and rank-2 polymorphism to simulate a lightweight form of state-dependent types. We have formally proven the soundness of GhostCell by adapting and extending RustBelt, a semantic soundness proof for a representative subset of Rust, mechanized in Coq.
Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures