user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Tree Borrows: Make tree root always be Active and initialized

Browse source 
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.
This commit is contained in:
Johannes Hostert 2024-03-25 17:35:29 +01:00
parent c4611708bd
commit df73cb710e
No known key found for this signature in database
GPG key ID: 0BA6032B5A38D049
3 changed files with 40 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
View file

@ -181,8 +181,12 @@ 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.
/// 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!
pub fn new_active() -> Self {
Self { inner: Active }
@ -193,11 +197,17 @@ impl Permission {
Self { inner: Reserved { ty_is_freeze, conflicted: false } }
}
/// Default initial permission of a reborrowed shared reference
/// Default initial permission of a reborrowed shared reference.
pub fn new_frozen() -> Self {
Self { inner: Frozen }
}
/// Default initial permission of the root of a new tre at out-of-bounds positions.
/// Must *only* be used for the root, this is not in general an "initial" permission!
pub fn new_disabled() -> Self {
Self { inner: Disabled }
}
/// Apply the transition to the inner PermissionPriv.
pub fn perform_access(
kind: AccessKind,

42
src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
View file

@ -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,
@ -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
@ -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,
@ -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(
@ -458,7 +464,7 @@ impl Tree {
tag: root_tag,
parent: None,
children: SmallVec::default(),
default_initial_perm: root_perm,
default_initial_perm: root_default_perm,
debug_info,
},
);
@ -466,7 +472,11 @@ impl Tree {
};
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 }
@ -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);
@ -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),

4
src/tools/miri/src/borrow_tracker/tree_borrows/tree/tests.rs
View file

@ -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,
},
};