calrify unfreeze-on-write

diff --git a/ralf/_posts/2018-11-16-stacked-borrows-implementation.md b/ralf/_posts/2018-11-16-stacked-borrows-implementation.md
index c1c02743bd85bb0b7b6634f122b8d75ae7e89b05..df60719f4d7fb9f190c94fa3e517a31a6707e8d8 100644 (file)
--- a/ralf/_posts/2018-11-16-stacked-borrows-implementation.md
+++ b/ralf/_posts/2018-11-16-stacked-borrows-implementation.md
@@ -375,8 +375,9 @@ perform the following operations on all locations affected by the access:
 
 1. If the location is frozen and this is a read access, nothing happens (even
    if the tag is `Uniq`).
 
 1. If the location is frozen and this is a read access, nothing happens (even
    if the tag is `Uniq`).

-2. Unfreeze the location (set `frozen_since` to `None`).  Either the location is
-   already unfrozen, or this is a write.
+2. Otherwise, if this is a write access, unfreeze the location (set
+   `frozen_since` to `None`).  (If this is a read access and we come here, the
+   location is already unfrozen.)

 3. Pop the stack until the top item matches the tag of the pointer.
     - A `Uniq` item matches a `Uniq` tag with the same ID.
     - A `Shr` item matches any `Shr` tag (with or without timestamp).
 3. Pop the stack until the top item matches the tag of the pointer.
     - A `Uniq` item matches a `Uniq` tag with the same ID.
     - A `Shr` item matches any `Shr` tag (with or without timestamp).