X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/e770d4e05702bb0cbff0f2d0cb78f09cf75a4b28..1014facc01a7f23163450af7c1dd57bbd09ce543:/personal/_posts/2018-04-05-a-formal-look-at-pinning.md

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 0093a21..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
@@ -47,16 +47,18 @@ Data is only pinned after a `Pin<T>` 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<T>` and `PinBox<T>`.
@@ -335,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.