X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/f1760068a46b81f96f44eb008601a4b8db9f2a6b..e53cc189578e746470272a98cefaef484fc07518:/personal/_posts/2018-04-05-a-formal-look-at-pinning.md?ds=sidebyside diff --git a/personal/_posts/2018-04-05-a-formal-look-at-pinning.md b/personal/_posts/2018-04-05-a-formal-look-at-pinning.md index 4aed608..2e72c2a 100644 --- a/personal/_posts/2018-04-05-a-formal-look-at-pinning.md +++ b/personal/_posts/2018-04-05-a-formal-look-at-pinning.md @@ -4,10 +4,10 @@ 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. +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. The purpose of these references is to express that the data at the memory it points to will not, ever, be moved elsewhere. -Others have [written](https://boats.gitlab.io/blog/post/2018-03-20-async-vi/) about why this is important in the context of async IO. -The purpose of this post is to 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. +@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/). +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. @@ -47,35 +47,37 @@ Data is only pinned after a `Pin` pointing to it has been created; it can be 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. I will not repeat that here but only show one example of how to use `Pin` references and exploit their guarantees: {% highlight rust %} -#![feature(pin, arbitrary_self_types)] +#![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: Option>, + self_ref: *const i32, } +impl !Unpin for SelfReferential {} impl SelfReferential { - fn new() -> Self { - SelfReferential { data: 42, self_ref: None } + fn new() -> SelfReferential { + SelfReferential { data: 42, self_ref: ptr::null() } } - fn init(mut self: Pin) { - unsafe { - let this = Pin::get_mut(&mut self); - // Set up self_ref to point to this.data - this.self_ref = ptr::NonNull::new(&mut this.data as *mut _); - } + fn init(mut self: Pin) { + let this : &mut SelfReferential = unsafe { Pin::get_mut(&mut self) }; + // Set up self_ref to point to this.data. + this.self_ref = &mut this.data as *const i32; } - - fn read_ref(mut self: Pin) -> Option { - unsafe { - let this = Pin::get_mut(&mut self); - // Dereference self_ref if it is set - this.self_ref.map(|self_ref| *self_ref.as_ptr()) + + fn read_ref(mut self: Pin) -> Option { + let this : &mut SelfReferential = unsafe { Pin::get_mut(&mut self) }; + // Dereference self_ref if it is non-NULL. + if this.self_ref == ptr::null() { + None + } else { + Some(unsafe { *this.self_ref }) } } } @@ -86,10 +88,12 @@ fn main() { println!("{:?}", s.as_pin().read_ref()); // prints Some(42) } {% endhighlight %} -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`). +**Update:** Previously, the example code used `Option>`. 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 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 @@ -121,29 +125,20 @@ forall |'a, ptr| 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. +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. -We also need some way to talk about ownership and contents of memory: -I will write `ptr.points_to_owned_bytes(bytes)` (where `ptr: Pointer` and `bytes: List`) 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 `ptr.points_to_owned(42i32)`. -We can define a suitable `points_to_owned` as -``` -ptr.points_to_owned(data: U) where List: TryInto := - 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`, this is just the same as `ptr.points_to_owned_bytes`. +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`) 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 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** +**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(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. +`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: @@ -154,18 +149,27 @@ Formally: ``` Box.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)) ``` -It turns out that using `try_into` like we do above is actually a common pattern. -We usually do not want to talk directly about the `List` but convert them to some higher-level representation first. +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` being implemented for `List`. +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` 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: TryInto`, 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.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)) ``` @@ -177,9 +181,9 @@ exists |data: U| bytes.try_into() == Ok(data) && T.own(data) ## Extending Types to Verify `SelfReferential` -What would it take to *prove* that `SelfReferential` can be used by arbitrary safe code? +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` it set to `Some(data_ptr)`, then `data_ptr` is the address of `self.data`. +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. @@ -193,20 +197,30 @@ We will add a new, *third* typestate on top of the existing owned and shared typ 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)`. -(In terms of memory layout, `SelfReferential` is the same as a pair of `i32` and `Option>`.) -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)` 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: Option>| +SelfReferential.pin(ptr) := exists |data: i32, self_ref: *const i32| ptr.points_to_owned((data, self_ref)) && - match self_ref { Some(data_ptr) => data_ptr.as_ptr() == ptr.offset(0), None => True } + (self_ref == ptr::null() || self_ref == ptr.offset(0)) ``` -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`). -(I am of course glossing over plenty of details here, like handling of padding, but those details are not relevant right now. +(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 the closure in `self_ref.map` runs, we are in the `Some` case of the `match` so the deref of the pointer obtained from `self_ref` is fine. +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`, 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` as follows: +``` +ptr.points_to_owned(data: U) where List: TryInto := + 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 @@ -223,6 +237,8 @@ A list of bytes makes a valid `PinBox` if those bytes form a pointer `ptr` su For `Pin<'a, T>`, `ptr` is valid if we have borrowed `T.pin(ptr)` for lifetime `'a`. ``` PinBox.own(ptr) := T.pin(ptr) +``` +``` Pin<'a, T>.own(ptr) := borrowed('a, T.pin(ptr)) ``` @@ -302,7 +318,7 @@ forall |ptr| T.pin(ptr) -> (exists |bytes| ptr.points_to_owned(bytes) && T.own(b 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`. +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` and `PinBox`. @@ -321,7 +337,7 @@ The latter is crucial, because it means we can automatically derive `Unpin` inst ## Conclusion -We have seen how the new `Pin` type can be used to give safe APIs to types like `SelfReferential`, and how we can (semi-)formally argue for the correctness of `SelfReferential` and the methods on `Pin` and `PinBox`. +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.