A Formal Look at Pinning

Recently, a new API for “pinned references” has landed as a new unstable feature in the standard library. The purpose of these references is to express that the data at the memory it points to will not, ever, be moved elsewhere. @withoutboats has written about how this solves a problem in the context of async IO. In this post, we take a closer, more formal look at that API: We are going to take a stab at extending the RustBelt model of types with support for pinning.

But before we get started, I have to lay down some basics.

Rust types: Recap

I have discussed my model of Rust types in a previous post; this may me a good time to read that post as I will be using it as a starting point. The short version is that I view Rust types with private invariants as not having just a single invariant, but different invariants that reflect the different “modes” the type can be in. @cramertj suggested to use “typestate” as terminology here, and I agree that this makes sense.

Definition 1: Rust types. Every Rust type T comes with two typestates, each having an invariant:

1. The owned typestate with invariant T.own(bytes) (where bytes: List<Byte>), saying whether the given sequence of bytes constitutes a valid fully owned T.
2. The shared typestate with invariant T.shr('a, ptr) (where 'a: Lifetime and ptr: Pointer), saying whether ptr is a valid pointer to an instance of T that has been shared for lifetime 'a.

Moreover, those two states must be connected in the sense that the following axiom always holds:

1. If we have borrowed, for lifetime 'a, a pointer ptr pointing to a list of bytes bytes such that T.own(bytes) holds, then we can move to the shared typestate and obtain T.shr('a, ptr). (Implicitly, when the original borrow ends, the type is moved back to the owned typestate.)

This axiom ensures that we can create a shared reference to something we own.

You may be wondering why sharing is a separate typestate here; shouldn’t that just be read-only access to a T that someone else owns? However, that clearly doesn’t work for &Cell; to explain types with interior mutability we need sharing as a separate state. I explained this in more detail in the previous post, but as a quick example consider that, if you fully own a RefCell, the first field (storing the current count of readers/writers) has no special meaning whatsoever. This is witnessed by RefCell::get_mut ignoring that field. In fact, it would be sound to add a RefCell::reset(&mut self) that just resets this field to 0.

Pinning

Now, let us extend our notion of types to also support pinning. The core piece of the pinning API is a new reference type Pin<'a, T> that guarantees that the data it points to will remain at the given location, i.e. it will not be moved. Crucially, pinning does not provide immovable types! Data is only pinned after a Pin<T> pointing to it has been created; it can be moved freely before that happens.

The corresponding RFC explains the entirey new API surface in quite some detail: Pin, PinBox and the Unpin marker trait. I will not repeat that here but only show one example of how to use Pin references and exploit their guarantees:

#![feature(pin, arbitrary_self_types, optin_builtin_traits)]

use std::ptr;
use std::mem::Pin;
use std::boxed::PinBox;
use std::marker::Unpin;

struct SelfReferential {
    data: i32,
    self_ref: *const i32,
}
impl !Unpin for SelfReferential {}

impl SelfReferential {
    fn new() -> SelfReferential {
        SelfReferential { data: 42, self_ref: ptr::null()  }
    }

    fn init(mut self: Pin<SelfReferential>) {
        let this : &mut SelfReferential = unsafe { Pin::get_mut(&mut self) };
        // Set up self_ref to point to this.data.
        this.self_ref = &this.data as *const i32;
    }

    fn read_ref(self: Pin<SelfReferential>) -> Option<i32> {
        let this : &SelfReferential = &*self;
        // Dereference self_ref if it is non-NULL.
        if this.self_ref == ptr::null() {
            None
        } else {
            Some(unsafe { *this.self_ref })
        }
    }
}

fn main() {
    let mut s = PinBox::new(SelfReferential::new());
    s.as_pin().init();
    println!("{:?}", s.as_pin().read_ref()); // prints Some(42)
}

Update: Previously, the example code used Option<ptr::NonNull<i32>>. I think using raw pointers directly makes the code easier to follow. /Update

The most intersting piece of code here is read_ref, which dereferences a raw pointer, this.self_ref. The reason this is legal is that we can rely on the entire SelfReferential not having been moved since init() was called (which is the only place that would set the pointer to something non-NULL).

In particular, if we changed the signature to fn init(&mut self), we could easily cause UB by writing the following code:

fn main() {
    // Create an initialize a SelfReferential in a Box, move it out, and drop the Box
    let s = { let b1 = Box::new(SelfReferential::new()); b1.init(); *b1 };
    let mut b2 = PinBox::new(s); // move the initialized SelfReferential into a new PinBox
    println!("{:?}", b2.as_pin().read_ref()); // Cause explosion
}

Now read_ref() will dereference a pointer into the memory that was allocated for b1, but has since then been deallocated! This is clearly wrong.

