typo
[web.git] / ralf / _posts / 2018-04-10-safe-intrusive-collections-with-pinning.md
1 ---
2 title: "Safe Intrusive Collections with Pinning"
3 categories: research rust
4 forum: https://internals.rust-lang.org/t/safe-intrusive-collections-with-pinning/7281
5 ---
6
7 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.
8 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.
9 This post is about another application of pinned references---another API whose safety relies on the pinning guarantees: Intrusive collections.
10 It turns out that pinned references can *almost* be used for this, but not quite.
11 However, this can be fixed by extending the guarantees provided by pinned references, as suggested by @cramertj.
12
13 <!-- MORE -->
14
15 The first part is going to explain how intrusive collections could benefit from `Pin`, were we to accept that additional guarantee.
16 This part assumes some familiarity with the `Pin` API, but not with the formal model I introduced previously.
17
18 In the second part, I am going to briefly sketch a formal perspective on intrusive collections and the extended pinning guarantees.
19 This builds on the formal notation I introduced in my last post.
20
21 Finally, I will discuss a variant of our "running example" intrusive collection that combines shared references and pinning.
22 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.
23 However, this extended model will actually call for a change to the `Pin` API (or rather, for a revert to an earlier version).
24
25 (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.)
26
27 ## 1 Safe Intrusive Collections
28
29 Intrusive collections typically are linked data structures that embed the links in the data they contain.
30 In the words of the [intrusive-collections crate](https://crates.io/crates/intrusive-collections):
31 > 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.
32
33 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.
34 The intrusive-collections crate realizes this by taking ownership of the objects.
35 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.
36 This means we cannot add short-lived objects, e.g. stack-allocated objects, to a collection that was created further up the call chain.
37 How could we go about lifting that restriction?
38
39 ### 1.1 An Example Collection
40
41 To get more concrete, consider the following example ([originally proposed by @cramertj](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-372432435)).
42 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.
43 (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.
44 I will leave [writing linked lists](http://cglab.ca/~abeinges/blah/too-many-lists/book/) to others.)
45 {% highlight rust %}
46 #![feature(pin, arbitrary_self_types, optin_builtin_traits)]
47
48 use std::cell::{Cell, RefCell};
49 use std::mem::Pin;
50 use std::boxed::PinBox;
51 use std::marker::Unpin;
52
53 struct Collection<T> {
54     objects: RefCell<Vec<*const Entry<T>>>,
55 }
56 impl<T> !Unpin for Collection<T> {}
57
58 struct Entry<T> {
59     x: T,
60     // set to Some if we are part of some collection
61     collection: Cell<Option<*const Collection<T>>>,
62 }
63 impl<T> !Unpin for Entry<T> {}
64
65 impl<T> Collection<T> {
66     fn new() -> Self {
67         Collection { objects: RefCell::new(Vec::new()) }
68     }
69
70     // Add the entry to the collection
71     fn insert(mut self: Pin<Self>, entry: Pin<Entry<T>>) {
72         if entry.collection.get().is_some() {
73             panic!("Can't insert the same object into multiple collections");
74         }
75         // Pointer from collection to entry
76         let this : &mut Self = unsafe { Pin::get_mut(&mut self) };
77         this.objects.borrow_mut().push(&*entry as *const _);
78         // Pointer from entry to collection
79         entry.collection.set(Some(this as *const _));
80     }
81     
82     // Show all entries of the collection
83     fn print_all(self: Pin<Self>)
84     where T: ::std::fmt::Debug
85     {
86         print!("[");
87         for entry in self.objects.borrow().iter() {
88             let entry : &Entry<T> = unsafe { &**entry };
89             print!(" {:?},", entry.x);
90         }
91         println!(" ]");
92     }
93 }
94
95 impl<T> Drop for Collection<T> {
96     fn drop(&mut self) {
97         // Go through the entries to remove pointers to collection
98         for entry in self.objects.borrow().iter() {
99             let entry : &Entry<T> = unsafe { &**entry };
100             entry.collection.set(None);
101         }
102     }
103 }
104
105 impl<T> Entry<T> {
106     fn new(x: T) -> Self {
107         Entry { x, collection: Cell::new(None) }
108     }
109 }
110
111 impl<T> Drop for Entry<T> {
112     fn drop(&mut self) {
113         // Go through collection to remove this entry
114         if let Some(collection) = self.collection.get() {
115             let collection : &Collection<T> = unsafe { &*collection };
116             collection.objects.borrow_mut().retain(|ptr| *ptr != self as *const _);
117         }
118     }
119 }
120
121 fn main() {
122     let mut collection = PinBox::new(Collection::new());
123     let mut entry = PinBox::new(Entry::new(42));
124     collection.as_pin().insert(entry.as_pin());
125     collection.as_pin().print_all(); // Prints "[ 42, ]"
126     drop(entry); // Dropping the entry removes it
127     collection.as_pin().print_all(); // Prints "[ ]"
128 }
129 {% endhighlight %}
130 This is lots of code.
131 The high-level picture is as follows:
132 The collection is represented by a `Vec` of raw pointers pointing to the entries.
133 Every entry has a "parent" pointer `self.collection` back to the main collection.
134 Inserting an entry into a collection involves adding it to the `Vec` and setting the collection pointer of the entry.
135 When an entry is dropped, if it is in a collection, it gets removed from the `Vec`.
136 When the collection is dropped, all the entries have their collection pointer reset to `None`.
137
138 The example code in `main` demonstrates how the collection could be used: First we add an entry containing `42` to the collection.
139 This is possible despite there being no guarantee that the entry will outlive the collection.
140 `print_all` shows that it is there.
141 Then we `drop` the entry while the collection still exists, and we can see it has vanished from the collection as well.
142
143 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!
144 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.
145 Thanks to this guarantee, and unlike in the intrusive-collections crate, `insert` can be called with entries *that do not outlive the collection*.
146 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.
147
148 ### 1.2 Pinning Is Not Enough
149
150 However, it turns out pinning as described so far is not enough to guarantee safety.
151 Imagine we added the following method to `PinBox`:
152 {% highlight rust %}
153 fn box_deallocate<T>(x: Box<T>) {
154   let content = *x; // move out of the box
155   mem::forget(content); // do not call drop
156   // Implicitly deallocate the box
157 }
158
159 impl<T> PinBox<T> {
160   // Deallocate the box without calling drop
161   fn deallocate(self) {
162     box_deallocate(self.inner)
163   }
164 }
165 {% endhighlight %}
166 `box_deallocate` is obviously safe on `Box` (we do not use any unsafe code).
167 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.
168 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.
169
170 Why is this a problem?  Well, we can now add an entry to a collection and then *deallocate the entry without calling `drop`*.
171 This leads to a dangling pointer inside the collection, which is obviously bad:
172 {% highlight rust %}
173 fn main() {
174     let mut collection = PinBox::new(Collection::new());
175     let mut entry = PinBox::new(Entry::new(42));
176     collection.as_pin().insert(entry.as_pin()); // Register entry in collection
177     entry.deallocate(); // Now the collection still points to the entry
178     collection.as_pin().print_all(); // And now everything explodes
179 }
180 {% endhighlight %}
181
182 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/stable/std/mem/struct.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`.
183 That has the same effect as `PinBox::deallocate`: It renders our collection interface unsound.
184 The concern about dropping pinned data is real.
185
186
187 ### 1.3 Requiring Drop To Be Run
188
189 @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*.
190 This just changes the way we have to think about pinned data, but does not affect the API at all.
191
192 Combining that with the guarantee about moving, we can summarize `Pin` as follows:
193
194 > 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.
195
196 Under our new rules, `PinBox::deallocate` is bogus, and our collection works again.
197
198 And not just our artificial little example collection would benefit from this guarantee.
199 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.
200 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.
201 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).
202 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.
203
204 ### 1.4 Some Common Objections
205
206 I hope I convinced you that it is desirable to guarantee that `drop` is run on pinned references.
207 Before we come to the formal part of this post, let me go over some possible objections to this extended guarantee.
208 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.
209 So I will just reiterate my own objections and how I feel about them now.
210
211 The first objection is: Haven't we had this discussion already?
212 [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.
213 However, even if we accept this proposal *leaking pinned data is still allowed*!
214 The guarantee says that *if memory gets deallocated or otherwise invalidated*, we will call `drop`.
215 So, calling `mem::forget` on a `PinBox` is fine.
216 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.
217 So, this proposal does *not* backpedal on memory leak guarantees in Rust.
218 Both `mem::forget` and `ManaullyDrop` remain sound.
219 What would *not* be sound is adding a way to obtain a `Pin` reference *into* a `ManuallyDrop`.
220 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.
221 (Linear reasoning is typically used to prove properties like memory-leak-freedom.)
222
223 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`?
224 Pinning and calling `drop` are entirely orthogonal concerns!
225 Well, this is certainly true for general leak-freedom.
226 However, the guarantee we are after here is that `drop` will be called *if this memory ever gets deallocated*.
227 So, the guarantee is tied to a particular spot in memory---a concept that only makes sense if data is pinned to begin with!
228 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.
229 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).
230 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!
231
232 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).
233 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.
234
235 ## 2 The Formal Perspective
236
237 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.
238 I am going to assume that you have read that post.
239
240 ### 2.1 The Intrusive Collection Invariant
241
242 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`.
243 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.
244 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:
245 ```
246 exists |bytes|, ptr.points_to_owned(bytes) && T.own(bytes)
247 ```
248 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.
249 We could even deallocate it.
250 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.
251
252 With `T.pin`, we have more freedom to choose our invariant.
253 `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.
254
255 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.
256 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]
257 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:
258
259 [^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).
260
261 ```
262 Collection<T>.pin(ptr) := exists |entries: List<Pointer>|
263   ptr.points_to_owned(RefCell::new(Vec::from(entries))) &&
264   entries.all(|entry| T.pin(entry.offset_to_field(x)) &&
265     entry.offset_to_field(collection).points_to_owned(Cell::new(Some(ptr)))
266   )
267 ```
268 Notice how we iterate over the elements of the list and make sure that we own whatever memory is to own there.
269 (I love how `all` [really exists for iterators](https://doc.rust-lang.org/stable/std/iter/trait.Iterator.html#method.all) so I can express quantification over lists without any hassle. :)
270
271 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`.
272
273 So, what will `Entry` say in its pinned invariant?
274 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.
275 ```
276 Entry<T>.pin(ptr) := exists |collection: Option<Pointer>|
277   match collection {
278     None => T.pin(ptr.offset_to_field(x)) &&
279       ptr.offset_to_field(collection).points_to_owned(Cell::new(None)),
280     Some(collection) => entry_owned_in_collection(ptr, collection)
281   }
282 ```
283 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.
284 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.
285 Fictional ownership is an extremely powerful concept---it forms the very basis of the [mathematical framework we use in RustBelt](http://iris-project.org/).
286 However, actually doing this formally is well beyond the scope of this post.[^2]
287
288 [^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`.
289
290 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.
291 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.
292
293 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.
294 In exchange, we obtain an `entry_owned_in_collection`, which can put back into the entry.
295 This means, when we return, the entry is fully valid in the `Some` branch.
296 That's crucial, because it's just a reference and hence borrowed---we have to restore all the invariants before we return!
297
298 ### 2.2 Requiring Drop To Be Run
299
300 So, how is the new `drop` guarantee we have been talking about reflected in the formal model?
301 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`.
302 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!
303 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`.
304
305 Now, I should make clear that we are entering uncharted territory here.
306 RustBelt does *not* model `drop`.
307 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.
308 My intuition has been wrong before.
309
310 With the disclaimer out of the way, let us look at `drop`.
311 First of all, `drop` is not a normal function. If we could just call it, we could write code like
312 {% highlight rust %}
313 let mut v = vec![0];
314 Vec::drop(&mut v);
315 v.push(1); // BOOM!
316 {% endhighlight %}
317 `Vec::drop` leaves the vector in a bad state, and we must not call any normal method on it again afterwards.
318 So, a correctness proof for `drop` is clearly going to be different from a correctness proof for a normal method that takes an `&mut`.
319 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`.
320 In the case of `Vec`, none of the fields implements `Drop`, so let us focus on that special case:
321
322 {% raw %}
323 > **Definition 1: `drop`, special case where no field implements `Drop`.**
324 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.
325
326 > 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:
327 ```
328 {{ T.pin(ptr) }}
329   T::drop(ptr)
330 {{ exists |bytes| ptr.points_to_owned(bytes) && bytes.len() == mem::size_of<T>() }}
331 ```
332 (The usual notation just uses single curly braces, but with me using Rust syntax here that looks too much like a block.)
333 {% endraw %}
334
335 This definition is deliberately narrow; `drop` is complicated and as I mentioned I don't feel ready to fully specify it.
336 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`.
337 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.
338
339 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.
340 We proceed by case distinction on `Entry<T>.pin`:
341 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.
342 Overall, we thus own all the memory backing the entry, so we can satisfy the postcondition.
343 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.
344 Then we proceed as above.
345
346 Noticeably, we did not make any kind of reasoning along the lines of "all memory will be deallocated eventually".
347 There is no talking about leaks.
348 We are just concerned with *safety* here: When memory is pinned, it is only safe to deallocate after `drop` has been called.
349
350 One important observation is that if we did *not* remove the entry from the collection, we would be unable to satisfy the postcondition!
351 This matches the fact that our entire collection would be unsound if we removed the `Entry::drop`.
352 In other words, if we do *not* implement `Drop`, this actually incurs a proof obligation!
353 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>()`.
354 This is the part that would go wrong if we were to remove `Entry::drop`.
355 It seems rather funny that *not* implementing a trait incurs a proof obligation, but there's also nothing fundamentally wrong with that idea.
356
357 Coming back to the general case, it seems quite curious to tie `drop` to pinning like that.
358 What about dropping things that are not pinned?
359 The answer is that it is always legal to start pinning something that we fully own.
360 Formally speaking, we can always use axiom (b) from my last post to briefly pin it, and then call `drop`.
361 In other words, we can derive the following Hoare triple:
362 ```
363 { exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes) }
364   T::drop(ptr)
365 { exists |bytes| ptr.points_to_owned(bytes) && bytes.len() == mem::size_of<T>() }
366 ```
367 Using axiom (b), the precondition of this triple implies the precondition of the one in definition 1.
368 That's good enough to show that this second specification for `drop` has to hold if the first holds.
369 So, if I use an arbitrary type while being oblivious to pinning, I can keep using the `drop` specification above.
370 This matches the locality of pinning that I described last time: Code that does not do pinning, does not have to care.
371
372 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.
373 As discussed last time, we will then pick `T.pin` to just piggy-back on `T.own`:
374 ```
375 T.pin(ptr) := exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes)
376 ```
377 For such `T`, the two different specifications for `drop` that I showed above are actually equivalent.
378 Such types can prove their `drop` correct with respect to the `T.own`-based specification and automatically satisfy the pinning guarantees.
379 In particular, if they do not implement `Drop`, this specification holds trivially.[^3]
380 The funny proof obligation incurred by not implementing `Drop` only arises for types that care about pinning.
381
382 [^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.
383
384 ## 3 What About Shared References?
385
386 Finally, we come to the part where my current model is not good enough.
387 If you paid really, really close attention to my example above, you may have been irritated by the type of `insert`:
388 {% highlight rust %}
389     fn insert(mut self: Pin<Self>, entry: Pin<Entry<T>>)
390 {% endhighlight %}
391 @cramertj originally proposed to use a slightly different type instead:
392 {% highlight rust %}
393     fn insert(mut self: Pin<Self>, entry: &Pin<Entry<T>>)
394 {% endhighlight %}
395 Notice the shared reference on the `entry` argument.
396 Since all the mutation we perform there happens inside a `Cell`, why shouldn't we provide this function for shared pinned data?[^4]
397
398 [^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.
399
400 That's a good question!
401 It seems perfectly fine to change `insert` to take `&Pin<Entry<T>>`.
402 I can't come up with any counter-example.
403 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`.
404 That made it easy to justify `Pin::deref`.
405 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*.
406 We could literally write functions transmuting between the two, and we could justify them in my model.
407 Clearly, `insert` taking `entry: &&T` would be unsound as nothing stops the entry from being moved later:
408 {% highlight rust %}
409 fn main() {
410     let mut collection = PinBox::new(Collection::new());
411     let entry = {
412       let mut entry = Box::new(Entry::new(42));
413       collection.as_pin().insert(&&*entry); // Register boxed entry in collection
414       *entry // Move entry out of the Box, and drop the box
415     };
416     // We keep the entry so it does not get dropped.
417     // The collection still points to the now deallocated box!
418     collection.as_pin().print_all(); // Fireworks happen
419 }
420 {% endhighlight %}
421 This shows that the version of `insert` that takes a shared reference cannot be sound in the model.
422
423 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`.
424 This does *not* show that `&Pin<T>` and `&&T` have to be the same type given the public API and the contract they provide.
425 Different choices in the model could lead to a different situation.
426 The problem is, how else *could* we define `Pin<'a, T>.shr`, if we do not want to use `T.shr`?
427 What *is* the invariant of a shared reference to a pinned reference?
428
429 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.
430 However, I previously argued strongly against introducing such a fourth state, on the grounds that three typestates is already complicated enough.
431 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.
432 The shared variant got subsequently removed, and I feel somewhat guilty about that now because I strongly pushed for it.
433 It seems, after all, that the fourth typestate arises anyway.
434
435 We have to make a decision here, before stabilizing `Pin`: Do we want `insert` with a shared reference to be legal?
436 Or do want to declare that `&Pin<T>` and `&&T` are interchangeable types?
437 One may argue that adding an entry to a collection logically changes that entry, so really this should require an exclusive pinned reference.
438 However, given that the changed collection API seems entirely safe to use, I have to admit that's a somewhat weak argument.
439 If the discussion so far is any indication, people want to write such APIs and will probably not be happy if we tell them that's illegal because there is a way to convert between `&Pin<T>` and `&&T`.
440 After all, that conversion seems to have no tangible benefit other than satisfying my model.
441
442 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.
443 At that point we might as well have a type reflecting it, avoiding the confusion and the double indirection that comes with `&Pin`.
444 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.
445 That just seems like the worst of both worlds.
446
447 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. :/
448 (**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**)
449 I feel bad about that.  Can we still fix this before everything gets stabilized?
450 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.
451 Thanks for not being convinced by me!
452
453 However, there is one strange aspect to this "shared pinned" typestate: Due to `Pin::deref`, we can turn a "shared pinned" reference into a shared reference.
454 We can go from `&Pin<T>` to `&&T`.
455 In other words, the shared pinned typestate invariant must *imply* the invariant for the (general, unpinned) shared typestate.
456 The reason for `Pin::deref` to exist is mostly a rustc implementation detail [related to using `Pin<Self>` as the type of `self`](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-372475895), but this detail has some significant consequences: Even with a separate shared pinned typestate, we can still not define `RefCell` in a way that a pinned `RefCell` pins its contents.
457 In particular, we cannot have a method like `fn get_pin(self: Pin<RefCell<T>>) -> Pin<T>`.
458 Removing `Pin::deref` (or restricting it to types that implement `Unpin`) would solve this issue.
459 I spelled out the details [in the RFC issue](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-372109981).
460 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?
461
462 **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**
463
464 ## 4 Conclusion
465
466 Leaving aside the last part about shared pinning, I am really excited how all of this fits together so nicely.
467 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.
468 I am happy to learn that I was wrong!
469 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.
470
471 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.
472
473 Anyway, as usual, please [let me know what you think](https://internals.rust-lang.org/t/safe-intrusive-collections-with-pinning/7281)!
474
475 #### Footnotes