mem_own -> points_to

diff --git a/personal/_posts/2017-07-17-types-as-contracts.md b/personal/_posts/2017-07-17-types-as-contracts.md
index bb867e78bcd9060690bafd94b568d903a397ce3a..d7b1b71a54c6dfbdc236bb1a5bf7fe2978f002ce 100644 (file)
--- a/personal/_posts/2017-07-17-types-as-contracts.md
+++ b/personal/_posts/2017-07-17-types-as-contracts.md
@@ -305,7 +305,7 @@ This grants the functions write access to memory that we are explicitly passing
 Suspend validation occurs before taking a reference, using the lifetime of the new reference.
 This encodes the fact that when the lifetime ends (and hence the lock is being reacquired), we are the exclusive owner of this memory again.
 
 Suspend validation occurs before taking a reference, using the lifetime of the new reference.
 This encodes the fact that when the lifetime ends (and hence the lock is being reacquired), we are the exclusive owner of this memory again.
 

-**Update**: It has been pointed out to me that another way for values to flow back into a function is through mutable references. Good catch! I will need to extend the validation machinery to also perform acquire validation when a write lock is reacquired. **/Update**
+**Update:** It has been pointed out to me that another way for values to flow back into a function is through mutable references. Good catch! I will need to extend the validation machinery to also perform acquire validation when a write lock is reacquired. **/Update**

 
 To summarize, validation statements are emitted during MIR construction in the following places:
 - At the beginning of the function, we perform acquire validation of the arguments.
 
 To summarize, validation statements are emitted during MIR construction in the following places:
 - At the beginning of the function, we perform acquire validation of the arguments.

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..e3c7412bb1912e0e8dec1d44efb0f0c522b2aef4 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
@@ -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(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_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(42i32)`.
+We can define a suitable `points_to` 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(data: U) where List<Bytes>: TryInto<U> :=
+  exists |bytes| bytes.try_into() == Ok(data) && ptr.points_to_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_bytes`.
+
+**Update:** In a previous version I called these predicates `mem_own_bytes` and `mem_own`. I decided that `points_to` 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(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:


@@ -151,9 +153,9 @@ A `Box<T>` is a list of bytes that make up a pointer, such that we own the memor
 Formally:
 ```
 Box<T>.own(bytes) := exists |ptr, inner_bytes|
 Formally:
 ```
 Box<T>.own(bytes) := exists |ptr, inner_bytes|

-   bytes.try_into() == Ok(ptr) && mem_own(ptr, inner_bytes) && T.own(inner_bytes)
+   bytes.try_into() == Ok(ptr) && ptr.points_to(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(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 +164,9 @@ 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(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(inner_bytes) && T.own(inner_bytes))

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


@@ -195,7 +197,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((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`).


@@ -233,7 +235,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(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 +243,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(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 +272,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_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 +296,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(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 +313,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(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.