一句话：提出 Rust API GhostCell，以 branded types 分离权限与数据，实现无需牺牲性能与并发安全的内部可变性，并在 Coq 中机器化验证其可靠性。
Rust 依靠“别名异或可变性”保证系统编程安全，但实现图、双向链表等内部共享的指针数据结构时仍需修改被别名引用的状态。Rust 现有的 interior mutability API 虽提供该能力，却在灵活性、并发访问或性能上有所牺牲。本文提出新的 Rust API GhostCell：它将权限与数据分离，让用户通过单个权限安全地同步访问一整组数据，从而避免上述牺牲。GhostCell 借用了类型化函数式编程中的 branded types 技巧（如 Haskell 的 ST monad），用 phantom types 与 rank-2 多态模拟轻量的依赖状态类型。作者还通过扩展 RustBelt，在 Coq 中机器化证明了 GhostCell 的可靠性。
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.
@article{paperbot1121,
title = {GhostCell: separating permissions from data in Rust},
author = {Joshua Yanovski and Hoang-Hai Dang and Ralf Jung and Derek Dreyer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473597}
}