From 0c401184a0c74f4c0bfa323dbf935fb314c26cf3 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 10 Apr 2018 19:24:35 +0200 Subject: [PATCH] fix some typos --- .../2018-04-10-safe-intrusive-collections-with-pinning.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/personal/_posts/2018-04-10-safe-intrusive-collections-with-pinning.md b/personal/_posts/2018-04-10-safe-intrusive-collections-with-pinning.md index 93cbad5..923480e 100644 --- a/personal/_posts/2018-04-10-safe-intrusive-collections-with-pinning.md +++ b/personal/_posts/2018-04-10-safe-intrusive-collections-with-pinning.md @@ -20,7 +20,7 @@ This builds on the formal notation I introduced in my last post. Finally, I will discuss a variant of our "running example" intrusive collection that combines shared references and pinning. 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. -Hiwever, this extended model will actually call for a change to the `Pin` API (or rather, for a revert to an earlier version). +However, this extended model will actually call for a change to the `Pin` API (or rather, for a revert to an earlier version). (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.) @@ -220,13 +220,13 @@ What would *not* be sound is adding a way to obtain a `Pin` reference *into* a ` 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. (Linear reasoning is typically used to prove properties like memory-leak-freedom.) -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`? +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`? Pinning and calling `drop` are entirely orthogonal concerns! Well, this is certainly true for general leak-freedom. However, the guarantee we are after here is that `drop` will be called *if this memory ever gets deallocated*. So, the guarantee is tied to a particular spot in memory---a concept that only makes sense if data is pinned to begin with! 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. -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). +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). 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! 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). @@ -350,7 +350,7 @@ We are just concerned with *safety* here: When memory is pinned, it is only safe One important observation is that if we did *not* remove the entry from the collection, we would be unable to satisfy the postcondition! This matches the fact that our entire collection would be unsound if we removed the `Entry::drop`. In other words, if we do *not* implement `Drop`, this actually incurs a proof obligation! -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()`. +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()`. This is the part that would go wrong if we were to remove `Entry::drop`. It seems rather funny that *not* implementing a trait incurs a proof obligation, but there's also nothing fundamentally wrong with that idea. -- 2.30.2