Code Monkey home page Code Monkey logo

ghost-cell's Introduction

A novel safe and zero-cost borrow-checking paradigm from the GhostCell paper.

Motivation

A number of collections, such as linked lists, binary trees, or B-trees are most easily implemented with aliasing pointers.

Traditionally, this means using run-time borrow-checking in order to still be able to mutate said structures, or using unsafe in the name of performance.

By using brands, GhostCell separate the data from the permission to mutate it, and uses a unique GhostToken to model this permission, tied at compile-time to a number of said GhostCells via the brand.

Safety

In the GhostCell paper, Joshua Yanovski and his colleagues from MPI-SWS, Germany, formally demonstrate the safety of GhostCell using the separation logic they have developed as part of the RustBelt project. I personally would trust them on this.

The official implementation can be found at https://gitlab.mpi-sws.org/FP/ghostcell/-/tree/master/ghostcell, along with examples. The current implementation will be upgraded soonish, now that I'm aware of it.

Use at your own risks!

(And please report any issue)

Maturity

This is very much an Alpha quality release, at best.

Documentation:

  • All methods are documented.
  • All non-trivial methods have examples.

Tests:

  • All non-trivial methods are tested, via their examples.
  • All methods with safety invariants are covered with compile-fail tests.
  • The entire test-suite, including examples, runs under Miri.

How to use?

Let's start with a self-contained example:

use ghost_cell::{GhostToken, GhostCell};

fn demo(n: usize) {
    let value = GhostToken::new(|mut token| {
        let cell = GhostCell::new(42);

        let vec: Vec<_> = (0..n).map(|_| &cell).collect();

        *vec[n / 2].borrow_mut(&mut token) = 33;

        *cell.borrow(&token)
    });

    assert_eq!(value, 33);
}

GhostToken uses the best known way to generate a unique lifetime, hence used as a brand, which is to combine:

  • A local variable, created within the GhostToken::new method.
  • A closure which must be valid for all lifetimes.

This means 2 restrictions:

  • The closure must be variant over the lifetimes, this does not always play well with closures already containing references.
  • None of the branded items can be returned by the closure.

Then, within the closure, any GhostCell can be associated to one, and only one, GhostToken which will encode its borrowing permissions:

  • &GhostToken<'brand> is the key to using GhostCell<'brand, T>::borrow -- note the matching 'brand -- and allows obtaining a &T reference.
  • &mut GhostToken<'brand> is the key to using GhostCell<'brand, T>::borrow_mut and allows obtaining a &mut T reference.

Using borrow or borrow_mut borrow both the cell and the token.

So what?

A GhostCell is a safe, zero-cost, cell. It allows aliasing with compile-time checked borrow-checking.

Combined with StaticRc, it allows writing doubly linked lists, binary trees and B-trees with parent pointers, etc... in safe, stable, Rust.

Other Cells

There are other cells in existence, performing a similar function with different trade-offs:

  • The standard Cell and RefCell.
  • The multiple cells of the qcell crate, of which LCell is based on discussions with the author of GhostCell, sharing a similar idea.

That's all folks!

And thanks for reading.

ghost-cell's People

Contributors

matthieu-m avatar wackbyte avatar konsumlamm avatar yuk1ty avatar programmerjake avatar mkatychev avatar noamtashma avatar

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.