Skip to content

Commit

Permalink
Merge pull request #4008 from JoJoDeveloping/tb-access-state-based-sk…
Browse files Browse the repository at this point in the history
…ipping

[TB Optimization] Skip subtrees based on the subtree's root node's permissions
  • Loading branch information
RalfJung authored Dec 11, 2024
2 parents 994802c + c387247 commit f0fe74f
Show file tree
Hide file tree
Showing 4 changed files with 88 additions and 1 deletion.
4 changes: 4 additions & 0 deletions src/borrow_tracker/tree_borrows/perms.rs
Original file line number Diff line number Diff line change
Expand Up @@ -237,6 +237,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!
Expand Down
25 changes: 24 additions & 1 deletion src/borrow_tracker/tree_borrows/tree.rs
Original file line number Diff line number Diff line change
Expand Up @@ -153,8 +153,31 @@ impl LocationState {
) -> ContinueTraversal {
if rel_pos.is_foreign() {
let happening_now = IdempotentForeignAccess::from_foreign(access_kind);
let new_access_noop =
let mut new_access_noop =
self.idempotent_foreign_access.can_skip_foreign_access(happening_now);
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.
// (Intuition: You're either protected initialized, and thus can't become Disabled
// or you're already Disabled protected, but not initialized, and then can't
// become initialized since that requires a child access, which Disabled blocks.)
// Further, the children will never be able to read or write again, since they
// have a `Disabled` parent. So this only affects diagnostics, such that 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 access is indeed guaranteed
// to be noop.
Expand Down
29 changes: 29 additions & 0 deletions tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
//@compile-flags: -Zmiri-tree-borrows -Zmiri-provenance-gc=0

// Shows the effect of the optimization of #4008.
// The diagnostics change, but not the error itself.

// When this method is called, the tree will be a single line and look like this,
// with other_ptr being the root at the top
// other_ptr = root : Active
// intermediary : Frozen // an intermediary node
// m : Reserved
fn write_to_mut(m: &mut u8, other_ptr: *const u8) {
unsafe {
std::hint::black_box(*other_ptr);
}
// In line 17 above, m should have become Reserved (protected) so that this write is impossible.
// However, that does not happen because the read above is not forwarded to the subtree below
// the Frozen intermediary node. This does not affect UB, however, because the Frozen that blocked
// the read already prevents any child writes.
*m = 42; //~ERROR: /write access through .* is forbidden/
}

fn main() {
let root = 42u8;
unsafe {
let intermediary = &root;
let data = &mut *(core::ptr::addr_of!(*intermediary) as *mut u8);
write_to_mut(data, core::ptr::addr_of!(root));
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
error: Undefined Behavior: write access through <TAG> at ALLOC[0x0] is forbidden
--> tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC
|
LL | *m = 42;
| ^^^^^^^ write access through <TAG> at ALLOC[0x0] is forbidden
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
= help: the accessed tag <TAG> is a child of the conflicting tag <TAG>
= help: the conflicting tag <TAG> has state Frozen which forbids this child write access
help: the accessed tag <TAG> was created here
--> tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC
|
LL | fn write_to_mut(m: &mut u8, other_ptr: *const u8) {
| ^
help: the conflicting tag <TAG> was created here, in the initial state Frozen
--> tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC
|
LL | let intermediary = &root;
| ^^^^^
= note: BACKTRACE (of the first span):
= note: inside `write_to_mut` at tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC
note: inside `main`
--> tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC
|
LL | write_to_mut(data, core::ptr::addr_of!(root));
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

error: aborting due to 1 previous error

0 comments on commit f0fe74f

Please sign in to comment.