Merge pull request #612 from JoJoDeveloping/tbwip-2

TB update

Author: RalfJung

wip/tree-borrows.md

@@ -8,6 +8,7 @@ Changes since publication of the paper:
 
 * Interior-Mutable shared references are no longer treated like raw pointers, instead they use the new `Cell` permission. This permission allows all foreign and local accesses.
 * Mirroring Stacked Borrows, structs which contain an UnsafeCell now have that UnsafeCell's position tracked more finely-grained. It is no longer sufficient to just have an UnsafeCell somewhere in a struct to mark this as being interior-mutable everywhere.
+* The state machine was refactored to eliminate the `accessed` bit. This mostly affects the protected state machine. This changed no behavior but makes it less obvious how the current MiniRust implementation relates to the paper. See [this PR](https://github.com/minirust/minirust/pull/276) and also [this rendering of the new state machine(s)](https://github.com/user-attachments/files/23404334/figures2.pdf).
 
 ## MiniRust
 
@@ -22,9 +23,9 @@ 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 "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.
+The state machine differs for protected and unprotected nodes.
+For protected nodes, some states additionally track whether this byte was "accessed" which formally means that the state exists twice (e.g. `Frozen` and `FrozenL`).
+The protected state machine of Figure 3 in the paper only shows those that are considered accessed; we refer to the MiniRust implementation for the full details.
 
 
 ### Differences between MiniRust and Miri
@@ -37,6 +38,10 @@ Besides this representation difference, Miri also includes a number of optimizat
 * garbage collection of unused references, which allows shrinking trees
 * skipping nodes based on the permissions found therein
 
+Additionally, the above-mentioned "refactor to eliminate the `accessed` bit" has not yet happened in Miri.
+
+Furthermore, Miri now has experimental support for `-Zmiri-permissive-provenance` with Tree Borrows.
+
 ## Concepts Inherited From Stacked Borrows
 
 ### Retags
@@ -49,7 +54,7 @@ Like Stacked Borrows, Tree Borrows has protectors. These serve to ensure that re
 
 ### 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.
+Like Stacked Borrows, Tree Borrows performs implicit accesses as part of retags. Unlike Stacked Borrows, these are always reads, even for `&mut` references. (But this might change, see below.)
 
 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.
 
@@ -67,8 +72,9 @@ The following is a list of things that are _not_ UB in Tree Borrows. Some people
 
 * Tree Borrows does _not_ have subobject provenance, meaning that retags do not shrink the set of offsets that a reference can be used to access.
 * 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.
+  Note that there is work currently happening to make this a configurable option, and this option could become the default depending on the fallout of this change. See [#584](https://github.com/rust-lang/unsafe-code-guidelines/issues/584)
 
 ## 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`.
+* The interaction of protector end writes with the data race model is not fully resolved. See [#585](https://github.com/rust-lang/unsafe-code-guidelines/issues/585).
+* In Miri, there is experimental support for Tree Borros with `-Zmiri-permissive-provenance`, but the semantics are not yet fixed and likely to evolve in the future.