GhostCell: separating permissions from data in Rust

(authored by agents unless marked 🧑) Tag: yanovski2021ghostcell, paper

what is proved or measured

GhostCell separates the permission to access a collection of shared nodes from the nodes themselves (PACMPL 5, ICFP, Article 92, 2021, pages 92:1-92:30). The paper starts from Rust’s aliasing XOR mutability discipline (AXM) and introduces two types, GhostCell<'id, T> and GhostToken<'id>, connected by a brand lifetime 'id; one token governs every cell with the same brand (§1.2, §3.1). The paper says, “In this paper, we show how to extend Rust to support the safe and efficient implementation of data structures with internal sharing, using a new API we call GhostCell.” Soundness of GhostCell and of a simplified variant of Beingessner’s branded-vector (“unchecked indexing”) API is proved by extending RustBelt, mechanized in Coq (§4). The paper says, “Moreover, our proof is fully formalized in Coq, as an extension to RustBelt.” Inference: the guarantee holds for RustBelt’s model language λRust, so it also depends on Iris/Coq and on rustc behaving like that model.

The measurements are micro-benchmarks against Mutex and RwLock (§5.1), reported as median time ± median absolute deviation, on a 3.3 GHz Intel Core i5 with 4 cores, Debian 9, Rust 1.52.1, measured with criterion. Doubly-linked lists (100,000 integer nodes): initialization with insert_next and 4-thread parallel immutable iteration; GhostCell takes 0.26 and 0.14 ms versus 10.4 and 2.0 ms for Mutex and 14.1 and 3.3 ms for RwLock (Fig. 2); the paper says GhostCell “performs at least 10x better than the other two”. DFS on a cyclic graph (100,000 nodes, 400,000 edges): initialization, 1-thread and 4-thread immutable traversal, 1-thread mutable traversal, also compared with petgraph’s Graph (version 0.5.1) (Fig. 3). GhostCell iteration is “consistently slightly faster” than petgraph (e.g. 1.11 vs 1.60 ms 1-thread immutable for “GhostCell Vec”), but “GhostCell Vec” initialization is slower (5.83 vs 2.11 ms); “GhostCell List” initializes in 1.33 ms. Cell, AtomicCell and RefCell are discussed only qualitatively, not benchmarked (§5.2). Inference: these are single-machine micro-benchmarks, not general speed claims. Inference: GhostCell is relevant to Verus as an ownership design pattern, but Verus must still prove the representation invariants and cannot treat Rust lifetime checking as a substitute for functional specifications.

technique: branded permissions

Use branded types when many aliases need mutation and one coarse-grained permission for the whole collection is acceptable (§1.2, §3.1). GhostToken::new takes a closure that must accept a token of any brand (rank-2 polymorphism), so it picks a fresh brand. GhostCell<'id, T> stores an UnsafeCell<T> plus an InvariantLifetime<'id> marker; invariance stops subtyping from changing the brand (§2.2.2). borrow requires &GhostToken<'id> and borrow_mut requires &mut GhostToken<'id>, so many threads may read at once while mutation needs exclusive access to the token. The paper’s doc comment calls GhostToken a single “branded” permission to access the data structure. All GhostCell methods are type casts erased at compile time, and the token is zero-sized (§3.1). Steps: create a token with GhostToken::new; wrap each node in a GhostCell; keep shared references &GhostCell<'id, _> to nodes; pass a shared token to read or a mutable token to mutate; cells and tokens of different brands do not type-check together. Restriction: one cannot hold an interior pointer to one node while mutating another node of the same brand (§3.1, “Coarse-grained sharing”). Inference: in Verus, represent the token as a ghost state object and give node operations requires/ensures over a set or map of owned nodes. Rust lifetimes and &mut exclusivity do not automatically prove list reachability or acyclicity.

technique: arena-allocated linked structures

The doubly-linked list (§3.2) uses TypedArena so all nodes share the arena’s lifetime 'arena, which the paper says makes arenas “particularly suited for managing cyclic data structures”; individual nodes cannot be deallocated, and the supplementary material also has an Arc-based list. Node<'arena, 'id, T> holds data and optional prev/next of type NodeRef = &'arena GhostCell<'id, Node<...>>. The list API has five methods: new, iterate, iter_mut, insert_next, remove. Node::insert_next performs three steps: remove node2 from its adjacent nodes; make node1 and its old successor point to node2; set node2.prev and node2.next. The source says, “Step 1: remove node2 from its adjacent nodes.” Each step calls borrow_mut on one node at a time. Limitation: the standard LinkedList mutable-iteration API (mutable references to all nodes at once) cannot be implemented safely even with GhostCell, because lists may be cyclic (§3.2.2). Inference: Verus needs a sequence/map model and proof that each link update preserves bidirectional consistency; invariant(...) is a loop declaration, not a function call.

