Skip to content

Commit

Permalink
Tree Borrows: Make tree root always be Active and initialized
Browse files Browse the repository at this point in the history
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-reordering 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 ini-
tialized during the allocation, which can be considered a write.
  • Loading branch information
JoJoDeveloping committed Mar 26, 2024
1 parent 878fa90 commit 07bbebb
Show file tree
Hide file tree
Showing 3 changed files with 37 additions and 18 deletions.
9 changes: 9 additions & 0 deletions src/borrow_tracker/tree_borrows/perms.rs
Expand Up @@ -181,6 +181,10 @@ impl Permission {
pub fn is_initial(&self) -> bool {
self.inner.is_initial()
}
/// Check if `self` is the terminal state of a pointer (is `Disabled`).
pub fn is_disabled(&self) -> bool {
self.inner == Disabled
}

/// Default initial permission of the root of a new tree.
/// Must *only* be used for the root, this is not in general an "initial" permission!
Expand All @@ -198,6 +202,11 @@ impl Permission {
Self { inner: Frozen }
}

/// Default initial permission of the root node at out-of-bounds positions
pub fn new_disabled() -> Self {
Self { inner: Disabled }
}

/// Apply the transition to the inner PermissionPriv.
pub fn perform_access(
kind: AccessKind,
Expand Down
42 changes: 26 additions & 16 deletions src/borrow_tracker/tree_borrows/tree.rs
Expand Up @@ -42,6 +42,7 @@ pub(super) struct LocationState {
/// protected, that is *not* the case for uninitialized locations. Instead we just have a latent
/// "future initial permission" of `Disabled`, causing UB only if an access is ever actually
/// performed.
/// Note that the tree root is also always initialized, as if the allocation was a write access.
initialized: bool,
/// This pointer's current permission / future initial permission.
permission: Permission,
Expand All @@ -55,17 +56,18 @@ pub(super) struct LocationState {
}

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

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

/// Check if the location has been initialized, i.e. if it has
Expand Down Expand Up @@ -238,8 +240,10 @@ pub(super) struct Node {
/// If the pointer was reborrowed, it has children.
// FIXME: bench to compare this to FxHashSet and to other SmallVec sizes
pub children: SmallVec<[UniIndex; 4]>,
/// Either `Reserved` or `Frozen`, the permission this tag will be lazily initialized
/// to on the first access.
/// Either `Reserved`, `Frozen`, or `Disabled`, it is the permission this tag will
/// lazily be initialized to on the first access.
/// It is only ever `Disabled` for a tree root, since the root is initialized to `Active` by
/// its own separate mechanism.
default_initial_perm: Permission,
/// Some extra information useful only for debugging purposes
pub debug_info: NodeDebugInfo,
Expand Down Expand Up @@ -444,12 +448,14 @@ impl<'tree> TreeVisitor<'tree> {
impl Tree {
/// Create a new tree, with only a root pointer.
pub fn new(root_tag: BorTag, size: Size, span: Span) -> Self {
let root_perm = Permission::new_active();
// the root has `Disabled` as the default permission,
// so that any access out of bounds is invalid
let root_default_perm = Permission::new_disabled();
let mut tag_mapping = UniKeyMap::default();
let root_idx = tag_mapping.insert(root_tag);
let nodes = {
let mut nodes = UniValMap::<Node>::default();
let mut debug_info = NodeDebugInfo::new(root_tag, root_perm, span);
let mut debug_info = NodeDebugInfo::new(root_tag, root_default_perm, span);
// name the root so that all allocations contain one named pointer
debug_info.add_name("root of the allocation");
nodes.insert(
Expand All @@ -458,15 +464,19 @@ impl Tree {
tag: root_tag,
parent: None,
children: SmallVec::default(),
default_initial_perm: root_perm,
default_initial_perm: root_default_perm,
debug_info,
},
);
nodes
};
let rperms = {
let mut perms = UniValMap::default();
perms.insert(root_idx, LocationState::new(root_perm).with_access());
// we manually set it to `Active` on all in-bounds positions.
// we also ensure that it is initalized, so that no `Active` but
// not yet initialized nodes exist. Essentially, we pretend there
// was a write that initialized these to `Active`.
perms.insert(root_idx, LocationState::new_init(Permission::new_active()));
RangeMap::new(size, perms)
};
Self { root: root_idx, nodes, rperms, tag_mapping }
Expand Down Expand Up @@ -500,7 +510,7 @@ impl<'tcx> Tree {
// Register new_tag as a child of parent_tag
self.nodes.get_mut(parent_idx).unwrap().children.push(idx);
// Initialize perms
let perm = LocationState::new(default_initial_perm).with_access();
let perm = LocationState::new_init(default_initial_perm);
for (_perms_range, perms) in self.rperms.iter_mut(reborrow_range.start, reborrow_range.size)
{
perms.insert(idx, perm);
Expand Down Expand Up @@ -599,7 +609,7 @@ impl<'tcx> Tree {
-> Result<ContinueTraversal, TransitionError> {
let NodeAppArgs { node, mut perm, rel_pos } = args;

let old_state = perm.or_insert(LocationState::new(node.default_initial_perm));
let old_state = perm.or_insert(LocationState::new_uninit(node.default_initial_perm));

match old_state.skip_if_known_noop(access_kind, rel_pos) {
ContinueTraversal::SkipChildren => return Ok(ContinueTraversal::SkipChildren),
Expand Down
4 changes: 2 additions & 2 deletions src/borrow_tracker/tree_borrows/tree/tests.rs
Expand Up @@ -516,11 +516,11 @@ mod spurious_read {
let source = LocStateProtPair {
xy_rel: RelPosXY::MutuallyForeign,
x: LocStateProt {
state: LocationState::new(Permission::new_frozen()).with_access(),
state: LocationState::new_init(Permission::new_frozen()),
prot: true,
},
y: LocStateProt {
state: LocationState::new(Permission::new_reserved(false)),
state: LocationState::new_uninit(Permission::new_reserved(false)),
prot: true,
},
};
Expand Down

0 comments on commit 07bbebb

Please sign in to comment.