From: Ralf Jung Date: Tue, 17 Apr 2018 08:00:28 +0000 (+0200) Subject: impl !Unpin X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/e47f8237c7a0da44c550230ddbe68a854b53f5ca?hp=60a3b9582df4cce2138281bc8749dcd362d69b8e impl !Unpin --- diff --git a/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md b/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md index 73073de..2e72c2a 100644 --- a/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md +++ b/ralf/_posts/2018-04-05-a-formal-look-at-pinning.md @@ -47,16 +47,18 @@ 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: *const i32, } +impl !Unpin for SelfReferential {} impl SelfReferential { fn new() -> SelfReferential { @@ -316,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`.