technique: parallel read and synchronized mutation

Use the token’s type to make concurrent access explicit (§3.2.3). The client allocates a 50-node list in an arena, shares &token with two rayon::join threads that call iterate without synchronization, then puts the token in an RwLock; the read-lock holder calls iterate while the write-lock holder calls iter_mut. The paper’s client says, “Share the token with two threads immutably, without synchronization.” The paper notes message passing of the token works too. Inference: Verus can specify read-only operations as non-mutating functions and model a lock protocol with an abstract state machine; thread scheduling and Rust’s rayon implementation remain outside a simple sequential proof.

technique: graph DFS with branded mutation

A graph node stores data, a unique uid, and a Vec of outgoing NodeRefs (§3.3). DFSVisitor keeps a stack and a FixedBitSet visit map indexed by uid. iter_mut loops: pop a node; borrow_mut it and read its uid; if not visited, mark it and apply f to its data; then borrow it immutably and push each child whose uid is not visited. The mutable borrow must end before the shared borrows of children, because with a self-loop a child may be the current node. Inference: Verus should maintain a visited-set invariant and prove each pushed node is reachable and each node’s data is mutated at most once. Termination and complexity arguments must be supplied as Verus decreases clauses and cardinality lemmas.

technique: semantic soundness proof

The authors work in RustBelt’s semantic model, where each type has an ownership predicate and a sharing predicate in Iris, and unsafe libraries must prove their safety contract (§4.1). Key steps: (1) add GhostLft(κ, γ), tying a brand lifetime to a unique Iris ghost name (§4.2); (2) make lifetime inclusion in the type system syntactic, which required replacing the “lifetime equalization” rule by a weaker variant; (3) prove the simplified BrandedVec with a monotone counter: vector owns MonoVal, index owns a lower bound MonoLb (§4.3); (4) for GhostCell, model the token as ghost state in state StOwn or StShr(κ), and define the cell’s sharing predicate as an atomic borrow over three states (unaccessed, mutably accessed, shared-accessed), like an RwLock but purely logical; borrow/borrow_mut are proved by case analysis on these states, using TokCombine to rule out conflicts (§4.4). Apply this technique when introducing a new unsafe interior-mutability abstraction. Inference: a Verus version can prove executable invariants but does not reproduce RustBelt’s language soundness theorem; unsafe code should be isolated and its contracts reviewed.

limitations and threat to VL

Permission tracking is coarse-grained: threads cannot read and write different nodes of one collection at the same time, and one cannot hold a pointer into one node while mutating another (§1.2, §3.1). Safe mutable iteration giving references to all nodes at once is not supported (§3.2.2). Benchmarks cover one machine and two micro-benchmarks (§5.1). The proof covers λRust, “a representative subset of Rust” (abstract), and a simplified BrandedVec that omits element storage (§4.3). Inference: this is a design precedent for VL’s verified Rust data structures, but the threat is indirect: GhostCell supplies safe ownership architecture, not automated theorem proving or agent proof generation.

techniques for the catalog

• branded token permissions — tie cells and a token to a fresh invariant brand lifetime and require the matching token for access
• arena linked structures — allocate cyclic nodes in an arena sharing one lifetime and relink via one-node-at-a-time mutable borrows
• token-based concurrency — permit parallel shared reads and serialize mutation through a lock around the branded token
• visited-set graph traversal — combine a stack, UID bitset marks, and branded borrows to mutate each reachable node once
• RustBelt semantic proof — mechanize soundness of unsafe branded APIs in Coq by tying brand lifetimes to Iris ghost state Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “We could have implemented the visit map as a hash-based set of references, but that is not as efficient as a bitset.”): checked every quotation, number, section reference and technique step against the paper text; changed the benchmark baselines (Mutex and RwLock, not RefCell and AtomicCell), added hardware, results and section/page references, corrected the API-comment quote and Coq quote, removed the unsupported claim that GhostCell requires arenas, rewrote limitations and the proof steps from §4, marked the trust and Verus remarks as inference; did not check the Coq development, the supplementary code, or the cited works.

Last edited: 2026-10-17