X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/e2f3b9bae5d87f9d9568ef9171bef77b83d15c78..384c25cb06b3c99d90bb4ef417082a75792dee05:/personal/_posts/2018-04-10-safe-intrusive-collections-with-pinning.md?ds=inline 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 37da65c..d786731 100644 --- 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 --- -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. @@ -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! -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. @@ -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 -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 @@ -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>`. 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). -However, it also means `&Pin` 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` 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 %} @@ -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. -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` 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.