ralf/_posts/2018-04-05-a-formal-look-at-pinning.md

   1 ---
   2 title: "A Formal Look at Pinning"
   3 categories: research rust
   4 forum: https://internals.rust-lang.org/t/a-formal-look-at-pinning/7236
   5 ---
   6
   7 Recently, a new [API for "pinned references"](https://github.com/rust-lang/rfcs/blob/master/text/2349-pin.md) has [landed as a new unstable feature](https://github.com/rust-lang/rust/pull/49058) in the standard library.
   8 The purpose of these references is to express that the data at the memory it points to will not, ever, be moved elsewhere.
   9 @withoutboats has written about how this [solves](https://boats.gitlab.io/blog/post/2018-03-20-async-vi/) a [problem in the context of async IO](https://boats.gitlab.io/blog/post/2018-01-25-async-i-self-referential-structs/).
  10 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.
  11
  12 <!-- MORE -->
  13
  14 But before we get started, I have to lay down some basics.
  15
  16 ## Rust types: Recap
  17
  18 I have discussed my model of Rust types [in a previous post]({{ site.baseurl }}{% post_url 2018-01-31-sharing-for-a-lifetime %}); this may me a good time to read that post as I will be using it as a starting point.
  19 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.
  20 @cramertj suggested to use "typestate" as terminology here, and I agree that this makes sense.
  21
  22 > **Definition 1: Rust types.** Every Rust type `T` comes with two typestates, each having an invariant:
  23
  24 > 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`.
  25 1. 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`.
  26
  27 > Moreover, those two states must be connected in the sense that the following axiom always holds:
  28
  29 > {:type="a"}
  30 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.)
  31
  32 > This axiom ensures that we can create a shared reference to something we own.
  33
  34 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?
  35 However, that clearly doesn't work for `&Cell`; to explain types with interior mutability we *need* sharing as a separate state.
  36 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.
  37 This is witnessed by [`RefCell::get_mut`](https://doc.rust-lang.org/beta/std/cell/struct.RefCell.html#method.get_mut) ignoring that field.
  38 In fact, it would be sound to add a `RefCell::reset(&mut self)` that just resets this field to `0`.
  39
  40 ## Pinning
  41
  42 Now, let us extend our notion of types to also support pinning.
  43 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.
  44 Crucially, **pinning does not provide immovable types**!
  45 Data is only pinned after a `Pin<T>` pointing to it has been created; it can be moved freely before that happens.
  46
  47 The [corresponding RFC](https://github.com/rust-lang/rfcs/blob/master/text/2349-pin.md) explains the entirey new API surface in quite some detail: [`Pin`](https://doc.rust-lang.org/nightly/std/mem/struct.Pin.html), [`PinBox`](https://doc.rust-lang.org/nightly/std/boxed/struct.PinBox.html) and the [`Unpin`](https://doc.rust-lang.org/nightly/std/marker/trait.Unpin.html) marker trait.
  48 I will not repeat that here but only show one example of how to use `Pin` references and exploit their guarantees:
  49 {% highlight rust %}
  50 #![feature(pin, arbitrary_self_types, optin_builtin_traits)]
  51
  52 use std::ptr;
  53 use std::mem::Pin;
  54 use std::boxed::PinBox;
  55 use std::marker::Unpin;
  56
  57 struct SelfReferential {
  58     data: i32,
  59     self_ref: *const i32,
  60 }
  61 impl !Unpin for SelfReferential {}
  62
  63 impl SelfReferential {
  64     fn new() -> SelfReferential {
  65         SelfReferential { data: 42, self_ref: ptr::null()  }
  66     }
  67
  68     fn init(mut self: Pin<SelfReferential>) {
  69         let this : &mut SelfReferential = unsafe { Pin::get_mut(&mut self) };
  70         // Set up self_ref to point to this.data.
  71         this.self_ref = &mut this.data as *const i32;
  72     }
  73
  74     fn read_ref(mut self: Pin<SelfReferential>) -> Option<i32> {
  75         let this : &mut SelfReferential = unsafe { Pin::get_mut(&mut self) };
  76         // Dereference self_ref if it is non-NULL.
  77         if this.self_ref == ptr::null() {
  78             None
  79         } else {
  80             Some(unsafe { *this.self_ref })
  81         }
  82     }
  83 }
  84
  85 fn main() {
  86     let mut s = PinBox::new(SelfReferential::new());
  87     s.as_pin().init();
  88     println!("{:?}", s.as_pin().read_ref()); // prints Some(42)
  89 }
  90 {% endhighlight %}
  91 **Update:** Previously, the example code used `Option<ptr::NonNull<i32>>`. I think using raw pointers directly makes the code easier to follow. **/Update**
  92
  93 The most intersting piece of code here is `read_ref`, which dereferences a raw pointer, `this.self_ref`.
  94 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).
  95
  96 In particular, if we changed the signature to `fn init(&mut self)`, we could easily cause UB by writing the following code:
  97 {% highlight rust %}
  98 fn main() {
  99     // Create an initialize a SelfReferential in a Box, move it out, and drop the Box
 100     let s = { let b1 = Box::new(SelfReferential::new()); b1.init(); *b1 };
 101     let mut b2 = PinBox::new(s); // move the initialized SelfReferential into a new PinBox
 102     println!("{:?}", b2.as_pin().read_ref()); // Cause explosion
 103 }
 104 {% endhighlight %}
 105 Now `read_ref()` will dereference a pointer into the memory that was allocated for `b1`, but has since then been deallocated!
 106 This is clearly wrong.
 107
 108 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>)`.
 109 In contrast, converting `Box<T>` to `PinBox<T>` is fine because this *consumes* the `Box`, so nobody will ever get "unpinned" access to it.
 110
 111 `Pin` lets us give a type to `SelfReferantial` that makes it safe to use.
 112 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).
 113 In the following, I will explain how one can prove that our claim of safe encapsulation actually holds true.
 114 This is building on the framework that we developed for the [RustBelt paper]({{ site.baseurl }}{% post_url 2017-07-08-rustbelt %}).
 115
 116 ## Formal Notation
 117
 118 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.
 119 I feel like trying to express this all just in English and leaving away the formalism is not actually making it easier to understand.
 120 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.
 121
 122 For example, the axiom (a) stated above would look as follows:
 123 ```
 124 forall |'a, ptr|
 125   borrowed('a, exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes))
 126   -> T.shr('a, ptr)
 127 ```
 128 This is a formal statement that we have to prove whenever we define `T.own` and `T.shr` for our own type `T`.
 129 It says that for all lifetimes `'a` and pointers `ptr`, if `borrowed('a, ...)` holds, then `T.shr('a, ptr)` holds.
 130 I am using the usual mathematical quantifiers, with a Rust-y syntax (`forall |var| ...` and `exists |var| ...`), and `->` for implication.
 131 For disjunction (`||`) and conjunction (`&&`), I follow Rust.
 132
 133 Because Rust types are a lot about pointers and what they point to, we also need some way to talk about memory:
 134 `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.
 135 *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.
 136
 137 **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**
 138
 139 Finally, `borrowed('a, P)` says that `P` is only temporarily owned, i.e., borrowed, for lifetime `'a`.
 140 `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])`.
 141 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.
 142
 143 Let us see how we can define the owned typestate of `Box` and mutable reference using this notation:
 144
 145 > **Definition 2: `Box<T>.own` and `(&'a mut T).own`.**
 146 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`.
 147 `&'a mut T` is almost the same, except that memory and `T.own` are only borrowed for lifetime `'a`.
 148 Formally:
 149 ```
 150 Box<T>.own(bytes) := exists |ptr, inner_bytes| bytes.try_into() == Ok(ptr) &&
 151   ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)
 152 ```
 153 ```
 154 (&'a mut T).own(bytes) := exists |ptr| bytes.try_into() == Ok(ptr) &&
 155   borrowed('a,
 156     exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))
 157 ```
 158
 159 The `:=` means "is defined as"; this is a lot like a function definition in Rust where the part after the `:=` is the function body.
 160 Notice how we use `try_into` to try to convert a sequence of bytes into a higher-level representation, namely a pointer.
 161 This relies in `TryInto<U>` being implemented for `List<Byte>`.
 162 The conversion fails, in particular, if the list of bytes does not have exactly the right length.
 163
 164 It turns out that using `try_into` like we do above is actually a common pattern:
 165 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.
 166 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`.
 167 This could look as follows:
 168 ```
 169 Box<T>.own(ptr: Pointer) :=
 170   exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)
 171 ```
 172 ```
 173 (&'a mut T).own(ptr: Pointer) :=
 174   borrowed('a, exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))
 175 ```
 176 The actual ownership predicate is then defined as
 177 ```
 178 exists |data: U| bytes.try_into() == Ok(data) && T.own(data)
 179 ```
 180
 181
 182 ## Extending Types to Verify `SelfReferential`
 183
 184 Coming back to our example, what would it take to *prove* that `SelfReferential` can be used by arbitrary safe code?
 185 We have to start by writing down the private invariants (for all typestates) of the type.
 186 We want to say that if `self.read_ref` is not NULL, then it is the address of `self.data`.
 187 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`!
 188 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.
 189
 190 So, to write down our invariant, we need to extend our notion of types.
 191 We will add a new, *third* typestate on top of the existing owned and shared typestates:
 192
 193 > **Definition 3a: Rust types with pinning.**  Extend definition 1 with a new typestate:
 194
 195 > {:start="3"}
 196 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.
 197
 198 Notice that this state talks about a *pointer* being valid, in contrast to `T.own` which talks about a *sequence of bytes*.
 199 This gives us the expressivity we need to talk about immovable data:
 200 `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`:
 201 ```
 202 SelfReferential.pin(ptr) := exists |data: i32, self_ref: *const i32|
 203   ptr.points_to_owned((data, self_ref)) &&
 204   (self_ref == ptr::null() || self_ref == ptr.offset(0))
 205 ```
 206 (In terms of memory layout, `SelfReferential` is the same as a pair of `i32` and `*const i32`.
 207 I am of course glossing over plenty of details here, but those details are not relevant right now.
 208 Moreover, `SelfReferential` also has an owned and a shared typestate, but nothing interesting happens there.)
 209
 210 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)`.
 211 If we enter the `else` branch, we know `self_ref` is not NULL, hence it must be `ptr.offset(0)`.
 212 As a consequence, the deref of `self_ref` is fine.
 213
 214 Before we go on, I have to explain what I did with `points_to_owned` above.
 215 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.
 216 Again this is an instance of using a higher-level view of memory than a raw list of bytes.
 217 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.
 218 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:
 219 ```
 220 ptr.points_to_owned(data: U) where List<Bytes>: TryInto<U> :=
 221   exists |bytes| bytes.try_into() == Ok(data) && ptr.points_to_owned_bytes(bytes)
 222 ```
 223 Just like before, we (ab)use the `TryInto` trait to convert a properly laid out list of bytes into something of type `U`.
 224
 225 ## Verifying the Pin API
 226
 227 With our notion of types extended with a pinned typestate, we can now justify the `Pin` and `PinBox` API.
 228 We will start with the methods that work for *all* types, and talk about the additional methods that require `Unpin` later.
 229 Along the way, we will discover which additional axioms we need to add to connect our new pinned typestate to the existing ones.
 230 This is where we get really technical.
 231
 232 Again, to verify a type, we first have to define its invariant for all typestates.
 233 Let us focus on the *owned* typestate:
 234
 235 > **Definition 4: `PinBox<T>.own` and `Pin<'a, T>.own`.**
 236 A list of bytes makes a valid `PinBox<T>` if those bytes form a pointer `ptr` such that we own `T.pin(ptr)`.
 237 For `Pin<'a, T>`, `ptr` is valid if we have borrowed `T.pin(ptr)` for lifetime `'a`.
 238 ```
 239 PinBox<T>.own(ptr) := T.pin(ptr)
 240 ```
 241 ```
 242 Pin<'a, T>.own(ptr) := borrowed('a, T.pin(ptr))
 243 ```
 244
 245 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.
 246 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>`.
 247 To justify this conversion, we need to turn a pointer to a fully owned `T` into a pinned `T` at the same location.
 248 This seems like a reasonable principle to require in general, so we add it to our definition of types:
 249
 250 > **Definition 3b: Rust types with pinning.**  Extend definition 3a with a new axiom:
 251
 252 > {:type="a" start="2"}
 253 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:
 254 ```
 255 forall |ptr, bytes| (ptr.points_to_owned(bytes) && T.own(bytes)) -> T.pin(ptr)
 256 ```
 257
 258 `PinBox::new` can now be easily implemented using `Box::new` and `PinBox<T>::from`.
 259
 260 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>`.
 261 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)`:
 262 ```
 263 borrowed('a, exists |bytes| ptr.points_to_owned(bytes) && PinBox<T>.own(bytes))
 264 ```
 265 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).
 266 This exactly matches our return type, so we're good!
 267
 268 Finally, let us look at `impl<T> Deref for PinBox<T>`.
 269 This is where the shared typestate of `PinBox` becomes relevant:
 270 This `impl` turns a `&'a PinBox<T>` into a `&'a T` by dereferencing it once.
 271 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:
 272
 273 > **Definition 3c: Rust types with pinning.**  Extend definition 3b with a new axiom:
 274
 275 > {:type="a" start="3"}
 276 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:
 277 ```
 278 forall |'a, ptr| borrowed('a, T.pin(ptr)) -> T.shr('a, ptr)
 279 ```
 280
 281 > This is the final definition of Rust types with pinning.
 282
 283 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.
 284
 285 Next, we define the shared typestate of `PinBox<T>`:
 286
 287 > **Definition 5: `PinBox<T>.shr`.**
 288 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)`.
 289 In other words, a shared `PinBox<T>` is just a read-only pointer to a shared `T`:
 290 ```
 291 PinBox<T>.shr('a, ptr) := exists |inner_ptr|
 292   ptr.points_to_read_only('a, inner_ptr) && T.shr('a, inner_ptr)
 293 ```
 294 This requires a way to talk about memory that is read-only for the duration of some lifetime.
 295 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.
 296 We then define a convenient variant based on higher-level memory representations as usual:
 297 ```
 298 ptr.points_to_read_only('a: Lifetime, data: U) where List<Bytes>: TryInto<U> :=
 299   exists |bytes| bytes.try_into() == Ok(data) && ptr.points_to_read_only_bytes('a, bytes)
 300 ```
 301
 302 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.
 303 With this definition of `PinBox<T>.shr`, justifying the `impl<T> Deref for PinBox<T>` is fairly straight-forward.
 304
 305 This completes the methods available on `PinBox`.
 306 Verifying `Pin` follows the same approach, so I am not going to spell that out here.
 307
 308 ## Unpin
 309
 310 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>`.
 311 Formally speaking:
 312
 313 > **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.
 314 Formally:
 315 ```
 316 forall |ptr| T.pin(ptr) -> (exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes))
 317 ```
 318
 319 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.
 320
 321 Clearly, `SelfReferential` is *not* `Unpin`, and the example code above makes that explicit with an `impl !Unpin`.
 322 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.
 323
 324 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>`.
 325 This justifies all the methods with an `Unpin` bound.
 326
 327 ## Pin is a Local Extension
 328
 329 One advantage of this proposal is that it is *local*:
 330 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.
 331 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)`:
 332 ```
 333 T.pin(ptr) := exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes)
 334 ```
 335 This satisfies the additional axioms (b) and (c) connecting the pinned typestate to the others, and it also satisfies `Unpin`.
 336 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.
 337
 338 ## Conclusion
 339
 340 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`.
 341 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.
 342 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.
 343
 344 Thanks for reading!
 345 I am looking forward to hearing your [comments](https://internals.rust-lang.org/t/sharing-for-a-lifetime/7236).
 346 In particular, I am curious if the made-up syntax for making the typestate invariants more precise was helpful.