add Coq typeclass index problem draft

[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 0093a21525daa8672610ba596b874441120fae15..edaf6c64632381a5783fec2eec4dfb3a125660e6 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
@@ -15,7 +15,7 @@ But before we get started, I have to lay down some basics.
 
 ## Rust types: Recap
 
 
 ## Rust types: Recap
 

-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.
+I have discussed my model of Rust types [in a previous post]({% 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.

 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.
 @cramertj suggested to use "typestate" as terminology here, and I agree that this makes sense.
 
 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.
 @cramertj suggested to use "typestate" as terminology here, and I agree that this makes sense.
 


@@ -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 %}
 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::ptr;
 use std::mem::Pin;
 use std::boxed::PinBox;

+use std::marker::Unpin;

 
 struct SelfReferential {
     data: i32,
     self_ref: *const i32,
 }
 
 struct SelfReferential {
     data: i32,
     self_ref: *const i32,
 }

+impl !Unpin for SelfReferential {}

 
 impl SelfReferential {
     fn new() -> SelfReferential {
 
 impl SelfReferential {
     fn new() -> SelfReferential {


@@ -109,7 +111,7 @@ In contrast, converting `Box<T>` to `PinBox<T>` is fine because this *consumes*
 `Pin` lets us give a type to `SelfReferantial` that makes it safe to use.
 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).
 In the following, I will explain how one can prove that our claim of safe encapsulation actually holds true.
 `Pin` lets us give a type to `SelfReferantial` that makes it safe to use.
 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).
 In the following, I will explain how one can prove that our claim of safe encapsulation actually holds true.

-This is building on the framework that we developed for the [RustBelt paper]({{ site.baseurl }}{% post_url 2017-07-08-rustbelt %}).
+This is building on the framework that we developed for the [RustBelt paper]({% post_url 2017-07-08-rustbelt %}).

 
 ## Formal Notation
 
 
 ## Formal Notation
 


@@ -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.
 
 
 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>`.
 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
 
 
 ## 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.
 
 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.