line breaks

Author: JoJoDeveloping

wip/tree-borrows.md

@@ -17,6 +17,7 @@ Instead of yet again defining Tree Borrows in prose here, we refer to MiniRust.
 
 
 ### High-level summary
+
 Tree Borrows maintains a tree for each allocation. Each pointer has a tag, that identifies a node in this tree.
 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.
@@ -27,6 +28,7 @@ These differences are not reflected in the state machines in the paper, we refer
 
 
 ### 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.
 
@@ -38,20 +40,25 @@ Besides this representation difference, Miri also includes a number of optimizat
 ## 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 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 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 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.
 
 ### Accesses
+
 Besides for the aforementioned differences in the handling of retags, what counted as a read or write in Stacked Borrows also counts as a read or write in Tree Borrows. These places are not surprising.
 
 ## Imprecisions
@@ -62,5 +69,6 @@ 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 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`.