add Coq typeclass index problem draft

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

diff --git a/personal/_posts/2018-04-10-safe-intrusive-collections-with-pinning.md b/personal/_posts/2018-04-10-safe-intrusive-collections-with-pinning.md
index 362a4e3dc8e27d5d8403f005952de3f9122341fc..d786731065602cbfddb0d5f27724e449127613e8 100644 (file)
--- a/personal/_posts/2018-04-10-safe-intrusive-collections-with-pinning.md
+++ b/personal/_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.


@@ -20,7 +20,7 @@ This builds on the formal notation I introduced in my last post.
 
 Finally, I will discuss a variant of our "running example" intrusive collection that combines shared references and pinning.
 It turns out this variant is actually incompatible with the formal model from the last post, but the model can be extended to fix this.
 
 Finally, I will discuss a variant of our "running example" intrusive collection that combines shared references and pinning.
 It turns out this variant is actually incompatible with the formal model from the last post, but the model can be extended to fix this.

-Hiwever, this extended model will actually call for a change to the `Pin` API (or rather, for a revert to an earlier version).
+However, this extended model will actually call for a change to the `Pin` API (or rather, for a revert to an earlier version).

 
 (Btw, I'm sorry for this blog post being *even longer* than the previous.  I guess I am just enjoying that there is no page limit (like there is in papers) when writing blog posts, so I can just ramble as much as I like.)
 
 
 (Btw, I'm sorry for this blog post being *even longer* than the previous.  I guess I am just enjoying that there is no page limit (like there is in papers) when writing blog posts, so I can just ramble as much as I like.)
 


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


@@ -220,13 +220,13 @@ What would *not* be sound is adding a way to obtain a `Pin` reference *into* a `
 In the formal part of this post, we will see that we can express the new guarantee without resorting to "linear reasoning", which is reasoning that forbids resources to not get used.
 (Linear reasoning is typically used to prove properties like memory-leak-freedom.)
 
 In the formal part of this post, we will see that we can express the new guarantee without resorting to "linear reasoning", which is reasoning that forbids resources to not get used.
 (Linear reasoning is typically used to prove properties like memory-leak-freedom.)
 

-Okay, so maybe this is much weaker than leek-freedom and we have some good reasons to want such a limited `drop`-guarantee, but why should this be coupled together with `Pin`?
+Okay, so maybe this is much weaker than leak-freedom and we have some good reasons to want such a limited `drop`-guarantee, but why should this be coupled together with `Pin`?

 Pinning and calling `drop` are entirely orthogonal concerns!
 Well, this is certainly true for general leak-freedom.
 However, the guarantee we are after here is that `drop` will be called *if this memory ever gets deallocated*.
 So, the guarantee is tied to a particular spot in memory---a concept that only makes sense if data is pinned to begin with!
 While `Pin` without the `drop`-guarantee makes sense (and is useful, e.g., for [async IO](https://boats.gitlab.io/blog/post/2018-03-20-async-vi/)), the `drop`-guarantee really only makes sense for pinned data.
 Pinning and calling `drop` are entirely orthogonal concerns!
 Well, this is certainly true for general leak-freedom.
 However, the guarantee we are after here is that `drop` will be called *if this memory ever gets deallocated*.
 So, the guarantee is tied to a particular spot in memory---a concept that only makes sense if data is pinned to begin with!
 While `Pin` without the `drop`-guarantee makes sense (and is useful, e.g., for [async IO](https://boats.gitlab.io/blog/post/2018-03-20-async-vi/)), the `drop`-guarantee really only makes sense for pinned data.

-Given that async IO is not bothered by this additional guarantee (it doesn't want to do anything that would violate the guarnatee), it seems preferable to have just one notion of pinned data as opposed to two (one where `drop` will be called, and one where it may not be called).
+Given that async IO is not bothered by this additional guarantee (it doesn't want to do anything that would violate the guarantee), it seems preferable to have just one notion of pinned data as opposed to two (one where `drop` will be called, and one where it may not be called).

 In fact, as we will see in the formal part, the way I have set up formal reasoning about pinning last time, we would have to do *extra work* to *not* get this guarantee!
 
 The only remaining downside is that the more ergonomic stack pinning API [proposed in the RFC](https://github.com/rust-lang/rfcs/blob/master/text/2349-pin.md#stack-pinning-api-potential-future-extension) becomes unsound, and we have to use a less ergonomic [closure-based API instead](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-374702107).
 In fact, as we will see in the formal part, the way I have set up formal reasoning about pinning last time, we would have to do *extra work* to *not* get this guarantee!
 
 The only remaining downside is that the more ergonomic stack pinning API [proposed in the RFC](https://github.com/rust-lang/rfcs/blob/master/text/2349-pin.md#stack-pinning-api-potential-future-extension) becomes unsound, and we have to use a less ergonomic [closure-based API instead](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-374702107).


@@ -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/beta/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`.
 


@@ -350,7 +350,7 @@ We are just concerned with *safety* here: When memory is pinned, it is only safe
 One important observation is that if we did *not* remove the entry from the collection, we would be unable to satisfy the postcondition!
 This matches the fact that our entire collection would be unsound if we removed the `Entry::drop`.
 In other words, if we do *not* implement `Drop`, this actually incurs a proof obligation!
 One important observation is that if we did *not* remove the entry from the collection, we would be unable to satisfy the postcondition!
 This matches the fact that our entire collection would be unsound if we removed the `Entry::drop`.
 In other words, if we do *not* implement `Drop`, this actually incurs a proof obligation!

-We have to show that *not doing anything* can turn the precondition `T.pin(ptr)` into the postconditon `exists |bytes| ptr.points_to_owned(bytes) && bytes.len() == mem::size_of<T>()`.
+We have to show that *not doing anything* can turn the precondition `T.pin(ptr)` into the postcondition `exists |bytes| ptr.points_to_owned(bytes) && bytes.len() == mem::size_of<T>()`.

 This is the part that would go wrong if we were to remove `Entry::drop`.
 It seems rather funny that *not* implementing a trait incurs a proof obligation, but there's also nothing fundamentally wrong with that idea.
 
 This is the part that would go wrong if we were to remove `Entry::drop`.
 It seems rather funny that *not* implementing a trait incurs a proof obligation, but there's also nothing fundamentally wrong with that idea.
 


@@ -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`.
+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`](https://doc.rust-lang.org/nightly/std/mem/struct.Pin.html#method.deref).
 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, 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.


@@ -440,6 +445,7 @@ I hope we do not end up in a situation where `insert` with a shared reference is
 That just seems like the worst of both worlds.
 
 However, now we already have a [version of the futures crate](https://aturon.github.io/2018/04/06/futures2/) using the revised `Pin`, so I don't know if changing it again is realistic. :/
 That just seems like the worst of both worlds.
 
 However, now we already have a [version of the futures crate](https://aturon.github.io/2018/04/06/futures2/) using the revised `Pin`, so I don't know if changing it again is realistic. :/

+(**Update:** Seems like [there may be breaking changes in future future versions anyway](https://www.reddit.com/r/rust/comments/8ac85w/futures_02_is_here/dwxkhvl/), so maybe the ship has not yet sailed after all. **/Update**)

 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!
 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!


@@ -453,6 +459,8 @@ Removing `Pin::deref` (or restricting it to types that implement `Unpin`) would
 I spelled out the details [in the RFC issue](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-372109981).
 So, if we want to declare that shared pinning is a typestate in its own right---which overall seems desirable---do we want it to be restricted like this due to an implementation detail of arbitrary self types?
 
 I spelled out the details [in the RFC issue](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-372109981).
 So, if we want to declare that shared pinning is a typestate in its own right---which overall seems desirable---do we want it to be restricted like this due to an implementation detail of arbitrary self types?
 

+**Update:** @Diggsey [points out](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-379230538) that we can still have a `PinRefCell` with a method like `fn get_pin(self: Pin<PinRefCell<T>>) -> Pin<T>`, as long as the `PinRefCell` never gives out mutable references. So it turns out that combining interior mutability and pinning should work fine.  Later, @glaebhoerl suggested we can even [combine `RefCell` and `PinRefCell` into one type if we dynamically track the pinning state](https://internals.rust-lang.org/t/safe-intrusive-collections-with-pinning/7281/11?u=ralfjung).  **/Update**
+

 ## 4 Conclusion
 
 Leaving aside the last part about shared pinning, I am really excited how all of this fits together so nicely.
 ## 4 Conclusion
 
 Leaving aside the last part about shared pinning, I am really excited how all of this fits together so nicely.


@@ -461,7 +469,6 @@ I am happy to learn that I was wrong!
 I am impressed by the creativity that went into coming up with these APIs, and looking forward to analyzing more of them in the future.
 
 The situation around shared pinning is still open, and it seems we need to have a discussion about what model we ultimately want to adopt---which code we ultimately want to be legal---and whether we want to change the `Pin` types before stabilization.
 I am impressed by the creativity that went into coming up with these APIs, and looking forward to analyzing more of them in the future.
 
 The situation around shared pinning is still open, and it seems we need to have a discussion about what model we ultimately want to adopt---which code we ultimately want to be legal---and whether we want to change the `Pin` types before stabilization.

-Unfortunately I am four days late in my race against the [first significant user of this API](https://aturon.github.io/2018/04/06/futures2/).

 
 Anyway, as usual, please [let me know what you think](https://internals.rust-lang.org/t/safe-intrusive-collections-with-pinning/7281)!
 
 
 Anyway, as usual, please [let me know what you think](https://internals.rust-lang.org/t/safe-intrusive-collections-with-pinning/7281)!