Reference-counted smart pointer, tutorial

Our next example is a reference-counted smart pointer like Rc.

We’re going to focus on 4 functions: new, clone, and drop, and borrow. The clone and drop functions will be incrementing and decrementing the reference count, and drop will be responsible for freeing memory when the count hits zero. Meanwhile, the borrow function provides access to the underlying data. Recall that since Rc is a shareable pointer, the underlying data must be accessed via shared pointer.

type Rc<T>

impl<T> Rc<T> {
    pub spec fn view(&self) -> T;

    pub fn new(t: T) -> (rc: Self)
        ensures rc@ === t

    pub fn clone(&self) -> (rc: Self)
        ensures rc@ === self@

    pub fn drop(self)

    pub fn borrow(&self) -> (t: &T)
        ensures *t === self@
}

In terms of specification, the view() interpretation of an Rc<T> object will simply be the underlying T, as is reflected in the post-conditions above.

NOTE: A current limitation, at the time of writing, is that Verus doesn’t yet have proper support for Drop, so the drop function of our Rc here needs to be called manually to avoid memory leaks.

Unverified implementation

As usual, we’ll start with an unverified implementation.

// Ordinary Rust code, not Verus

struct InnerRc<T> {
    rc_cell: std::cell::UnsafeCell<u64>,
    t: T,
}

struct Rc<T> {
    ptr: *mut InnerRc<T>,
}

impl<T> Rc<T> {
    fn new(t: T) -> Self {
        // Allocate a new InnerRc object, initialize the counter to 1,
        // and return a pointer to it.
        let rc_cell = std::cell::UnsafeCell::new(1);
        let inner_rc = InnerRc { rc_cell, t };
        let ptr = Box::leak(Box::new(inner_rc));
        Rc { ptr }
    }

    fn clone(&self) -> Self {
        unsafe {
            // Increment the counter.
            // If incrementing the counter would lead to overflow, then abort.
            let inner_rc = &*self.ptr;
            let count = *inner_rc.rc_cell.get();
            if count == 0xffffffffffffffff {
                std::process::abort();
            }
            *inner_rc.rc_cell.get() = count + 1;
        }

        // Return a new Rc object with the same pointer.
        Rc { ptr: self.ptr }
    }

    fn drop(self) {
        unsafe {
            // Decrement the counter.
            let inner_rc = &*self.ptr;
            let count = *inner_rc.rc_cell.get() - 1;
            *inner_rc.rc_cell.get() = count;

            // If the counter hits 0, drop the `T` and deallocate the memory.
            if count == 0 {
                std::ptr::drop_in_place(&mut (*self.ptr).t);
                std::alloc::dealloc(self.ptr as *mut u8, std::alloc::Layout::for_value(&*self.ptr));
            }
        }
    }

    fn borrow(&self) -> &T {
        unsafe { &(*self.ptr).t }
    }
}

// Example usage

enum Sequence<V> {
    Nil,
    Cons(V, Rc<Sequence<V>>),
}

fn main() {
    let nil = Rc::new(Sequence::Nil);
    let nil_clone = nil.clone();
    let a5 = Rc::new(Sequence::Cons(5, nil.clone()));
    let a7 = Rc::new(Sequence::Cons(7, nil.clone()));
    let a67 = Rc::new(Sequence::Cons(6, a7.clone()));

    let x1 = nil.borrow();
    let x2 = nil_clone.borrow();
    match x1 {
        Sequence::Nil => {}
        Sequence::Cons(_, _) => {
            assert!(false);
        }
    }
    match x2 {
        Sequence::Nil => {}
        Sequence::Cons(_, _) => {
            assert!(false);
        }
    }

    nil.drop();
    nil_clone.drop();
    a5.drop();
    a7.drop();
    a67.drop();
}

Verified implementation

The main challenge here is to figure out what structure the ghost code will take.

• We need a “something” that will let us get the &PointsTo object that we need to dereference the pointer. This has to be a shared reference by necessity.
• The “something” needs to be duplicateable somehow; we need to obtain a new one whenever we call Rc::clone.
  • The counter, somehow, needs to correspond to the number of “somethings” in existence. In other words, we should be able to get a new “something” when we increment the counter, and we should destroy a “something” when we decrement it.
• We need a way to obtain ownership of the the PointsTo object for the PCell storing the counter, so that we can write to it.

Let’s stop being coy and name the ghost components. The “something” is the driver of action here, so let’s go ahead and call it a ref. Let’s have another ghost object called a counter—the counter counts the refs. The ghost counter needs to be tied to the actual u64 counter, which we will do with a LocalInvariant.

Therefore, an Rc ought to have:

• A ref object, which will somehow let us obtain access a &ptr::PointsTo<InnerRc>.
• A LocalInvariant storing both a counter and a cell::PointsTo<u64>.

Now, with this rough plan in place, we can finally begin devising our tokenized_state_machine to define the ref and counter tokens along with the relationship between the ref token and the ptr::PointsTo.

tokenized_state_machine!(RefCounter<Perm> {
    fields {
        #[sharding(variable)]
        pub counter: nat,

        #[sharding(storage_option)]
        pub storage: Option<Perm>,

        #[sharding(multiset)]
        pub reader: Multiset<Perm>,
    }

TODO - finish the rest of this tutorial