---
title: "A Formal Look at Pinning"
categories: research rust
+forum: https://internals.rust-lang.org/t/a-formal-look-at-pinning/7236
---
Recently, a new API for "pinned references" has [landed as a new unstable feature](https://github.com/rust-lang/rust/pull/49058) in the standard library.
The most intersting piece of code here is `read_ref`, which dereferences a raw pointer.
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 `Some`).
-In particular, if we changed the signature of `init()` to take `&mut`, we could easily cause UB by writing the following code:
+In particular, if we changed the signature to `fn init(&mut self)`, we could easily cause UB by writing the following code:
{% highlight rust %}
fn main() {
// Create an initialize a SelfReferential in a Box, move it out, and drop the Box
For example, the axiom (a) stated above would look as follows:
```
forall |'a, ptr|
- borrowed('a, exists |bytes| mem_own(ptr, bytes) && T.own(bytes))
+ borrowed('a, exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes))
-> T.shr('a, ptr)
```
I am using the usual mathematical quantifiers, with a Rust-y syntax (`forall |var| P` and `exists |var| P`), and `->` for implication.
For disjunction (`||`) and conjunction (`&&`), I follow Rust.
We also need some way to talk about ownership and contents of memory:
-I will write `mem_own_bytes(ptr, bytes)` (where `ptr: Pointer` and `bytes: List<Byte>`) to express that we own `bytes.len()` many bytes of memory pointed to by `ptr`.
+I will write `ptr.points_to_owned_bytes(bytes)` (where `ptr: Pointer` and `bytes: List<Byte>`) to express 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.
Frequently, it is more convenient to not talk about raw lists of bytes but about some higher-level representation of the bytes, and not care about how exactly that data is laid out in memory.
-For example, we might want to say that `ptr` points to `42` of type `i32` by saying `mem_own(ptr, 42i32)`.
-We can define a suitable `mem_own` as
+For example, we might want to say that `ptr` points to `42` of type `i32` by saying `ptr.points_to_owned(42i32)`.
+We can define a suitable `points_to_owned` as
```
-mem_own<U>(ptr: Pointer, data: U) where List<Bytes>: TryInto<U> :=
- exists |bytes| bytes.try_into() == Ok(data) && mem_own(ptr, bytes)
+ptr.points_to_owned(data: U) where List<Bytes>: TryInto<U> :=
+ exists |bytes| bytes.try_into() == Ok(data) && ptr.points_to_owned_bytes(bytes)
```
Here, we (ab)use the `TryInto` trait to convert a properly laid out list of bytes into something of type `U`.
The conversion fails, in particular, if the list does not have exactly the right length.
-If `U == List<Bytes>`, this is just the same as `mem_own_bytes`.
+If `U == List<Bytes>`, this is just the same as `ptr.points_to_owned_bytes`.
+
+**Update:** In a previous version I called these predicates `mem_own_bytes` and `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 `mem_own(ptr, 42i32)`.
+`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(42i32)`.
You can think of propositions as a fancy version of `bool` where we can use things like quantifiers or 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:
`&'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) && mem_own(ptr, inner_bytes) && T.own(inner_bytes)
+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| mem_own(ptr, inner_bytes) && T.own(inner_bytes))
+ borrowed('a,
+ exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))
```
It turns out that using `try_into` like we do above is actually a common pattern.
This could look as follows:
```
Box<T>.own(ptr: Pointer) :=
- exists |inner_bytes| mem_own(ptr, inner_bytes) && T.own(inner_bytes)
+ exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)
+```
+```
(&'a mut T).own(ptr: Pointer) :=
- borrowed('a, exists |inner_bytes| mem_own(ptr, inner_bytes) && T.own(inner_bytes))
+ borrowed('a, exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))
```
The actual ownership predicate is then defined as
```
Moreover, if `self_ref` is set to `Some(data_ptr)`, then `data_ptr` is the address of the first field of the pair:
```
SelfReferential.pin(ptr) := exists |data: i32, self_ref: Option<ptr::NonNull<i32>>|
- mem_own(ptr, (data, self_ref)) &&
+ ptr.points_to_owned((data, self_ref)) &&
match self_ref { Some(data_ptr) => data_ptr.as_ptr() == ptr.offset(0), None => True }
```
The most important part of this is the last line, saying that if `data_ptr` is a `Some`, it actually points to the first field (at offset `0`).
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))
```
> {:type="a" start="2"}
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| (mem_own(ptr, bytes) && T.own(bytes)) -> T.pin(ptr)
+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| mem_own(ptr, bytes) && 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!
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|
- mem_read_only('a, ptr, inner_ptr) && T.shr('a, 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 `mem_read_only_bytes('a: Lifetime, ptr: Pointer, bytes: List<Byte>)` for this purpose, and then define a typed variant as usual:
+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:
```
-mem_read_only<U>('a: Lifetime, ptr: Pointer, data: U) where List<Bytes>: TryInto<U> :=
- exists |bytes| bytes.try_into() == Ok(data) && mem_read_only_bytes('a, ptr, bytes)
+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.
> **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| mem_own(ptr, bytes) && T.own(bytes))
+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.
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| mem_own(ptr, bytes) && 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.
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.
+I am looking forward to hearing your [comments](https://internals.rust-lang.org/t/sharing-for-a-lifetime/7236).
In particular, I am curious if the made-up syntax for making the typestate invariants more precise was helpful.
projects / web.git / blobdiff