typo
[web.git] / ralf / _posts / 2018-08-07-stacked-borrows.md
index 6787754..0314fbb 100644 (file)
@@ -1,6 +1,7 @@
 ---
 title: "Stacked Borrows: An Aliasing Model For Rust"
 categories: internship rust
+forum: https://internals.rust-lang.org/t/stacked-borrows-an-aliasing-model-for-rust/8153
 ---
 
 In this post, I am proposing "Stacked Borrows": A set of rules defining which kinds of aliasing are allowed in Rust.
@@ -12,7 +13,7 @@ The model I am proposing here is by far not the first attempt at giving a defini
 <!-- MORE -->
 
 But before I delve into my latest proposal, I want to briefly discuss a key difference between my previous model and this one:
-"Types as Contracts" was a fully "validity"-based model, while "Stacked Borrows" is (to some extend) "access"-based.
+"Types as Contracts" was a fully "validity"-based model, while "Stacked Borrows" is (to some extent) "access"-based.
 
 ## 1 Validity-based vs. Access-based
 
@@ -30,7 +31,7 @@ Validity-based models have several advantages: Eager checking means we can typic
 
 However, in Rust, we cannot talk about references and whether the are valid at their given type without talking about lifetimes.
 With "Types as Contracts", the exact place where a lifetime ended turned out to be really important.
-Not only did this make the specification complex and hard to understand; the implementation in [Miri]({% post_url 2017-06-06-MIR-semantics %}) also had to actively work against the compiler's general intention to forget about lifetimes as early as possible.
+Not only did this make the specification complex and hard to understand; the implementation in Miri also had to actively work against the compiler's general intention to forget about lifetimes as early as possible.
 With non-lexical lifetimes, the "end" of a lifetime is not even so clearly defined any more.
 
 ## 2 Stacking Borrows
@@ -228,7 +229,7 @@ With this additional step, it is now easy to argue that `demo4` above is UB when
 After using `x`, we know it is active.
 Next we use and activate `y`, which has to pop `Uniq(x)` as they have distinct tags.
 Finally, we use `x` again even though it is no longer in the stack, triggering UB.
-(A `Uniq` is only veer pushed when it is created, so it is never in the stack more than once.)
+(A `Uniq` is only ever pushed when it is created, so it is never in the stack more than once.)
 
 ### 4.2 Barriers
 
@@ -404,7 +405,7 @@ This is where the code gets more "pseudo" and less Rust. ;)
 For each of these operation, we iterate over all affected locations; let us call the loop variable `loc` of type `MemoryByte`.
 We also have a variable `tag` with the tag of the pointer we are operating on (loading, or storing, or casting to a raw pointer, ...).
 
-Moreover, we have a boolean variable `in_unsafe_cell` indicating whether, according to the type of the pointer, the location we are currently working on is covered by an [`UnsafeCell`](https://doc.rust-lang.org/beta/std/cell/struct.UnsafeCell.html).
+Moreover, we have a boolean variable `in_unsafe_cell` indicating whether, according to the type of the pointer, the location we are currently working on is covered by an [`UnsafeCell`](https://doc.rust-lang.org/stable/std/cell/struct.UnsafeCell.html).
 (This realizes the conditions checking whether we have interior mutability or not.)
 For example, in `&Cell<i32>`, all 4 locations are inside an `UnsafeCell`.
 However, in `&(i32, Cell<i32>)`, only the last 4 of the 8 covered locations are inside an `UnsafeCell`.
@@ -464,4 +465,4 @@ I hope to explore this question further in the following weeks by implementing a
 It is just easier to answer these questions when you do not have to *manually* reevaluate all examples after every tiny change.
 However, I can always use more examples, so if you think you found some interesting or surprising corner case, please let me know!
 
-<!-- As always, if you have any questions or comments, feel free to [ask in the forums](). -->
+As always, if you have any questions or comments, feel free to [ask in the forums](https://internals.rust-lang.org/t/stacked-borrows-an-aliasing-model-for-rust/8153).