From 73383fdc4f0a5c1287d8f6c3434bd880b32a5ab2 Mon Sep 17 00:00:00 2001
From: Johannes Hostert <jhostert@ethz.ch>
Date: Fri, 23 Aug 2024 22:19:05 +0200
Subject: [PATCH] try optimizing accesses on large trees by ignoring subtrees
 if the access would mostly be a NOP

---
 src/borrow_tracker/tree_borrows/perms.rs |  4 ++++
 src/borrow_tracker/tree_borrows/tree.rs  | 26 +++++++++++++++++++++++-
 2 files changed, 29 insertions(+), 1 deletion(-)

diff --git a/src/borrow_tracker/tree_borrows/perms.rs b/src/borrow_tracker/tree_borrows/perms.rs
index 1d0b5dc930..b0b42de968 100644
--- a/src/borrow_tracker/tree_borrows/perms.rs
+++ b/src/borrow_tracker/tree_borrows/perms.rs
@@ -236,6 +236,10 @@ impl Permission {
     pub fn is_active(&self) -> bool {
         self.inner == Active
     }
+    /// Check if `self` is the never-allow-writes-again state of a pointer (is `Frozen`).
+    pub fn is_frozen(&self) -> bool {
+        self.inner == Frozen
+    }
 
     /// Default initial permission of the root of a new tree at inbounds positions.
     /// Must *only* be used for the root, this is not in general an "initial" permission!
diff --git a/src/borrow_tracker/tree_borrows/tree.rs b/src/borrow_tracker/tree_borrows/tree.rs
index 116cdf0d40..0b84c9d274 100644
--- a/src/borrow_tracker/tree_borrows/tree.rs
+++ b/src/borrow_tracker/tree_borrows/tree.rs
@@ -173,7 +173,7 @@ impl LocationState {
         rel_pos: AccessRelatedness,
     ) -> ContinueTraversal {
         if rel_pos.is_foreign() {
-            let new_access_noop = match (self.latest_foreign_access, access_kind) {
+            let mut new_access_noop = match (self.latest_foreign_access, access_kind) {
                 // Previously applied transition makes the new one a guaranteed
                 // noop in the two following cases:
                 // (1) justified by `foreign_read_is_noop_after_foreign_write`
@@ -185,6 +185,30 @@ impl LocationState {
                 // need to be applied to this subtree.
                 _ => false,
             };
+            if self.permission.is_disabled() {
+                // A foreign access to a `Disabled` tag will have almost no observable effect.
+                // It's a theorem that `Disabled` node have no protected initialized children,
+                // and so this foreign access will never trigger any protector.
+                // Further, the children will never be able to read or write again, since they
+                // have a `Disabled` parents. Even further, all children of `Disabled` are one
+                // of `ReservedIM`, `Disabled`, or a not-yet-accessed "lazy" permission thing.
+                // The two former are already invariant under all foreign accesses, and for
+                // the latter it does not really matter, since they can not be used/initialized
+                // due to having a protected parent. So this only affects diagnostics, but the
+                // blocking write will still be identified directly, just at a different tag.
+                new_access_noop = true;
+            }
+            if self.permission.is_frozen() && access_kind == AccessKind::Read {
+                // A foreign read to a `Frozen` tag will have almost no observable effect.
+                // It's a theorem that `Frozen` nodes have no active children, so all children
+                // already survive foreign reads. Foreign reads in general have almost no
+                // effect, the only further thing they could do is make protected `Reserved`
+                // nodes become conflicted, i.e. make them reject child writes for the further
+                // duration of their protector. But such a child write is already rejected
+                // because this node is frozen. So this only affects diagnostics, but the
+                // blocking read will still be identified directly, just at a different tag.
+                new_access_noop = true;
+            }
             if new_access_noop {
                 // Abort traversal if the new transition is indeed guaranteed
                 // to be noop.