Skip to content

Commit 7cf91ad

Browse files
committed
Auto merge of #3415 - JoJoDeveloping:tree-borrows-initialized-root, r=RalfJung
Tree Borrows: Make tree root always be initialized This PR fixes a slight annoyance we discovered while formally proving that certain optimizations are sound with Tree Borrows. In particular... (copied from the commit message): There should never be an `Active` but not initialized node in the borrow tree. If such a node exists, and if it has a protector, then on a foreign read, it could become disabled. This leads to some problems when formally proving that read moving optimizations are sound. The root node is the only node for which this can happen, since all other nodes can only become `Active` when actually used. But special-casing the root node here is annoying to reason about, everything becomes much nicer if we can simply say that *all* `Active` nodes must be initialized. This requires making the root node default-initialized. This is also more intuitive, since the root arguably becomes initialized during the allocation, which can be considered a write.
2 parents 2376e3f + 5b208c4 commit 7cf91ad

File tree

3 files changed

+40
-20
lines changed

3 files changed

+40
-20
lines changed

src/borrow_tracker/tree_borrows/perms.rs

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -181,8 +181,12 @@ impl Permission {
181181
pub fn is_initial(&self) -> bool {
182182
self.inner.is_initial()
183183
}
184+
/// Check if `self` is the terminal state of a pointer (is `Disabled`).
185+
pub fn is_disabled(&self) -> bool {
186+
self.inner == Disabled
187+
}
184188

185-
/// Default initial permission of the root of a new tree.
189+
/// Default initial permission of the root of a new tree at inbounds positions.
186190
/// Must *only* be used for the root, this is not in general an "initial" permission!
187191
pub fn new_active() -> Self {
188192
Self { inner: Active }
@@ -193,11 +197,17 @@ impl Permission {
193197
Self { inner: Reserved { ty_is_freeze, conflicted: false } }
194198
}
195199

196-
/// Default initial permission of a reborrowed shared reference
200+
/// Default initial permission of a reborrowed shared reference.
197201
pub fn new_frozen() -> Self {
198202
Self { inner: Frozen }
199203
}
200204

205+
/// Default initial permission of the root of a new tre at out-of-bounds positions.
206+
/// Must *only* be used for the root, this is not in general an "initial" permission!
207+
pub fn new_disabled() -> Self {
208+
Self { inner: Disabled }
209+
}
210+
201211
/// Apply the transition to the inner PermissionPriv.
202212
pub fn perform_access(
203213
kind: AccessKind,

src/borrow_tracker/tree_borrows/tree.rs

Lines changed: 26 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,7 @@ pub(super) struct LocationState {
4242
/// protected, that is *not* the case for uninitialized locations. Instead we just have a latent
4343
/// "future initial permission" of `Disabled`, causing UB only if an access is ever actually
4444
/// performed.
45+
/// Note that the tree root is also always initialized, as if the allocation was a write access.
4546
initialized: bool,
4647
/// This pointer's current permission / future initial permission.
4748
permission: Permission,
@@ -55,17 +56,18 @@ pub(super) struct LocationState {
5556
}
5657

5758
impl LocationState {
58-
/// Default initial state has never been accessed and has been subjected to no
59-
/// foreign access.
60-
fn new(permission: Permission) -> Self {
59+
/// Constructs a new initial state. It has neither been accessed, nor been subjected
60+
/// to any foreign access yet.
61+
/// The permission is not allowed to be `Active`.
62+
fn new_uninit(permission: Permission) -> Self {
63+
assert!(permission.is_initial() || permission.is_disabled());
6164
Self { permission, initialized: false, latest_foreign_access: None }
6265
}
6366

64-
/// Record that this location was accessed through a child pointer by
65-
/// marking it as initialized
66-
fn with_access(mut self) -> Self {
67-
self.initialized = true;
68-
self
67+
/// Constructs a new initial state. It has not yet been subjected
68+
/// to any foreign access. However, it is already marked as having been accessed.
69+
fn new_init(permission: Permission) -> Self {
70+
Self { permission, initialized: true, latest_foreign_access: None }
6971
}
7072

7173
/// Check if the location has been initialized, i.e. if it has
@@ -238,8 +240,10 @@ pub(super) struct Node {
238240
/// If the pointer was reborrowed, it has children.
239241
// FIXME: bench to compare this to FxHashSet and to other SmallVec sizes
240242
pub children: SmallVec<[UniIndex; 4]>,
241-
/// Either `Reserved` or `Frozen`, the permission this tag will be lazily initialized
242-
/// to on the first access.
243+
/// Either `Reserved`, `Frozen`, or `Disabled`, it is the permission this tag will
244+
/// lazily be initialized to on the first access.
245+
/// It is only ever `Disabled` for a tree root, since the root is initialized to `Active` by
246+
/// its own separate mechanism.
243247
default_initial_perm: Permission,
244248
/// Some extra information useful only for debugging purposes
245249
pub debug_info: NodeDebugInfo,
@@ -444,12 +448,14 @@ impl<'tree> TreeVisitor<'tree> {
444448
impl Tree {
445449
/// Create a new tree, with only a root pointer.
446450
pub fn new(root_tag: BorTag, size: Size, span: Span) -> Self {
447-
let root_perm = Permission::new_active();
451+
// The root has `Disabled` as the default permission,
452+
// so that any access out of bounds is invalid.
453+
let root_default_perm = Permission::new_disabled();
448454
let mut tag_mapping = UniKeyMap::default();
449455
let root_idx = tag_mapping.insert(root_tag);
450456
let nodes = {
451457
let mut nodes = UniValMap::<Node>::default();
452-
let mut debug_info = NodeDebugInfo::new(root_tag, root_perm, span);
458+
let mut debug_info = NodeDebugInfo::new(root_tag, root_default_perm, span);
453459
// name the root so that all allocations contain one named pointer
454460
debug_info.add_name("root of the allocation");
455461
nodes.insert(
@@ -458,15 +464,19 @@ impl Tree {
458464
tag: root_tag,
459465
parent: None,
460466
children: SmallVec::default(),
461-
default_initial_perm: root_perm,
467+
default_initial_perm: root_default_perm,
462468
debug_info,
463469
},
464470
);
465471
nodes
466472
};
467473
let rperms = {
468474
let mut perms = UniValMap::default();
469-
perms.insert(root_idx, LocationState::new(root_perm).with_access());
475+
// We manually set it to `Active` on all in-bounds positions.
476+
// We also ensure that it is initalized, so that no `Active` but
477+
// not yet initialized nodes exist. Essentially, we pretend there
478+
// was a write that initialized these to `Active`.
479+
perms.insert(root_idx, LocationState::new_init(Permission::new_active()));
470480
RangeMap::new(size, perms)
471481
};
472482
Self { root: root_idx, nodes, rperms, tag_mapping }
@@ -500,7 +510,7 @@ impl<'tcx> Tree {
500510
// Register new_tag as a child of parent_tag
501511
self.nodes.get_mut(parent_idx).unwrap().children.push(idx);
502512
// Initialize perms
503-
let perm = LocationState::new(default_initial_perm).with_access();
513+
let perm = LocationState::new_init(default_initial_perm);
504514
for (_perms_range, perms) in self.rperms.iter_mut(reborrow_range.start, reborrow_range.size)
505515
{
506516
perms.insert(idx, perm);
@@ -599,7 +609,7 @@ impl<'tcx> Tree {
599609
-> Result<ContinueTraversal, TransitionError> {
600610
let NodeAppArgs { node, mut perm, rel_pos } = args;
601611

602-
let old_state = perm.or_insert(LocationState::new(node.default_initial_perm));
612+
let old_state = perm.or_insert(LocationState::new_uninit(node.default_initial_perm));
603613

604614
match old_state.skip_if_known_noop(access_kind, rel_pos) {
605615
ContinueTraversal::SkipChildren => return Ok(ContinueTraversal::SkipChildren),

src/borrow_tracker/tree_borrows/tree/tests.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -516,11 +516,11 @@ mod spurious_read {
516516
let source = LocStateProtPair {
517517
xy_rel: RelPosXY::MutuallyForeign,
518518
x: LocStateProt {
519-
state: LocationState::new(Permission::new_frozen()).with_access(),
519+
state: LocationState::new_init(Permission::new_frozen()),
520520
prot: true,
521521
},
522522
y: LocStateProt {
523-
state: LocationState::new(Permission::new_reserved(false)),
523+
state: LocationState::new_uninit(Permission::new_reserved(false)),
524524
prot: true,
525525
},
526526
};

0 commit comments

Comments
 (0)