Apply suggestions from code review

Co-authored-by: Ralf Jung <[email protected]>

Author: JoJoDeveloping

wip/tree-borrows.md

@@ -21,31 +21,32 @@ Tree Borrows maintains a tree for each allocation. Each pointer has a tag, that
 Each node, for each offset/byte in the allocation, tracks a permission. The permission is per-byte, i.e. each byte has its own independent permission.
 The permission evolves according to a state machine, which depends on the access (read/write), the relation between accessed and affected node (local/foreign), the current state, and whether the current node is protected by a protector.
 
-There is also an "initialized" tracking which makes protectors behave different on offsets "out of bounds" of a retag, that have not yet been accessed.
+There is also an "accessed" bit in each node for each byte, tracking whether this byte has already been accessed by a pointer tagged with this node.
+This is relevant for protectors, because only "accessed" nodes are being protected.
 These differences are not reflected in the state machines in the paper, we refer to the MiniRust implementation for the full details.
 
 
 ### Differences between MiniRust and Miri
 MiniRust includes an idealized implementation of Tree Borrows, intended for easy readability.
- In particular, it models provenance/tags as tree addresses, which uniquely identify a node in the borrow tree. Miri however uses unique integer IDs, with the Tree being tracked more implicitly as maps/relations between these IDs. The precise implementation of the tree is an implementation detail and not relevant for the semantics.
+In particular, it models provenance/tags as tree addresses, which uniquely identify a node in the borrow tree. Miri however uses unique integer IDs, with the Tree being tracked more implicitly as maps/relations between these IDs. The precise implementation of the tree is an implementation detail and not relevant for the semantics.
 
-Besides this representation difference, Miri also includes a number of optimizations that make Tree Borrows have acceptable performance. These include
+Besides this representation difference, Miri also includes a number of optimizations that make Tree Borrows have acceptable performance. These include:
 * skipping nodes based on past foreign accesses, exploiting idempotence properties in the state machine
 * garbage collection of unused references, which allows shrinking trees
 * skipping nodes based on the permissions found therein
 
 ## Concepts Inherited From Stacked Borrows
 
 ### Retags
-Tree Borrows has retags happen in the same place as Stacked Borrows. But note that Tree Borrows treats raw pointer retags as NOPs, i.e. it does not attempt to track these.
+Tree Borrows has retags happen in the same place as Stacked Borrows. But note that Tree Borrows treats raw pointer retags as NOPs, i.e. it does not distinguish a raw pointer from the references it is derived from.
 
 ### Protectors
-Like Stacked Borrows, Tree Borrows has protectors. These serve to ensure that references remain live throughout a function. Protectors are strong and weak, as in SB, and they protect the same places in the same way.
+Like Stacked Borrows, Tree Borrows has protectors. These serve to ensure that references remain live throughout a function. Protectors come in "strong" and "weak" forms, as in SB, and they protect the same places in the same way.
 
 ### Implicit Reads and Writes
 Like Stacked Borrows, Tree Borrows performs implicit accesses as part of retags. Unlike Stacked Borrows, these are always reads, even for `&mut` references.
 
-A new concept in TB are protector end accesses. These can be writes. See the section on "protector end semantics" in the paper for more info.
+A new concept in TB are implicit protector end accesses. These can be writes. See the section on "protector end semantics" in the paper for more info.
 
 ### UnsafeCell tracking
 Like Stacked Borrows, Tree Borrows tracks where there are UnsafeCells, and treats these bytes differently from other bytes. UnsafeCells are tracked in structs and tuple fields, but enums are not inspected further.
@@ -61,5 +62,5 @@ The following is a list of things that are _not_ UB in Tree Borrows. Some people
 * Tree Borrows does not initially consider `&mut` references writable, it only does so after the first write. In practice, this might mean that optimizations moving writes up above the first write are forbidden.
 
 ## Other problems
-* The interaction of protector end writes with the data race model is not fully thought out.
+* The interaction of protector end writes with the data race model is not fully resolved.
 * Finding a good model of exposed provenance in Tree Borrows (that does not use angelic nondeterminism) is an open research question. Until then, Tree Borrows does not support `-Zmiri-permissive-provenance`.