TB: Track permissions on the byte-level #4314

yoctocell · 2025-05-08T08:42:14Z

This makes the tracking of permissions on the byte-level, like in Stacked Borrows, which makes the tracking of interior mutable data more fine-grained.

cc @RalfJung @JoJoDeveloping

src/borrow_tracker/tree_borrows/mod.rs

src/borrow_tracker/tree_borrows/tree.rs

tests/pass/tree_borrows/cell-inside-struct.rs

JoJoDeveloping · 2025-05-12T09:23:29Z

So, how does adding a new node work (and why do we need to call visit_freeze_sensitive three times:

First, you do a read access at the parent node
Then, you add the new node. Note that adding a new node is a per-block operation, not per-access
Then you set the correct permissions for the new node
Then you reset the SIFA thingy (also per-block)
Then you call into the data race model

For Stacked Borrows, there are no per-block operations: each stack at each offset its own stack and completely independent from the other ones at different offsets in the same allocation. So there, more (basically everything) can be moved into the per-offset function.

So what do we do for Tree Borrows? One answer is to combine parent reading, permission setting and data race notifying together. This would be somewhat ugly, because you're constructing a node, while also accessing the tree, and this would only be fine because you're careful to not actually add the node into the children array of its parent so that it's not visited when walking the tree.

Should we do this?

RalfJung · 2025-05-12T14:41:00Z

Ignoring the SIFA thingy since I already forgot how it works, what I think would make sense is to do a single visit_freeze_sensitive where you

do the parent access
do the data race access
prepare a RangeMap<LocationState> of per-location initial states that will later be passed to Tree::new_child

Does that makes sense or is it too ugly as well?

JoJoDeveloping · 2025-05-12T20:04:35Z

That would work. It has to construct an extra RangeMap but presumably this is cheaper than calling visit_freeze_sensitive thrice.
And it requires moving some logic for retags around quite a bit.

RalfJung · 2025-05-12T21:48:49Z

presumably this is cheaper than calling visit_freeze_sensitive thrice.

I'm not sure, but that's at least plausible. I also prefer it conceptually.

Previously, the assert would cause an error if the `RangeMap` was empty.

src/borrow_tracker/tree_borrows/mod.rs

RalfJung

Thanks! This is a lot better.

I don't fully understand the logic around the new perms_map though. It seems like the map is created to cover all the bytes from the beginning of the allocation to the end of the retagged place, which is odd -- it should be either the entire allocation, or just the place. And given that we do not want to actually put anything into the perms map outside the place, I think it should be just the place.

RalfJung · 2025-05-20T12:45:53Z

src/borrow_tracker/tree_borrows/mod.rs

        let mut tree_borrows = alloc_extra.borrow_tracker_tb().borrow_mut();
+        let prot = new_perm.protector.is_some();
+
+        // Store initialized permissions and their corresponding range.


Suggested change

// Store initialized permissions and their corresponding range.

// Store initial permissions and their corresponding range.

RalfJung · 2025-05-20T12:47:31Z

src/borrow_tracker/tree_borrows/mod.rs

+        let NewPermission { freeze_perm, freeze_access, nonfreeze_perm, nonfreeze_access, .. } =
+            new_perm;


Why do you destruct the NewPermission like this here? Seems a bit more clear to say new_perm.<field> everywhere below.

RalfJung · 2025-05-20T12:51:16Z

src/borrow_tracker/tree_borrows/tree.rs

@@ -31,7 +33,7 @@ mod tests;

 /// Data for a single *location*.
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
-pub(super) struct LocationState {
+pub(crate) struct LocationState {


Why does the entire crate now need access to this?

Because the compiler would complain about the visibility of
LocationState being private than new_child. But seems like super
should be enough for new_child, so I will change both of the to super.

RalfJung · 2025-05-20T12:57:57Z

tests/fail/tree_borrows/cell-inside-struct.rs

@@ -0,0 +1,32 @@
+//@compile-flags: -Zmiri-tree-borrows


Suggested change

//@compile-flags: -Zmiri-tree-borrows

//! A version of `cell_inside_struct` that dumps the tree so that we can see what is happening.

//@compile-flags: -Zmiri-tree-borrows

RalfJung · 2025-05-20T12:58:25Z

src/borrow_tracker/tree_borrows/tree.rs

+            for (_perms_range, perms) in
+                self.rperms.iter_mut(Size::from_bytes(start), Size::from_bytes(end - start))
+            {
+                perms.insert(idx, perm);


So this will insert a bunch of Disabled, won't it?

RalfJung · 2025-05-20T13:01:30Z

src/borrow_tracker/tree_borrows/mod.rs

+        let mut perms_map: RangeMap<LocationState> = RangeMap::new(
+            base_offset + ptr_size,
+            LocationState::new_uninit(
+                Permission::new_disabled(),
+                foreign_access_skipping::IdempotentForeignAccess::None,
+            ),
+        );


I think this should be initialized with size ptr_size, and only cover the place we are retagging. That way we can avoid introducing some disabled states here that I don't think we actually want.

RalfJung · 2025-05-20T13:02:50Z

src/borrow_tracker/tree_borrows/tree.rs

        let idx = self.tag_mapping.insert(new_tag);
        let parent_idx = self.tag_mapping.get(&parent_tag).unwrap();
+        let default_initial_perm = perm.freeze_perm;


I don't think this is obviously the right choice. There's an interesting decision to be made here: if I have an &Cell<i32>, should I be allowed to lazily write to surrounding memory? The general consensus, I think, is that the answer is "yes" -- the permission of an &T should default to frozen only if T: Freeze, and should default to non-frozen otherwise.

This should also be covered by a test.

What do you mean with "lazily write to surrounding memory"? Do you have an example in mind?

fn foo(x: &Cell<i32>) { let ptr = x as *const Cell<i32> as *mut _ as *mut i32; ptr.offset(1).write(0); } let arr = [Cell::new(1), Cell::new(1)]; foo(&arr[0]);

This code should be accepted without UB.

Xinglu Chen added 8 commits May 6, 2025 11:10

Track permissions on the byte-level

a36348d

Don't differentiate between Uniform and FreezeSensitive

9e7a2e3

Mark compatible_with_protector as test-only

a3d4a0d

Remove unused functions

6a5a478

Cleanup comments and whitespace

a7b1d7b

Rename freeze_protector to protector

3eed6ff

Update comment

263e083

Fix clippy errors

9dc3e47

RalfJung reviewed May 8, 2025

View reviewed changes

Xinglu Chen added 3 commits May 13, 2025 17:17

Fix assert in iter for RangeMap

9f52d71

Previously, the assert would cause an error if the `RangeMap` was empty.

Suggestions from first round of review

8f7a451

fmt code

a816f9d

JoJoDeveloping reviewed May 19, 2025

View reviewed changes

src/borrow_tracker/tree_borrows/mod.rs Outdated Show resolved Hide resolved

Address nit

d97f94a

RalfJung reviewed May 20, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

TB: Track permissions on the byte-level #4314

TB: Track permissions on the byte-level #4314

yoctocell commented May 8, 2025

JoJoDeveloping commented May 12, 2025

RalfJung commented May 12, 2025

JoJoDeveloping commented May 12, 2025 •

edited

Loading

RalfJung commented May 12, 2025

RalfJung left a comment

RalfJung May 20, 2025

RalfJung May 20, 2025

RalfJung May 20, 2025

yoctocell May 20, 2025

RalfJung May 20, 2025

RalfJung May 20, 2025

RalfJung May 20, 2025

RalfJung May 20, 2025

yoctocell May 20, 2025 •

edited

Loading

RalfJung May 20, 2025 •

edited

Loading

	// Store initialized permissions and their corresponding range.
	// Store initial permissions and their corresponding range.

		let NewPermission { freeze_perm, freeze_access, nonfreeze_perm, nonfreeze_access, .. } =
		new_perm;

	//@compile-flags: -Zmiri-tree-borrows
	//! A version of `cell_inside_struct` that dumps the tree so that we can see what is happening.
	//@compile-flags: -Zmiri-tree-borrows

TB: Track permissions on the byte-level #4314

Are you sure you want to change the base?

TB: Track permissions on the byte-level #4314

Conversation

yoctocell commented May 8, 2025

JoJoDeveloping commented May 12, 2025

RalfJung commented May 12, 2025

JoJoDeveloping commented May 12, 2025 • edited Loading

RalfJung commented May 12, 2025

RalfJung left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

yoctocell May 20, 2025 • edited Loading

Choose a reason for hiding this comment

RalfJung May 20, 2025 • edited Loading

Choose a reason for hiding this comment

JoJoDeveloping commented May 12, 2025 •

edited

Loading

yoctocell May 20, 2025 •

edited

Loading

RalfJung May 20, 2025 •

edited

Loading