add camera-ready version of itree-program-logic paper

[web.git] / personal / _posts / 2018-11-16-stacked-borrows-implementation.md

diff --git a/personal/_posts/2018-11-16-stacked-borrows-implementation.md b/personal/_posts/2018-11-16-stacked-borrows-implementation.md
index dbea705eefbe4d9e9518723e9433e9b58901a63d..64f9e3172ad286a0642eb7238b4f5f2f232fad3c 100644 (file)
--- a/personal/_posts/2018-11-16-stacked-borrows-implementation.md
+++ b/personal/_posts/2018-11-16-stacked-borrows-implementation.md
@@ -497,7 +497,7 @@ refine these instructions later) on all locations covered by the reference
 3. Perform the actions that would also happen when an actual access happens
    through this reference (for shared references a read access, for mutable
    references a write access).
-4. Check if the new tag is `Shr(Some(t))` and the location is inside an `UnsafeCell`.
+4. Check if the new tag is `Shr(Some(t))` and the location is *not* inside an `UnsafeCell`.
     - If both conditions apply, freeze the location with timestamp `t`.  If it
       is already frozen, do nothing.
     - Otherwise, push a new item onto the stack: `Shr` if the tag is a `Shr(_)`,
@@ -669,9 +669,8 @@ executed on all locations covered by the reference, according to `size_of_val`):
    Now the location cannot be frozen any more: If the fresh tag is `Uniq`, we
    just unfroze; if the fresh tag is `Shr` and the location was already frozen,
    then the redundancy check (step 3) would have kicked in.
-5. Check if the new tag is `Shr(Some(t))` and the location is inside an `UnsafeCell`.
-    - If both conditions apply, freeze the location with timestamp `t`.  If it
-      is already frozen, do nothing.
+5. Check if the new tag is `Shr(Some(t))` and the location is *not* inside an `UnsafeCell`.
+    - If both conditions apply, freeze the location with timestamp `t`.
     - Otherwise, push a new item onto the stack: `Shr` if the tag is a `Shr(_)`,
       `Uniq(id)` if the tag is `Uniq(id)`.