3074503f7474a38ee77db95df5f2ed3edbe70150
[web.git] / personal / _drafts / safe-intrusive-collections-with-pinning.md
1 ---
2 title: "Safe Intrusive Collections with Pinning"
3 categories: rust
4 ---
5
6 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.
7 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.
8 This post is about another application of pinned references---another API whose safety relies on the pinning guarantees: Intrusive collections.
9 It turns out that pinned references can *almost* be used for this, but not quite.
10 However, this can be fixed by extending the guarantees provided by pinned references, as suggested by @cramertj.
11
12 <!-- MORE -->
13
14 The first part is going to explain how intrusive collections could benefit from `Pin`, were we to accept that additional guarantee.
15 This part assumes some familiarity with the `Pin` API, but not with the formal model I introduced previously.
16
17 In the second part, I am going to briefly sketch a formal perspective on intrusive collections and the extended pinning guarantees.
18 This builds on the formal notation I introduced in my last post.
19
20 Finally, I will discuss a variant of our "running example" intrusive collection that this model can *not* handle, and how the model could be extended.
21 This extended model will actually call for a change to the `Pin` API (or rather, for a revert to an earlier version).
22
23 (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.)
24
25 ## 1 Safe Intrusive Collections
26
27 Intrusive collections typically are linked data structures that embed the links in the data they contain.
28 In the words of the [intrusive-collections crate](https://crates.io/crates/intrusive-collections):
29 > The main difference between an intrusive collection and a normal one is that while normal collections allocate memory behind your back to keep track of a set of *values*, intrusive collections never allocate memory themselves and instead keep track of a set of *objects*. Such collections are called intrusive because they requires explicit support in objects to allow them to be inserted into a collection.
30
31 To make this work safely, we better make sure that the "objects" (allocated and managed by the user of the collection) are not moved around or deallocated while they are part of the collection.
32 The intrusive-collections crate realizes this by taking ownership of the objects.
33 The crate also offers a [more advanced API](https://docs.rs/intrusive-collections/0.7.0/intrusive_collections/#scoped-collections) that works with borrowed data, but in this case the objects must outlive the entire collection.
34 This means we cannot add short-lived objects, e.g. stack-allocated objects, to a collection that was created further up the call chain.
35 How could we go about lifting that restriction?
36
37 ### 1.1 An Example Collection
38
39 To get more concrete, consider the following example ([originally proposed by @cramertj](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-372432435)).
40 This is not *really* an intrusive collections, but it has all the same properties and problems: The collection involves pointers to elements allocated by the user, and hence risks dangling pointers if they get moved or deallocated.
41 (If I were to make this a proper intrusive linked list, the code would be twice as long and I would most definitely get the re-linking wrong.
42 I will leave [writing linked lists](http://cglab.ca/~abeinges/blah/too-many-lists/book/) to others.)
43 {% highlight rust %}
44 #![feature(pin, arbitrary_self_types, optin_builtin_traits)]
45
46 use std::cell::{Cell, RefCell};
47 use std::mem::Pin;
48 use std::boxed::PinBox;
49 use std::marker::Unpin;
50
51 struct Collection<T> {
52     objects: RefCell<Vec<*const Entry<T>>>,
53 }
54 impl<T> !Unpin for Collection<T> {}
55
56 struct Entry<T> {
57     x: T,
58     // set to Some if we are part of some collection
59     collection: Cell<Option<*const Collection<T>>>,
60 }
61 impl<T> !Unpin for Entry<T> {}
62
63 impl<T> Collection<T> {
64     fn new() -> Self {
65         Collection { objects: RefCell::new(Vec::new()) }
66     }
67
68     // Add the entry to the collection
69     fn insert(mut self: Pin<Self>, entry: Pin<Entry<T>>) {
70         if entry.collection.get().is_some() {
71             panic!("Can't insert the same object into multiple collections");
72         }
73         // Pointer from collection to entry
74         let this : &mut Self = unsafe { Pin::get_mut(&mut self) };
75         this.objects.borrow_mut().push(&*entry as *const _);
76         // Pointer from entry to collection
77         entry.collection.set(Some(this as *const _));
78     }
79     
80     // Show all entries of the collection
81     fn print_all(self: Pin<Self>)
82     where T: ::std::fmt::Debug
83     {
84         print!("[");
85         for entry in self.objects.borrow().iter() {
86             let entry : &Entry<T> = unsafe { &**entry };
87             print!(" {:?},", entry.x);
88         }
89         println!(" ]");
90     }
91 }
92
93 impl<T> Drop for Collection<T> {
94     fn drop(&mut self) {
95         // Go through the entries to remove pointers to collection
96         for entry in self.objects.borrow().iter() {
97             let entry : &Entry<T> = unsafe { &**entry };
98             entry.collection.set(None);
99         }
100     }
101 }
102
103 impl<T> Entry<T> {
104     fn new(x: T) -> Self {
105         Entry { x, collection: Cell::new(None) }
106     }
107 }
108
109 impl<T> Drop for Entry<T> {
110     fn drop(&mut self) {
111         // Go through collection to remove this entry
112         if let Some(collection) = self.collection.get() {
113             let collection : &Collection<T> = unsafe { &*collection };
114             collection.objects.borrow_mut().retain(|ptr| *ptr != self as *const _);
115         }
116     }
117 }
118
119 fn main() {
120     let mut collection = PinBox::new(Collection::new());
121     let mut entry = PinBox::new(Entry::new(42));
122     collection.as_pin().insert(entry.as_pin());
123     collection.as_pin().print_all(); // Prints "[ 42, ]"
124     drop(entry); // Dropping the entry removes it
125     collection.as_pin().print_all(); // Prints "[ ]"
126 }
127 {% endhighlight %}
128 This is lots of code.
129 The high-level picture is as follows:
130 The collection is represented by a `Vec` of raw pointers pointing to the entries.
131 Every entry has a "parent" pointer `self.collection` back to the main collection.
132 Inserting an entry into a collection involves adding it to the `Vec` and setting the collection pointer of the entry.
133 When an entry is dropped, if it is in a collection, it gets removed from the `Vec`.
134 When the collection is dropped, all the entries have their collection pointer reset to `None`.
135
136 The example code in `main` demonstrates how the collection could be used: First we add an entry containing `42` to the collection.
137 This is possible despite there being no guarantee that the entry will outlive the collection.
138 `print_all` shows that it is there.
139 Then we `drop` the entry while the collection still exists, and we can see it has vanished from the collection as well.
140
141 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!
142 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.
143 Thanks to this guarantee, and unlike in the intrusive-collections crate, `insert` can be called with entries *that do not outlive the collection*.
144 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.
145
146 ### 1.2 Pinning Is Not Enough
147
148 However, it turns out pinning as described so far is not enough to guarantee safety.
149 Imagine we added the following method to `PinBox`:
150 {% highlight rust %}
151 fn box_deallocate<T>(x: Box<T>) {
152   let content = *x; // move out of the box
153   mem::forget(content); // do not call drop
154   // Implicitly deallocate the box
155 }
156
157 impl<T> PinBox<T> {
158   // Deallocate the box without calling drop
159   fn deallocate(self) {
160     box_deallocate(self.inner)
161   }
162 }
163 {% endhighlight %}
164 `box_deallocate` is obviously safe on `Box` (we do not use any unsafe code).
165 Moreover, from what I said so far, it is also safe to add to `PinBox`: While, technically, the data *does* get moved inside `box_deallocate`, that's just a NOP.
166 We essentially perform a `memcpy` (the move in `box_deallocate`) followed by a `mem::forget`, so nothing really happens aside from calling `free` on the `Box` itself.
167
168 Why is this a problem?  Well, we can now add an entry to a collection and then *deallocate the entry without calling `drop`*.
169 This leads to a dangling pointer inside the collection, which is obviously bad:
170 {% highlight rust %}
171 fn main() {
172     let mut collection = PinBox::new(Collection::new());
173     let mut entry = PinBox::new(Entry::new(42));
174     collection.as_pin().insert(entry.as_pin()); // Register entry in collection
175     entry.deallocate(); // Now the collection still points to the entry
176     collection.as_pin().print_all(); // And now everything explodes
177 }
178 {% endhighlight %}
179
180 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`.
181 That has the same effect as `PinBox::deallocate`: It renders our collection interface unsound.
182 The concern about dropping pinned data is real.
183
184
185 ### 1.3 Requiring Drop To Be Run
186
187 @cramertj has [suggested](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-374702107) to fix this situation by adding a new guarantee to `Pin`: *If the memory a `Pin<T>` points to is ever deallocated or otherwise invalidated, `drop` has been called on it*.
188 This just changes the way we have to think about pinned data, but does not affect the API at all.
189
190 Combining that with the guarantee about moving, we can summarize `Pin` as follows:
191
192 > Given a `Pin<'a, T>`, the data it points to will remain at the given location until it is dropped.  In particular, if it is never dropped, it will remain at the given location forever.
193
194 Under our new rules, `PinBox::deallocate` is bogus, and our collection works again.
195
196 And not just our artificial little example collection would benefit from this guarantee.
197 A proper intrusive collection would have the same problem: When an entry in an intrusive doubly-linked list gets deallocated, we better make sure that we patch the pointers from the neighboring elements or else they will soon be dangling.
198 Moreover, this has applications not just for container data structures but also for GC integration: When a stack-allocated root has been registered with the GC, we have to make sure it gets deregistered before the stack frame pops.
199 In fact, the trick of using `ManuallyDrop` to cause havoc has originally been [discovered in the context of GC integration](https://internals.rust-lang.org/t/rust-1-20-caused-pinning-to-become-incorrect/6695).
200 If `Pin` obtains the guarantee described above, a GC API can just take something along the lines of `Pin<GcRoot<T>>`, relying on the fact that `GcRoot::drop` will get called before this memory gets deallocated.
201
202 ### 1.4 Some Common Objections
203
204 I hope I convinced you that it is desirable to guarantee that `drop` is run on pinned references.
205 Before we come to the formal part of this post, let me go over some possible objections to this extended guarantee.
206 In fact, I have been opposed to it initially myself, and went to the [Berlin All-Hands](https://blog.rust-lang.org/2018/04/06/all-hands.html) arguing against it, but @cramertj convinced me otherwise.
207 So I will just reiterate my own objections and how I feel about them now.
208
209 The first objection is: Haven't we had this discussion already?
210 [Leakpocalypse](http://cglab.ca/~abeinges/blah/everyone-poops/) happened back in 2015, and ever since then everyone knows that in Rust, you can leak memory, period.
211 However, even if we accept this proposal *leaking pinned data is still allowed*!
212 The guarantee says that *if memory gets deallocated or otherwise invalidated*, we will call `drop`.
213 So, calling `mem::forget` on a `PinBox` is fine.
214 And indeed, that's fine for our collection as well---the entry will just stay in the collection, but the pointers to it will also remain valid.
215 So, this proposal does *not* backpedal on memory leak guarantees in Rust.
216 Both `mem::forget` and `ManaullyDrop` remain sound.
217 What would *not* be sound is adding a way to obtain a `Pin` reference *into* a `ManuallyDrop`.
218 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.
219 (Linear reasoning is typically used to prove properties like memory-leak-freedom.)
220
221 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`?
222 Pinning and calling `drop` are entirely orthogonal concerns!
223 Well, this is certainly true for general leak-freedom.
224 However, the guarantee we are after here is that `drop` will be called *if this memory ever gets deallocated*.
225 So, the guarantee is tied to a particular spot in memory---a concept that only makes sense if data is pinned to begin with!
226 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.
227 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).
228 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!
229
230 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).
231 For now, that seems worth it; if one day we decide that pinning ought to be more ergonomic, we could have a built-in type of `&pin` references with ergonomic stack pinning enforced by the compiler.
232
233 ## 2 The Formal Perspective
234
235 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.
236 I am going to assume that you have read that post.
237
238 ### 2.1 The Intrusive Collection Invariant
239
240 Remember that, in my model, every type comes with three separate invariants, each matching a "mode" or "typestate" the type can be in: `T.own`, `T.shr`, and `T.pin`.
241 The key point we are going to exploit here is that `T.pin` is a predicate on *pointers*, and it is the job of the type `T` to say how the memory behind that pointer is managed.
242 In contrast, `T.own` is a predicate on *lists of bytes*, and whoever holds an instance of a type will typically assume something along the lines of: I own some memory containing some bytes, and those bytes form a valid `T`. Formally:
243 ```
244 exists |bytes|, ptr.points_to_owned(bytes) && T.own(bytes)
245 ```
246 Given such an assumption, we are free to just forget the `T.own` part, grab ownership of the memory, and use it for our purposes.
247 We could even deallocate it.
248 In fact, this is exactly what happens in the `box_deallocate` function I wrote above---and as we have seen, it is a disaster for intrusive collections.
249
250 With `T.pin`, we have more freedom to choose our invariant.
251 `T.pin` does not *have to* say that it owns the memory the pointer points to---and for `Entry`, this is exactly what we are going to do.
252
253 But let us start with `Collection`: The idea is that a pinned `Collection` is going to *own* the memory of all the entries it contains.
254 All these raw pointers in the `Vec` point to memory we own and containing an `Entry<T>`, i.e., a pair of a (pinned) `T` and a raw pointer back to the collection.[^1]
255 Actually saying this fully formally would require us to talk about the `RefCell` and the `Vec` in there, which we do not want to do, so the following is a very rough sketch:
256
257 [^1]: The fact that the inner `T` are pinned here is an arbitrary choice.  We could also make them fully owned.  This is a choice every collection has to make.  Of course, if they decide to go for pinning, they have to uphold all the pinning guarantees, including calling destructors---which, for example, [`VecDeque` does not](https://internals.rust-lang.org/t/rust-1-20-caused-pinning-to-become-incorrect/6695/12?u=ralfjung).
258
259 ```
260 Collection<T>.pin(ptr) := exists |entries: List<Pointer>|
261   ptr.points_to_owned(RefCell::new(Vec::from(entries))) &&
262   entries.all(|entry| T.pin(entry.offset_to_field(x)) &&
263     entry.offset_to_field(collection).points_to_owned(Cell::new(Some(ptr)))
264   )
265 ```
266 Notice how we iterate over the elements of the list and make sure that we own whatever memory is to own there.
267 (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. ;)
268
269 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`.
270
271 So, what will `Entry` say in its pinned invariant?
272 Essentially, there is a case distinction: If `collection` is `None`, we own the memory, otherwise all we know is that we are inside that collection.
273 ```
274 Entry<T>.pin(ptr) := exists |collection: Option<Pointer>|
275   match collection {
276     None => T.pin(ptr.offset_to_field(x)) &&
277       ptr.offset_to_field(collection).points_to_owned(Cell::new(None)),
278     Some(collection) => entry_owned_in_collection(ptr, collection)
279   }
280 ```
281 The `entry_owned_in_collection` here does not only assert that this entry is a part of that collection, it also asserts *ownership* of that membership, which means that nobody else can remove the entry from the collection.
282 This is our first example of "fictional ownership": Ownership not of part of the memory, but of some made-up resource that has no resemblance in the actual machine.
283 Fictional ownership is an extremely powerful concept---it forms the very basis of the [mathematical framework we use in RustBelt](http://iris-project.org/).
284 However, actually doing this formally is well beyond the scope of this post.[^2]
285
286 [^2]: For example, for fictional ownership to actually work, we would have to extend `Collection<T>.pin` to be set up as "the other end" of this ownership relation. With fictional ownership, there is always some invariant somewhere that ties it to "less fictional" ownership. Think of how a check is just fictional money that is "tied to" real money by the bank, and how "real" money used to be tied to some actual value, namely gold, by the central reserve. Similarly, `Collection<T>` owns the "real thing", the memory, and then ties it to the fictional `entry_owned_in_collection`.
287
288 This justifies `Entry::drop`: If we enter the `if let`, we know we are in the `Some` branch, so we will for sure find ourselves in that collection.
289 To remove ourselves, we have to give up ownership of `entry_owned_in_collection`, but in exchange we gain the `points_to_owned` and the `T.pin` for the entry which the collection now needs to longer.
290
291 This is the inverse of what happens in `Collection::insert`: After we made sure that the entry is in the `None` branch, we can take its ownership and put it into the collection.
292 In exchange, we obtain an `entry_owned_in_collection`, which can put back into the entry.
293 This means, when we return, the entry is fully valid in the `Some` branch.
294 That's crucial, because it's just a reference and hence borrowed---we have to restore all the invariants before we return!
295
296 ### 2.2 Requiring Drop To Be Run
297
298 So, how is the new `drop` guarantee we have been talking about reflected in the formal model?
299 First of all, notice that---due to the nature of `T.pin` taking a pointer, as discussed above---we can already not justify our fictional `PinBox::deallocate`.
300 The `PinBox` owns a `T.pin(ptr)`, which it is free to throw away, but it has no way to just gain access to the underlying memory covered by the pointer and deallocate it!
301 So, the question is not actually how we can enforce the guarantee, the question is how we can justify the correctness of dropping a `PinBox`.
302
303 Now, I should make clear that we are entering uncharted territory here.
304 RustBelt does *not* model `drop`.
305 So, I am going to take some guesses here, but these are purely based on my intuition and not at all backed by formal proofs.
306 My intuition has been wrong before.
307
308 With the disclaimer out of the way, let us look at `drop`.
309 First of all, `drop` is not a normal function. If we could just call it, we could write code like
310 {% highlight rust %}
311 let mut v = vec![0];
312 Vec::drop(&mut v);
313 v.push(1); // BOOM!
314 {% endhighlight %}
315 `Vec::drop` leaves the vector in a bad state, and we must not call any normal method on it again afterwards.
316 So, a correctness proof for `drop` is clearly going to be different from a correctness proof for a normal method that takes an `&mut`.
317 Before `drop`, we can assume that all the invariants of the type are satisfied; after `drop`, all we know is that the fields of the vector are themselves ready for `drop`.
318 In the case of `Vec`, none of the fields implements `Drop`, so let us focus on that special case:
319
320 {% raw %}
321 > **Definition 1: `drop`, special case where no field implements `Drop`.**
322 The `drop` function must satisfy the following specification (or contract): `T::drop(ptr)` is safe to call whenever `T.pin(ptr)` holds, and when `drop` returns, we own the memory `ptr` points to.
323
324 > We write these specifications as "Hoare triples" that consist of a precondition between double curly braces, followed by the code that is executed, followed by the postcondition in double curly braces:
325 ```
326 {{ T.pin(ptr) }}
327   T::drop(ptr)
328 {{ exists |bytes| ptr.points_to_owned(bytes) && bytes.len() == mem::size_of<T>() }}
329 ```
330 (The usual notation just uses single curly braces, but with me using Rust syntax here that looks too much like a block.)
331 {% endraw %}
332
333 This definition is deliberately narrow; `drop` is complicated and as I mentioned I don't feel ready to fully specify it.
334 But we can already see the interaction between the pinned typestate and dropping: If we move to the pinned typestate, we can call `drop` to re-gain ownership of the memory backing the `T`.
335 This is what happens when a `PinBox<t>` gets deallocated: It first calls `T::drop` on the contents (which it can do, because it as `T` pinned and hence the precondition is satisfied), obtaining ownership of the memory as expressed in the postcondition above, and then uses that ownership to deallocate the memory.
336
337 Let us look at `Entry<T>` as an example `drop` implementation, and see how we can justify that it satisfies the specification in definition 1.
338 We proceed by case distinction on `Entry<T>.pin`:
339 1. We are in the `None` branch.  Then we already own the memory for the `collection` field, and calling `T::drop` on `x` is guaranteed to give us the ownership of the first field as well.
340 Overall, we thus own all the memory backing the entry, so we can satisfy the postcondition.
341 2. We are in the `Some` branch. As already discussed, we then give up ownership of `entry_owned_in_collection` to remove ourselves from the collection, obtaining ownership of our own memory.
342 Then we proceed as above.
343
344 Noticeably, we did not make any kind of reasoning along the lines of "all memory will be deallocated eventually".
345 There is no talking about leaks.
346 We are just concerned with *safety* here: When memory is pinned, it is only safe to deallocate after `drop` has been called.
347
348 One important observation is that if we did *not* remove the entry from the collection, we would be unable to satisfy the postcondition!
349 This matches the fact that our entire collection would be unsound if we removed the `Entry::drop`.
350 In other words, if we do *not* implement `Drop`, this actually incurs a proof obligation!
351 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>()`.
352 This is the part that would go wrong if we were to remove `Entry::drop`.
353 It seems rather funny that *not* implementing a trait incurs a proof obligation, but there's also nothing fundamentally wrong with that idea.
354
355 Coming back to the general case, it seems quite curious to tie `drop` to pinning like that.
356 What about dropping things that are not pinned?
357 The answer is that it is always legal to start pinning something that we fully own.
358 Formally speaking, we can always use axiom (b) from my last post to briefly pin it, and then call `drop`.
359 In other words, we can derive the following Hoare triple:
360 ```
361 { exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes) }
362   T::drop(ptr)
363 { exists |bytes| ptr.points_to_owned(bytes) && bytes.len() == mem::size_of<T>() }
364 ```
365 Using axiom (b), the precondition of this triple implies the precondition of the one in definition 1.
366 That's good enough to show that this second specification for `drop` has to hold if the first holds.
367 So, if I use an arbitrary type while being oblivious to pinning, I can keep using the `drop` specification above.
368 This matches the locality of pinning that I described last time: Code that does not do pinning, does not have to care.
369
370 To complete the locality story, we have to think not only about *using* some arbitrary `T`, but also about *defining* a `T` without caring about pinning.
371 As discussed last time, we will then pick `T.pin` to just piggy-back on `T.own`:
372 ```
373 T.pin(ptr) := exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes)
374 ```
375 For such `T`, the two different specifications for `drop` that I showed above are actually equivalent.
376 Such types can prove their `drop` correct with respect to the `T.own`-based specification and automatically satisfy the pinning guarantees.
377 In particular, if they do not implement `Drop`, this specification holds trivially.[^3]
378 The funny proof obligation incurred by not implementing `Drop` only arises for types that care about pinning.
379
380 [^3]: This uses the fact that `T.own(bytes)` implies `bytes.len() == mem::size_of<T>()`.  This is another axiom that has to hold for all types, one that did not come up in previous discussion.
381
382 ## 3 What About Shared References?
383
384 Finally, we come to the part where my current model is not good enough.
385 If you paid really, really close attention to my example above, you may have been irritated by the type of `insert`:
386 {% highlight rust %}
387     fn insert(mut self: Pin<Self>, entry: Pin<Entry<T>>)
388 {% endhighlight %}
389 @cramertj originally proposed to use a slightly different type instead:
390 {% highlight rust %}
391     fn insert(mut self: Pin<Self>, entry: &Pin<Entry<T>>)
392 {% endhighlight %}
393 Notice the shared reference on the `entry` argument.
394 Since all the mutation we perform there happens inside a `Cell`, why shouldn't we provide this function for shared pinned data?[^4]
395
396 [^4]: In my version, the collection itself is also using `RefCell`, which I believe @cramertj just forgot to do---the write access from `Entry::drop` would be unsound otherwise. However, it seems more natural to ask the collection itself to be mutable for insertion, not exposing the fact that we use interior mutability.
397
398 That's a good question!
399 It seems perfectly fine to change `insert` to take `&Pin<Entry<T>>`.
400 I can't come up with any counter-example.
401 However, the formal model also cannot justify this variant of `insert`: As we defined previously, `Pin<'a, T>.shr` just uses `T.shr`.
402 That made it easy to justify [`Pin::deref`](https://doc.rust-lang.org/nightly/std/mem/struct.Pin.html#method.deref).
403 However, it also means `&Pin<T>` and `&&T` *are the same type*.
404 The two invariants are equivalent.
405 We could literally write functions transmuting between the two, and we could justify them in my model.
406 Clearly, `insert` taking `entry: &&T` would be unsound as nothing stops the entry from being moved later:
407 {% highlight rust %}
408 fn main() {
409     let mut collection = PinBox::new(Collection::new());
410     let entry = {
411       let mut entry = Box::new(Entry::new(42));
412       collection.as_pin().insert(&&*entry); // Register boxed entry in collection
413       *entry // Move entry out of the Box, and drop the box
414     };
415     // We keep the entry so it does not get dropped.
416     // The collection still points to the now deallocated box!
417     collection.as_pin().print_all(); // Fireworks happen
418 }
419 {% endhighlight %}
420 This shows that the version of `insert` that takes a shared reference cannot be sound in the model.
421
422 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.
423 However, I previously argued strongly against introducing such a fourth state, on the grounds that three typestates is already complicated enough.
424 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.
425 The shared variant got subsequently removed, and I feel somewhat guilty about that now because I strongly pushed for it.
426 It seems, after all, that the fourth typestate arises anyway.
427
428 We have to make a decision here, before stabilizing `Pin`: Do we want `insert` with a shared reference to be legal?
429 Or do want to declare that `&Pin<T>` and `&&T` are interchangeable types?
430 One may argue that adding an entry to a collection logically changes that entry, so really this should require an exclusive pinned reference.
431 However, given that the changed API seems entirely safe to use, I have to admit that's a somewhat weak argument.
432 Converting between `&Pin<T>` and `&&T` seems to have no tangible benefit other than satisfying my model.
433
434 For these reasons, I now think that removing the shared pinned reference may have been a mistake: It turns out that, if we want to allow an intrusive collection like the above that works with `&Pin`, we need the fourth typestate anyway.
435 At that point we might as well have a type reflecting it, avoiding the confusion and the double indirection that comes with `&Pin`.
436 I hope we do not end up in a situation where `insert` with a shared reference is legal, but we do not have a type for shared pinned references.
437 That just seems like the worst of both worlds.
438
439 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. :/
440 I feel bad about that.  Can we still fix this before everything gets stabilized?
441 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 am repentantly joining their choir now after arguing against them previously.
442 Sorry for that, and thanks for not being convinced by me!
443
444 ## 4 Conclusion
445
446 Leaving aside the last part about shared pinning, I am really excited how all of this fits together so nicely.
447 Back when I was learning Rust, I remember thinking how intrusive collections with entries on the stack (as they are commonly used, for example, in the Linux kernel) unfortunately cannot be given a safe interface in Rust.
448 I am happy to learn that I was wrong!
449 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.
450
451 #### Footnotes