Name
Abstract | ||
|---|---|---|
AbstractThe 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. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1145/3473597 | Proceedings of the ACM on Programming Languages |
Keywords | DocType | Volume |
Rust, type systems, separation logics | Journal | 5 |
Issue | Citations | PageRank |
ICFP | 0 | 0.34 |
References | Authors | |
0 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Joshua Yanovski | 1 | 0 | 0.34 |
| Hoang-Hai Dang | 2 | 1 | 1.70 |
| Ralf Jung | 3 | 8 | 1.14 |
| Derek Dreyer | 4 | 0 | 0.34 |