add MoSeL paper

[web.git] / 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 73073dec2e1aff3d4224c9699c0323a2d39daa11..2e72c2a6a73f3a7ef004bf939872c642257a4fb5 100644 (file)
--- 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>`.