clarify changed init signature

[web.git] / personal / _posts / 2018-04-05-a-formal-look-at-pinning.md

diff --git a/personal/_posts/2018-04-05-a-formal-look-at-pinning.md b/personal/_posts/2018-04-05-a-formal-look-at-pinning.md
index a82c9cdad329543e0cf0f98a87bf1a1600e9ad1a..98b53a18eea36c911f55de6f30f4733c83da360b 100644 (file)
--- a/personal/_posts/2018-04-05-a-formal-look-at-pinning.md
+++ b/personal/_posts/2018-04-05-a-formal-look-at-pinning.md
@@ -89,7 +89,7 @@ fn main() {
 The most intersting piece of code here is `read_ref`, which dereferences a raw pointer.
 The reason this is legal is that we can rely on the entire `SelfReferential` not having been moved since `init()` was called (which is the only place that would set the pointer to `Some`).
 
 The most intersting piece of code here is `read_ref`, which dereferences a raw pointer.
 The reason this is legal is that we can rely on the entire `SelfReferential` not having been moved since `init()` was called (which is the only place that would set the pointer to `Some`).
 

-In particular, if we changed the signature of `init()` to take `&mut`, we could easily cause UB by writing the following code:
+In particular, if we changed the signature to `fn init(&mut self)`, we could easily cause UB by writing the following code:

 {% highlight rust %}
 fn main() {
     // Create an initialize a SelfReferential in a Box, move it out, and drop the Box
 {% highlight rust %}
 fn main() {
     // Create an initialize a SelfReferential in a Box, move it out, and drop the Box


@@ -118,29 +118,31 @@ The full formalism we use in the paper is probably overkill, so I will go with a
 For example, the axiom (a) stated above would look as follows:
 ```
 forall |'a, ptr|
 For example, the axiom (a) stated above would look as follows:
 ```
 forall |'a, ptr|

-  borrowed('a, exists |bytes| mem_own(ptr, bytes) && T.own(bytes))
+  borrowed('a, exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes))

   -> T.shr('a, ptr)
 ```
 I am using the usual mathematical quantifiers, with a Rust-y syntax (`forall |var| P` and `exists |var| P`), and `->` for implication.
 For disjunction (`||`) and conjunction (`&&`), I follow Rust.
 
 We also need some way to talk about ownership and contents of memory:
   -> T.shr('a, ptr)
 ```
 I am using the usual mathematical quantifiers, with a Rust-y syntax (`forall |var| P` and `exists |var| P`), and `->` for implication.
 For disjunction (`||`) and conjunction (`&&`), I follow Rust.
 
 We also need some way to talk about ownership and contents of memory:

-I will write `mem_own_bytes(ptr, bytes)` (where `ptr: Pointer` and `bytes: List<Byte>`) to express that we own `bytes.len()` many bytes of memory pointed to by `ptr`.
+I will write `ptr.points_to_owned_bytes(bytes)` (where `ptr: Pointer` and `bytes: List<Byte>`) to express that `ptr` points to `bytes.len()` many bytes of memory containing the given `bytes` of data, and that moreover, we *own* that memory.

 Ownership here means that we are free to read, write and deallocate that memory.
 
 Frequently, it is more convenient to not talk about raw lists of bytes but about some higher-level representation of the bytes, and not care about how exactly that data is laid out in memory.
 Ownership here means that we are free to read, write and deallocate that memory.
 
 Frequently, it is more convenient to not talk about raw lists of bytes but about some higher-level representation of the bytes, and not care about how exactly that data is laid out in memory.

-For example, we might want to say that `ptr` points to `42` of type `i32` by saying `mem_own(ptr, 42i32)`.
-We can define a suitable `mem_own` as
+For example, we might want to say that `ptr` points to `42` of type `i32` by saying `ptr.points_to_owned(42i32)`.
+We can define a suitable `points_to_owned` as

 ```
 ```

-mem_own<U>(ptr: Pointer, data: U) where List<Bytes>: TryInto<U> :=
-  exists |bytes| bytes.try_into() == Ok(data) && mem_own(ptr, bytes)
+ptr.points_to_owned(data: U) where List<Bytes>: TryInto<U> :=
+  exists |bytes| bytes.try_into() == Ok(data) && ptr.points_to_owned_bytes(bytes)

 ```
 Here, we (ab)use the `TryInto` trait to convert a properly laid out list of bytes into something of type `U`.
 The conversion fails, in particular, if the list does not have exactly the right length.
 ```
 Here, we (ab)use the `TryInto` trait to convert a properly laid out list of bytes into something of type `U`.
 The conversion fails, in particular, if the list does not have exactly the right length.

-If `U == List<Bytes>`, this is just the same as `mem_own_bytes`.
+If `U == List<Bytes>`, this is just the same as `ptr.points_to_owned_bytes`.
+
+**Update:** In a previous version I called these predicates `mem_own_bytes` and `mem_own`. I decided that `points_to_owned` was actually easier to understand, and it also matches the standard terminology in the literature, so I switched to using that term instead. **/Update**

 
 Finally, `borrowed('a, P)` says that `P` is only temporarily owned, i.e., borrowed, for lifetime `'a`.
 
 Finally, `borrowed('a, P)` says that `P` is only temporarily owned, i.e., borrowed, for lifetime `'a`.

-`P` here is a *proposition* or *assertion*, i.e., a statement about what we expect to own. The axiom above is a proposition, as is `mem_own(ptr, 42i32)`.
+`P` here is a *proposition* or *assertion*, i.e., a statement about what we expect to own. The axiom above is a proposition, as is `ptr.points_to_owned(42i32)`.

 You can think of propositions as a fancy version of `bool` where we can use things like quantifiers or borrowing, and talk about memory and ownership.
 
 Let us see how we can define the owned typestate of `Box` and mutable reference using this notation:
 You can think of propositions as a fancy version of `bool` where we can use things like quantifiers or borrowing, and talk about memory and ownership.
 
 Let us see how we can define the owned typestate of `Box` and mutable reference using this notation:


@@ -150,10 +152,13 @@ A `Box<T>` is a list of bytes that make up a pointer, such that we own the memor
 `&'a mut T` is almost the same, except that memory and `T.own` are only borrowed for lifetime `'a`.
 Formally:
 ```
 `&'a mut T` is almost the same, except that memory and `T.own` are only borrowed for lifetime `'a`.
 Formally:
 ```

-Box<T>.own(bytes) := exists |ptr, inner_bytes|
-   bytes.try_into() == Ok(ptr) && mem_own(ptr, inner_bytes) && T.own(inner_bytes)
+Box<T>.own(bytes) := exists |ptr, inner_bytes| bytes.try_into() == Ok(ptr) &&
+  ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)
+```
+```

 (&'a mut T).own(bytes) := exists |ptr| bytes.try_into() == Ok(ptr) &&
 (&'a mut T).own(bytes) := exists |ptr| bytes.try_into() == Ok(ptr) &&

-  borrowed('a, exists |inner_bytes| mem_own(ptr, inner_bytes) && T.own(inner_bytes))
+  borrowed('a,
+    exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))

 ```
 
 It turns out that using `try_into` like we do above is actually a common pattern.
 ```
 
 It turns out that using `try_into` like we do above is actually a common pattern.


@@ -162,9 +167,11 @@ To facilitate this, we will typically define `T.own(data: U)` for some `U` such
 This could look as follows:
 ```
 Box<T>.own(ptr: Pointer) :=
 This could look as follows:
 ```
 Box<T>.own(ptr: Pointer) :=

-  exists |inner_bytes| mem_own(ptr, inner_bytes) && T.own(inner_bytes)
+  exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)
+```
+```

 (&'a mut T).own(ptr: Pointer) :=
 (&'a mut T).own(ptr: Pointer) :=

-  borrowed('a, exists |inner_bytes| mem_own(ptr, inner_bytes) && T.own(inner_bytes))
+  borrowed('a, exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))

 ```
 The actual ownership predicate is then defined as
 ```
 ```
 The actual ownership predicate is then defined as
 ```


@@ -195,7 +202,7 @@ This gives us the expressivity we need to talk about immovable data:
 Moreover, if `self_ref` is set to `Some(data_ptr)`, then `data_ptr` is the address of the first field of the pair:
 ```
 SelfReferential.pin(ptr) := exists |data: i32, self_ref: Option<ptr::NonNull<i32>>|
 Moreover, if `self_ref` is set to `Some(data_ptr)`, then `data_ptr` is the address of the first field of the pair:
 ```
 SelfReferential.pin(ptr) := exists |data: i32, self_ref: Option<ptr::NonNull<i32>>|

-  mem_own(ptr, (data, self_ref)) &&
+  ptr.points_to_owned((data, self_ref)) &&

   match self_ref { Some(data_ptr) => data_ptr.as_ptr() == ptr.offset(0), None => True }
 ```
 The most important part of this is the last line, saying that if `data_ptr` is a `Some`, it actually points to the first field (at offset `0`).
   match self_ref { Some(data_ptr) => data_ptr.as_ptr() == ptr.offset(0), None => True }
 ```
 The most important part of this is the last line, saying that if `data_ptr` is a `Some`, it actually points to the first field (at offset `0`).


@@ -220,6 +227,8 @@ A list of bytes makes a valid `PinBox<T>` if those bytes form a pointer `ptr` su
 For `Pin<'a, T>`, `ptr` is valid if we have borrowed `T.pin(ptr)` for lifetime `'a`.
 ```
 PinBox<T>.own(ptr) := T.pin(ptr)
 For `Pin<'a, T>`, `ptr` is valid if we have borrowed `T.pin(ptr)` for lifetime `'a`.
 ```
 PinBox<T>.own(ptr) := T.pin(ptr)

+```
+```

 Pin<'a, T>.own(ptr) := borrowed('a, T.pin(ptr))
 ```
 
 Pin<'a, T>.own(ptr) := borrowed('a, T.pin(ptr))
 ```
 


@@ -233,7 +242,7 @@ This seems like a reasonable principle to require in general, so we add it to ou
 > {:type="a" start="2"}
 2. If we own a pointer `ptr` pointing to a list of bytes `bytes` such that `T.own(bytes)` holds, then we can move to the pinned typestate and obtain `T.pin(ptr)`. Formally:
 ```
 > {:type="a" start="2"}
 2. If we own a pointer `ptr` pointing to a list of bytes `bytes` such that `T.own(bytes)` holds, then we can move to the pinned typestate and obtain `T.pin(ptr)`. Formally:
 ```

-forall |ptr, bytes| (mem_own(ptr, bytes) && T.own(bytes)) -> T.pin(ptr)
+forall |ptr, bytes| (ptr.points_to_owned(bytes) && T.own(bytes)) -> T.pin(ptr)

 ```
 
 `PinBox::new` can now be easily implemented using `Box::new` and `PinBox<T>::from`.
 ```
 
 `PinBox::new` can now be easily implemented using `Box::new` and `PinBox<T>::from`.


@@ -241,7 +250,7 @@ forall |ptr, bytes| (mem_own(ptr, bytes) && T.own(bytes)) -> T.pin(ptr)
 For `PinBox::as_pin`, we start with a `&'a mut PinBox<T>`, which is a pointer-to-pointer, and return the inner pointer as `Pin<'a, T>`.
 This is justified because we start with a borrow for lifetime `'a` of a pointer to some `bytes` that satisfy (for the given lifetime) `PinBox<T>.own(bytes)`:
 ```
 For `PinBox::as_pin`, we start with a `&'a mut PinBox<T>`, which is a pointer-to-pointer, and return the inner pointer as `Pin<'a, T>`.
 This is justified because we start with a borrow for lifetime `'a` of a pointer to some `bytes` that satisfy (for the given lifetime) `PinBox<T>.own(bytes)`:
 ```

-borrowed('a, exists |bytes| mem_own(ptr, bytes) && PinBox<T>.own(bytes))
+borrowed('a, exists |bytes| ptr.points_to_owned(bytes) && PinBox<T>.own(bytes))

 ```
 Unfolding the `PinBox<T>.own`, we can deduce that `bytes` actually form a pointer `inner_ptr` such that `T.pin(inner_ptr)` (for the given lifetime).
 This exactly matches our return type, so we're good!
 ```
 Unfolding the `PinBox<T>.own`, we can deduce that `bytes` actually form a pointer `inner_ptr` such that `T.pin(inner_ptr)` (for the given lifetime).
 This exactly matches our return type, so we're good!


@@ -270,13 +279,14 @@ A pointer `ptr` and lifetime `'a` satisfy the shared typestate of `PinBox<T>` if
 In other words, a shared `PinBox<T>` is just a read-only pointer to a shared `T`:
 ```
 PinBox<T>.shr('a, ptr) := exists |inner_ptr|
 In other words, a shared `PinBox<T>` is just a read-only pointer to a shared `T`:
 ```
 PinBox<T>.shr('a, ptr) := exists |inner_ptr|

-  mem_read_only('a, ptr, inner_ptr) && T.shr('a, inner_ptr)
+  ptr.points_to_read_only('a, inner_ptr) && T.shr('a, inner_ptr)

 ```
 This requires a way to talk about memory that is read-only for the duration of some lifetime.
 ```
 This requires a way to talk about memory that is read-only for the duration of some lifetime.

-We assume we have a predicate `mem_read_only_bytes('a: Lifetime, ptr: Pointer, bytes: List<Byte>)` for this purpose, and then define a typed variant as usual:
+We assume we have a predicate `ptr.points_to_read_only_bytes('a: Lifetime, bytes: List<Byte>)` saying that `ptr` points to `bytes.len()` many bytes of valid memory containing `bytes`, and that for lifetime `'a`, we are free to read that memory and it will not change.
+We then define a convenient variant based on higher-level memory representations as usual:

 ```
 ```

-mem_read_only<U>('a: Lifetime, ptr: Pointer, data: U) where List<Bytes>: TryInto<U> :=
-  exists |bytes| bytes.try_into() == Ok(data) && mem_read_only_bytes('a, ptr, bytes)
+ptr.points_to_read_only('a: Lifetime, data: U) where List<Bytes>: TryInto<U> :=
+  exists |bytes| bytes.try_into() == Ok(data) && ptr.points_to_read_only_bytes('a, bytes)

 ```
 
 Remember that there is an axiom (a) connecting the owned and shared typestate; we have to make sure that this axiom is satisfied for `PinBox`---it turns out that is the case, and the proof relies on the new axiom (c) we just added.
 ```
 
 Remember that there is an axiom (a) connecting the owned and shared typestate; we have to make sure that this axiom is satisfied for `PinBox`---it turns out that is the case, and the proof relies on the new axiom (c) we just added.


@@ -293,7 +303,7 @@ Formally speaking:
 > **Definition 6: `Unpin`.** A type `T` is `Unpin` if from `T.pin(ptr)` we can deduce that we own the pointer `ptr` and it points to a list of bytes `bytes` such that `T.own(bytes)` holds.
 Formally:
 ```
 > **Definition 6: `Unpin`.** A type `T` is `Unpin` if from `T.pin(ptr)` we can deduce that we own the pointer `ptr` and it points to a list of bytes `bytes` such that `T.own(bytes)` holds.
 Formally:
 ```

-forall |ptr| T.pin(ptr) -> (exists |bytes| mem_own(ptr, bytes) && T.own(bytes))
+forall |ptr| T.pin(ptr) -> (exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes))

 ```
 
 Note that this is exactly the inverse direction of axiom (b) added in definition 2b: For `Unpin` types, we can freely move between the owned and pinned typestate.
 ```
 
 Note that this is exactly the inverse direction of axiom (b) added in definition 2b: For `Unpin` types, we can freely move between the owned and pinned typestate.


@@ -310,7 +320,7 @@ One advantage of this proposal is that it is *local*:
 Existing types (and new types) that are designed without considering `Pin` remain sound in the presence of this new typestate, even if we automatically derive the `Unpin` trait for these types.
 The reason this works is that we can always define `T.pin(ptr)` as saying that we fully own `ptr` pointing to `bytes` such that we have `T.own(bytes)`:
 ```
 Existing types (and new types) that are designed without considering `Pin` remain sound in the presence of this new typestate, even if we automatically derive the `Unpin` trait for these types.
 The reason this works is that we can always define `T.pin(ptr)` as saying that we fully own `ptr` pointing to `bytes` such that we have `T.own(bytes)`:
 ```

-T.pin(ptr) := exists |bytes| mem_own(ptr, bytes) && T.own(bytes)
+T.pin(ptr) := exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes)

 ```
 This satisfies the additional axioms (b) and (c) connecting the pinned typestate to the others, and it also satisfies `Unpin`.
 The latter is crucial, because it means we can automatically derive `Unpin` instances through the auto trait mechanism and do not have to review the entire ecosystem for `Pin`-compatibility.
 ```
 This satisfies the additional axioms (b) and (c) connecting the pinned typestate to the others, and it also satisfies `Unpin`.
 The latter is crucial, because it means we can automatically derive `Unpin` instances through the auto trait mechanism and do not have to review the entire ecosystem for `Pin`-compatibility.