X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/021466ba05c160cfa526c7946a14c6ac4763b480..384c25cb06b3c99d90bb4ef417082a75792dee05:/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 a3f0cca..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