add Eduard Martin Preis

[web.git] / ralf / _posts / 2018-04-10-safe-intrusive-collections-with-pinning.md

diff --git a/ralf/_posts/2018-04-10-safe-intrusive-collections-with-pinning.md b/ralf/_posts/2018-04-10-safe-intrusive-collections-with-pinning.md
index 37da65c29587937af3d87adee74655b5a10e39de..db706aefb07fab79d341e08795f92e28330d6409 100644 (file)
--- a/ralf/_posts/2018-04-10-safe-intrusive-collections-with-pinning.md
+++ b/ralf/_posts/2018-04-10-safe-intrusive-collections-with-pinning.md
@@ -4,7 +4,7 @@ categories: research rust
 forum: https://internals.rust-lang.org/t/safe-intrusive-collections-with-pinning/7281
 ---
 
 forum: https://internals.rust-lang.org/t/safe-intrusive-collections-with-pinning/7281
 ---
 

-In my [last post]({{ site.baseurl }}{% post_url 2018-04-05-a-formal-look-at-pinning %}), I talked about the new ["pinned references"](https://github.com/rust-lang/rfcs/blob/master/text/2349-pin.md) which guarantee that the data at the memory it points to will not, ever, be moved elsewhere.
+In my [last post]({% post_url 2018-04-05-a-formal-look-at-pinning %}), I talked about the new ["pinned references"](https://github.com/rust-lang/rfcs/blob/master/text/2349-pin.md) which guarantee that the data at the memory it points to will not, ever, be moved elsewhere.

 I explained how they enable giving a safe API to code that could previously only be exposed with `unsafe`, and how one could go about proving such a thing.
 This post is about another application of pinned references---another API whose safety relies on the pinning guarantees: Intrusive collections.
 It turns out that pinned references can *almost* be used for this, but not quite.
 I explained how they enable giving a safe API to code that could previously only be exposed with `unsafe`, and how one could go about proving such a thing.
 This post is about another application of pinned references---another API whose safety relies on the pinning guarantees: Intrusive collections.
 It turns out that pinned references can *almost* be used for this, but not quite.


@@ -141,7 +141,7 @@ This is possible despite there being no guarantee that the entry will outlive th
 Then we `drop` the entry while the collection still exists, and we can see it has vanished from the collection as well.
 
 Notice that using `Pin` in the `insert` method above is crucial: If the collection of the entry were to move around, their respective pointers would get stale!
 Then we `drop` the entry while the collection still exists, and we can see it has vanished from the collection as well.
 
 Notice that using `Pin` in the `insert` method above is crucial: If the collection of the entry were to move around, their respective pointers would get stale!

-This is fundamentally the same problem as [`SelfReferential` in my previous post]({{ site.baseurl }}{% post_url 2018-04-05-a-formal-look-at-pinning %}), and `Pin` helps.
+This is fundamentally the same problem as [`SelfReferential` in my previous post]({% post_url 2018-04-05-a-formal-look-at-pinning %}), and `Pin` helps.

 Thanks to this guarantee, and unlike in the intrusive-collections crate, `insert` can be called with entries *that do not outlive the collection*.
 With an [API for stack pinning](https://github.com/rust-lang/rfcs/blob/master/text/2349-pin.md#stack-pinning-api-potential-future-extension), we could even have put the `entry` in `main` on the stack.
 
 Thanks to this guarantee, and unlike in the intrusive-collections crate, `insert` can be called with entries *that do not outlive the collection*.
 With an [API for stack pinning](https://github.com/rust-lang/rfcs/blob/master/text/2349-pin.md#stack-pinning-api-potential-future-extension), we could even have put the `entry` in `main` on the stack.
 


@@ -179,7 +179,7 @@ fn main() {
 }
 {% endhighlight %}
 
 }
 {% endhighlight %}
 

-Now, `PinBox::deallocate` is pretty artificial, but in fact the [API for stack pinning](https://github.com/rust-lang/rfcs/blob/master/text/2349-pin.md#stack-pinning-api-potential-future-extension) that is drafted in the RFC, together with [`ManuallyDrop`](https://doc.rust-lang.org/beta/std/mem/union.ManuallyDrop.html), make it possible to obtain a `Pin<T>` to a stack-allocated `T` and subsequently pop the stack frame without calling `drop` on the `T`.
+Now, `PinBox::deallocate` is pretty artificial, but in fact the [API for stack pinning](https://github.com/rust-lang/rfcs/blob/master/text/2349-pin.md#stack-pinning-api-potential-future-extension) that is drafted in the RFC, together with [`ManuallyDrop`](https://doc.rust-lang.org/stable/std/mem/struct.ManuallyDrop.html), make it possible to obtain a `Pin<T>` to a stack-allocated `T` and subsequently pop the stack frame without calling `drop` on the `T`.

 That has the same effect as `PinBox::deallocate`: It renders our collection interface unsound.
 The concern about dropping pinned data is real.
 
 That has the same effect as `PinBox::deallocate`: It renders our collection interface unsound.
 The concern about dropping pinned data is real.
 


@@ -234,7 +234,7 @@ For now, that seems worth it; if one day we decide that pinning ought to be more
 
 ## 2 The Formal Perspective
 
 
 ## 2 The Formal Perspective
 

-In this second part of the post, we are going to try and apply the formal methodology from the [previous post]({{ site.baseurl }}{% post_url 2018-04-05-a-formal-look-at-pinning %}) to the intrusive collection example above.
+In this second part of the post, we are going to try and apply the formal methodology from the [previous post]({% post_url 2018-04-05-a-formal-look-at-pinning %}) to the intrusive collection example above.

 I am going to assume that you have read that post.
 
 ### 2.1 The Intrusive Collection Invariant
 I am going to assume that you have read that post.
 
 ### 2.1 The Intrusive Collection Invariant


@@ -266,7 +266,7 @@ Collection<T>.pin(ptr) := exists |entries: List<Pointer>|
   )
 ```
 Notice how we iterate over the elements of the list and make sure that we own whatever memory is to own there.
   )
 ```
 Notice how we iterate over the elements of the list and make sure that we own whatever memory is to own there.

-(I love how `all` [really exists for iterators](https://doc.rust-lang.org/beta/std/iter/trait.Iterator.html#method.all) so I can express quantification over lists without any hassle. :)
+(I love how `all` [really exists for iterators](https://doc.rust-lang.org/stable/std/iter/trait.Iterator.html#method.all) so I can express quantification over lists without any hassle. :)

 
 This invariant already justifies `print_all`: All the entries we are going to see there are in the list, so we have their `T.pin` at our disposal and are free to call `Debug::fmt`.
 
 
 This invariant already justifies `print_all`: All the entries we are going to see there are in the list, so we have their `T.pin` at our disposal and are free to call `Debug::fmt`.
 


@@ -400,10 +400,9 @@ Since all the mutation we perform there happens inside a `Cell`, why shouldn't w
 That's a good question!
 It seems perfectly fine to change `insert` to take `&Pin<Entry<T>>`.
 I can't come up with any counter-example.
 That's a good question!
 It seems perfectly fine to change `insert` to take `&Pin<Entry<T>>`.
 I can't come up with any counter-example.

-However, the formal model also cannot justify this variant of `insert`: As we defined previously, `Pin<'a, T>.shr` just uses `T.shr`.
-That made it easy to justify [`Pin::deref`](https://doc.rust-lang.org/nightly/std/mem/struct.Pin.html#method.deref).
-However, it also means `&Pin<T>` and `&&T` *are the same type*.
-The two invariants are equivalent.
+However, the formal model also cannot justify this variant of `insert`: Our model as defind previously defines `Pin<'a, T>.shr` in terms of `T.shr`.
+That made it easy to justify `Pin::deref`.
+However, as a consequence, `Pin<'a, T>.shr` and `(&'a T).shr` are literally the same invariant, and hence `&Pin<T>` and `&&T` *are the same type*.

 We could literally write functions transmuting between the two, and we could justify them in my model.
 Clearly, `insert` taking `entry: &&T` would be unsound as nothing stops the entry from being moved later:
 {% highlight rust %}
 We could literally write functions transmuting between the two, and we could justify them in my model.
 Clearly, `insert` taking `entry: &&T` would be unsound as nothing stops the entry from being moved later:
 {% highlight rust %}


@@ -421,7 +420,13 @@ fn main() {
 {% endhighlight %}
 This shows that the version of `insert` that takes a shared reference cannot be sound in the model.
 
 {% endhighlight %}
 This shows that the version of `insert` that takes a shared reference cannot be sound in the model.
 

-I do have an idea for how to solve this problem: Introduce a *fourth* "mode" or typestate, the "shared pinned" state, with an accompanying invariant.
+Notice that this is a consequence of a choice I made when building the model, namely the choice to define `Pin<'a, T>.shr` in terms of `T.shr`.
+This does *not* show that `&Pin<T>` and `&&T` have to be the same type given the public API and the contract they provide.
+Different choices in the model could lead to a different situation.
+The problem is, how else *could* we define `Pin<'a, T>.shr`, if we do not want to use `T.shr`?
+What *is* the invariant of a shared reference to a pinned reference?
+
+I do have an idea for how to answer this question: Introduce a *fourth* "mode" or typestate, the "shared pinned" state, with an accompanying invariant.

 However, I previously argued strongly against introducing such a fourth state, on the grounds that three typestates is already complicated enough.
 In fact, an earlier version of the `Pin` API used to have two kinds of pinned references (shared and mutable) reflecting the two distinct "shared pinned" and "(owned) pinned" typestates.
 The shared variant got subsequently removed, and I feel somewhat guilty about that now because I strongly pushed for it.
 However, I previously argued strongly against introducing such a fourth state, on the grounds that three typestates is already complicated enough.
 In fact, an earlier version of the `Pin` API used to have two kinds of pinned references (shared and mutable) reflecting the two distinct "shared pinned" and "(owned) pinned" typestates.
 The shared variant got subsequently removed, and I feel somewhat guilty about that now because I strongly pushed for it.


@@ -445,7 +450,7 @@ I feel bad about that.  Can we still fix this before everything gets stabilized?
 Others [have](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-373206171) [argued](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-378555691) for a shared pinned reference after it got removed from the API, and I argued against them as I did not understand how it could be useful.
 Thanks for not being convinced by me!
 
 Others [have](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-373206171) [argued](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-378555691) for a shared pinned reference after it got removed from the API, and I argued against them as I did not understand how it could be useful.
 Thanks for not being convinced by me!
 

-However, there is one strange aspect to this "shared pinned" typestate: Due to [`Pin::deref`](https://doc.rust-lang.org/beta/std/mem/struct.Pin.html#method.deref), we can turn a "shared pinned" reference into a shared reference.
+However, there is one strange aspect to this "shared pinned" typestate: Due to `Pin::deref`, we can turn a "shared pinned" reference into a shared reference.

 We can go from `&Pin<T>` to `&&T`.
 In other words, the shared pinned typestate invariant must *imply* the invariant for the (general, unpinned) shared typestate.
 The reason for `Pin::deref` to exist is mostly a rustc implementation detail [related to using `Pin<Self>` as the type of `self`](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-372475895), but this detail has some significant consequences: Even with a separate shared pinned typestate, we can still not define `RefCell` in a way that a pinned `RefCell` pins its contents.
 We can go from `&Pin<T>` to `&&T`.
 In other words, the shared pinned typestate invariant must *imply* the invariant for the (general, unpinned) shared typestate.
 The reason for `Pin::deref` to exist is mostly a rustc implementation detail [related to using `Pin<Self>` as the type of `self`](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-372475895), but this detail has some significant consequences: Even with a separate shared pinned typestate, we can still not define `RefCell` in a way that a pinned `RefCell` pins its contents.