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


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


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