This example also shows that there cannot be a safe conversion from &mut T to Pin<T>: That would let us implement the problematic init_ref(&mut self) by calling init(self: Pin<Self>). In contrast, converting Box<T> to PinBox<T> is fine because this consumes the Box, so nobody will ever get “unpinned” access to it.

Pin lets us give a type to SelfReferantial that makes it safe to use. This is in the best tradition of Rust: We are using an expressive type system to provide safe APIs for operations that only have unsafe APIs in other languages (e.g., iterators that avoid iterator invalidation which plague even memory safe languages like Java). In the following, I will explain how one can prove that our claim of safe encapsulation actually holds true. This is building on the framework that we developed for the RustBelt paper.

Formal Notation

Before we go on, I’d like to introduce some notation to make it easier to talk about ownership and borrowing of memory in a precise way. I feel like trying to express this all just in English and leaving away the formalism is not actually making it easier to understand. The full formalism we use in the paper is probably overkill, so I will go with a simplified version that glosses over many of the details.

For example, the axiom (a) stated above would look as follows:

forall |'a, ptr|
  borrowed('a, exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes))
  -> T.shr('a, ptr)

This is a formal statement that we have to prove whenever we define T.own and T.shr for our own type T. It says that for all lifetimes 'a and pointers ptr, if borrowed('a, ...) holds, then T.shr('a, ptr) holds. I am using the usual mathematical quantifiers, with a Rust-y syntax (forall |var| ... and exists |var| ...), and -> for implication. For disjunction (||) and conjunction (&&), I follow Rust.

Because Rust types are a lot about pointers and what they point to, we also need some way to talk about memory: ptr.points_to_owned(bytes) (where ptr: Pointer and bytes: List<Byte>) means that ptr points to bytes.len() many bytes of memory containing the given bytes of data, and that moreover, we own that memory. Ownership here means that we are free to read, write and deallocate that memory, and that we are the only party that can do so.

Update: In a previous version I called this predicate mem_own. I decided that points_to_owned was actually easier to understand, and it also matches the standard terminology in the literature, so I switched to using that term instead. /Update

Finally, borrowed('a, P) says that P is only temporarily owned, i.e., borrowed, for lifetime 'a. P here is a proposition or assertion, i.e., a statement about what we expect to own. The axiom above is a proposition, as is ptr.points_to_owned([0, 0]). You can think of propositions as a fancy version of bool where we can use things like quantifiers and borrowing, and talk about memory and ownership.

Let us see how we can define the owned typestate of Box and mutable reference using this notation:

Definition 2: Box<T>.own and (&'a mut T).own. A Box<T> is a list of bytes that make up a pointer, such that we own the memory this pointer points to and that memory satisfies T.own. &'a mut T is almost the same, except that memory and T.own are only borrowed for lifetime 'a. Formally:

Box<T>.own(bytes) := exists |ptr, inner_bytes| bytes.try_into() == Ok(ptr) &&
  ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)

(&'a mut T).own(bytes) := exists |ptr| bytes.try_into() == Ok(ptr) &&
  borrowed('a,
    exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))

The := means “is defined as”; this is a lot like a function definition in Rust where the part after the := is the function body. Notice how we use try_into to try to convert a sequence of bytes into a higher-level representation, namely a pointer. This relies in TryInto<U> being implemented for List<Byte>. The conversion fails, in particular, if the list of bytes does not have exactly the right length.

It turns out that using try_into like we do above is actually a common pattern: Often, when we define a predicate on bytes, we do not want to talk directly about the List<Byte> but convert them to some higher-level representation first. To facilitate this, we will typically define T.own(data: U) for some U such that List<Byte>: TryInto<U>, the idea being that the raw list of bytes is first converted to a U and the predicate can then directly access the higher-level data in U. This could look as follows:

Box<T>.own(ptr: Pointer) :=
  exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)

(&'a mut T).own(ptr: Pointer) :=
  borrowed('a, exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))

The actual ownership predicate is then defined as

exists |data: U| bytes.try_into() == Ok(data) && T.own(data)

Extending Types to Verify SelfReferential

Coming back to our example, what would it take to prove that SelfReferential can be used by arbitrary safe code? We have to start by writing down the private invariants (for all typestates) of the type. We want to say that if self.read_ref is not NULL, then it is the address of self.data. However, if we go back to our notion of Rust types that I laid out at the beginning of this post, we notice that it is impossible to refer to the “address of self.data” in T.own! And that’s not even surprising; this just reflects the fact that in Rust, if we own a type, we can always move it to a different location—and hence the invariant must not depend on the location.

So, to write down our invariant, we need to extend our notion of types. We will add a new, third typestate on top of the existing owned and shared typestates:

Definition 3a: Rust types with pinning. Extend definition 1 with a new typestate:

3. The pinned state with invariant T.pin(ptr) (where ptr: Pointer), saying whether ptr is a valid pointer to an instance of T that is considered pinned.

Notice that this state talks about a pointer being valid, in contrast to T.own which talks about a sequence of bytes. This gives us the expressivity we need to talk about immovable data: SelfReferential.pin(ptr) says that ptr points to some memory we own, and that memory stores some pair (data, self_ref), and self_ref is either NULL or the address of the first field, data, at offset 0:

SelfReferential.pin(ptr) := exists |data: i32, self_ref: *const i32|
  ptr.points_to_owned((data, self_ref)) &&
  (self_ref == ptr::null() || self_ref == ptr.offset(0))

(In terms of memory layout, SelfReferential is the same as a pair of i32 and *const i32. I am of course glossing over plenty of details here, but those details are not relevant right now. Moreover, SelfReferential also has an owned and a shared typestate, but nothing interesting happens there.)

With this choice, it is easy to justify that read_ref is safe to execute: When the function begins, we can rely on SelfReferential.pin(self). If we enter the else branch, we know self_ref is not NULL, hence it must be ptr.offset(0). As a consequence, the deref of self_ref is fine.

Before we go on, I have to explain what I did with points_to_owned above. Before I said that this predicate operates on List<Byte>, but now I am using it on a pair of an i32 and a raw pointer. Again this is an instance of using a higher-level view of memory than a raw list of bytes. For example, we might want to say that ptr points to 42 of type i32 by saying ptr.points_to_owned(42i32), without worrying about how to turn that value into a sequence of bytes. It turns out that we can define points_to_owned in terms of a lower-level points_to_owned_bytes that operates on List<Byte> as follows:

ptr.points_to_owned(data: U) where List<Bytes>: TryInto<U> :=
  exists |bytes| bytes.try_into() == Ok(data) && ptr.points_to_owned_bytes(bytes)

Just like before, we (ab)use the TryInto trait to convert a properly laid out list of bytes into something of type U.

Verifying the Pin API

With our notion of types extended with a pinned typestate, we can now justify the Pin and PinBox API. We will start with the methods that work for all types, and talk about the additional methods that require Unpin later. Along the way, we will discover which additional axioms we need to add to connect our new pinned typestate to the existing ones. This is where we get really technical.

Again, to verify a type, we first have to define its invariant for all typestates. Let us focus on the owned typestate:

Definition 4: PinBox<T>.own and Pin<'a, T>.own. A list of bytes makes a valid PinBox<T> if those bytes form a pointer ptr such that we own T.pin(ptr). For Pin<'a, T>, ptr is valid if we have borrowed T.pin(ptr) for lifetime 'a.

PinBox<T>.own(ptr) := T.pin(ptr)

Pin<'a, T>.own(ptr) := borrowed('a, T.pin(ptr))

Let us start with the impl<T> From<Box<T>> for PinBox<T> , which can turn a Box<T> into a PinBox<T> in-place. We can assume that self satisfies the owned typestate invariant of Box<T>, and we have to prove that our return value (which is the same pointer) satisfies the owned typestate invariant of PinBox<T>. To justify this conversion, we need to turn a pointer to a fully owned T into a pinned T at the same location. This seems like a reasonable principle to require in general, so we add it to our definition of types:

Definition 3b: Rust types with pinning. Extend definition 3a with a new axiom:

2. If we own a pointer ptr pointing to a list of bytes bytes such that T.own(bytes) holds, then we can move to the pinned typestate and obtain T.pin(ptr). Formally:

   forall |ptr, bytes| (ptr.points_to_owned(bytes) && T.own(bytes)) -> T.pin(ptr)
   

PinBox::new can now be easily implemented using Box::new and PinBox<T>::from.

For PinBox::as_pin, we start with a &'a mut PinBox<T>, which is a pointer-to-pointer, and return the inner pointer as Pin<'a, T>. This is justified because we start with a borrow for lifetime 'a of a pointer to some bytes that satisfy (for the given lifetime) PinBox<T>.own(bytes):

borrowed('a, exists |bytes| ptr.points_to_owned(bytes) && PinBox<T>.own(bytes))

Unfolding the PinBox<T>.own, we can deduce that bytes actually form a pointer inner_ptr such that T.pin(inner_ptr) (for the given lifetime). This exactly matches our return type, so we’re good!

Finally, let us look at impl<T> Deref for PinBox<T>. This is where the shared typestate of PinBox becomes relevant: This impl turns a &'a PinBox<T> into a &'a T by dereferencing it once. To justify this, we have to be able to move from the pinned typestate of T to the shared typestate, which we require as our final additional axiom:

Definition 3c: Rust types with pinning. Extend definition 3b with a new axiom:

3. If we have borrowed, for lifetime 'a, a pointer ptr such that T.pin(ptr) holds, then we can move to the shared typestate and obtain T.shr('a, ptr). (Implicitly, when the original borrow ends, the type is moved back to the owned typestate.) Formally:

   forall |'a, ptr| borrowed('a, T.pin(ptr)) -> T.shr('a, ptr)
   

This is the final definition of Rust types with pinning.

Now we have connected the new pinned typestate with both the owned and the shared typestate, so these should be all the axioms we need.

Next, we define the shared typestate of PinBox<T>:

Definition 5: PinBox<T>.shr. A pointer ptr and lifetime 'a satisfy the shared typestate of PinBox<T> if ptr is a read-only pointer to another pointer inner_ptr such that T.shr('a, inner_ptr). In other words, a shared PinBox<T> is just a read-only pointer to a shared T:

PinBox<T>.shr('a, ptr) := exists |inner_ptr|
  ptr.points_to_read_only('a, inner_ptr) && T.shr('a, inner_ptr)

This requires a way to talk about memory that is read-only for the duration of some lifetime. We assume we have a predicate ptr.points_to_read_only_bytes('a: Lifetime, bytes: List<Byte>) saying that ptr points to bytes.len() many bytes of valid memory containing bytes, and that for lifetime 'a, we are free to read that memory and it will not change. We then define a convenient variant based on higher-level memory representations as usual:

ptr.points_to_read_only('a: Lifetime, data: U) where List<Bytes>: TryInto<U> :=
  exists |bytes| bytes.try_into() == Ok(data) && ptr.points_to_read_only_bytes('a, bytes)

Remember that there is an axiom (a) connecting the owned and shared typestate; we have to make sure that this axiom is satisfied for PinBox—it turns out that is the case, and the proof relies on the new axiom (c) we just added. With this definition of PinBox<T>.shr, justifying the impl<T> Deref for PinBox<T> is fairly straight-forward.

This completes the methods available on PinBox. Verifying Pin follows the same approach, so I am not going to spell that out here.

Unpin

The Unpin marker trait lets type opt-out of pinning: If a type is Unpin, the type doesn’t actually care about being pinned and hence we can freely convert between &'a mut T and Pin<'a, T>. Formally speaking:

Definition 6: Unpin. A type T is Unpin if from T.pin(ptr) we can deduce that we own the pointer ptr and it points to a list of bytes bytes such that T.own(bytes) holds. Formally:

forall |ptr| T.pin(ptr) -> (exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes))

Note that this is exactly the inverse direction of axiom (b) added in definition 2b: For Unpin types, we can freely move between the owned and pinned typestate.

Clearly, SelfReferential is not Unpin, and the example code above makes that explicit with an impl !Unpin. On the other hand, for types like i32, their pinned typestate invariant i32.pin(ptr) will only care about the memory that ptr points to and not about the actual value of ptr, so they satisfy the Unpin axiom.

With this definition at hand, it should be clear that if we assume T: Unpin, then &'a mut T and Pin<'a, T> are equivalent types, and so are Box<T> and PinBox<T>. This justifies all the methods with an Unpin bound.

Pin is a Local Extension

One advantage of this proposal is that it is local: Existing types (and new types) that are designed without considering Pin remain sound in the presence of this new typestate, even if we automatically derive the Unpin trait for these types. The reason this works is that we can always define T.pin(ptr) as saying that we fully own ptr pointing to bytes such that we have T.own(bytes):

T.pin(ptr) := exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes)

This satisfies the additional axioms (b) and (c) connecting the pinned typestate to the others, and it also satisfies Unpin. The latter is crucial, because it means we can automatically derive Unpin instances through the auto trait mechanism and do not have to review the entire ecosystem for Pin-compatibility.

Conclusion

We have seen how the new Pin type can be used to give safe APIs to types like SelfReferential (which, previously, was not possible), and how we can (semi-)formally argue for the correctness of SelfReferential and the methods on Pin and PinBox. I hope I was able to shed some light both on how pinning is useful, and how we can reason about safety of a typed API in general. Next time, we are going to look at an extension to the pinning API proposed by @cramertj which guarantees that drop will be called under some circumstances, and how that is useful for intrusive collections.

Thanks for reading! I am looking forward to hearing your comments. In particular, I am curious if the made-up syntax for making the typestate invariants more precise was helpful.

Posted on Ralf's Ramblings on Apr 5, 2018.
Comments? Drop me a mail or leave a note in the forum!