add MoSeL paper

[web.git] / ralf / _posts / 2018-04-10-safe-intrusive-collections-with-pinning.md

diff --git a/ralf/_posts/2018-04-10-safe-intrusive-collections-with-pinning.md b/ralf/_posts/2018-04-10-safe-intrusive-collections-with-pinning.md
index 37da65c29587937af3d87adee74655b5a10e39de..a3f0cca04972c20f62db0500eb3cdddeef230164 100644 (file)
--- a/ralf/_posts/2018-04-10-safe-intrusive-collections-with-pinning.md
+++ b/ralf/_posts/2018-04-10-safe-intrusive-collections-with-pinning.md
@@ -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<Entry<T>>`.
 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<T>` 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<T>` 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<T>` 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.