Skip to content

Commit

Permalink
refactor foreign access skipping
Browse files Browse the repository at this point in the history
  • Loading branch information
JoJoDeveloping committed Nov 19, 2024
1 parent 04630e0 commit bbbec3a
Show file tree
Hide file tree
Showing 5 changed files with 210 additions and 171 deletions.
84 changes: 84 additions & 0 deletions src/borrow_tracker/tree_borrows/foreign_access_skipping.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
use super::AccessKind;
use super::tree::AccessRelatedness;

/// To speed up tree traversals, we want to skip traversing subtrees when we know the traversal will have no effect.
/// This is often the case for foreign accesses, since usually foreign accesses happen several times in a row, but also
/// foreign accesses are idempotent. In particular, see tests `foreign_read_is_noop_after_foreign_write` and `all_transitions_idempotent`.
/// Thus, for each node we keep track of the "strongest idempotent foreign access," (SIFA) i.e. which foreign access can be skipped.
/// This enum represents the kinds of values we store:
/// `LocalAccess` means that the last access was local, and thus the next foreign access needs to happen, it can not be skipped.
/// `ForeignRead` means that we are idempotent under foreign reads, but not (yet) under foreign writes.
/// `ForeignWrite` means that we are idempotent under foreign writes. In other words, this node can be skipped for all foreign accesses.
/// Due to the subtree property of traversals, this also means that all our children can be skipped, which makes this optimization
/// worthwhile. In order for this to work, the invariant for multiple nodes in a tree is that at each location, the SIFA at each
/// child must be stronger than that at the parent. However, note that this is quite invariant, due to retags inserting nodes across
/// the entire range, which can violate this invariant without explicitly causing a local access which would reset things.
/// So this needs to be done manually, thus `ensure_no_stronger_than`, and also the test `permission_sifa_is_correct` in `perms.rs`
#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug, Default)]
pub enum LastForeignAccess {
#[default]
LocalAccess,
ForeignRead,
ForeignWrite,
}

impl LastForeignAccess {
/// Returns true if a node where the strongest idempotent foreign access is `self`
/// can skip the access `happening_next`. Note that if this returns
/// `true`, then the entire subtree will be skipped.
pub fn can_skip_foreign_access(self, happening_next: LastForeignAccess) -> bool {
debug_assert!(happening_next.is_foreign());
// This ordering is correct. Intuitively, if the last access here was
// a foreign write, everything can be skipped, since after a foreign write,
// all further foreign accesses are idempotent
happening_next <= self
}

/// Updates `self` to account for a foreign access.
pub fn record_new(&mut self, just_happened: LastForeignAccess) {
if just_happened.is_local() {
// If the access is local, reset it.
*self = LastForeignAccess::LocalAccess;
} else {
// Otherwise, keep it or stengthen it.
*self = just_happened.max(*self);
}
}

/// Returns true if this access is local.
pub fn is_local(self) -> bool {
matches!(self, LastForeignAccess::LocalAccess)
}

/// Returns true if this access is foreign, i.e. not local.
pub fn is_foreign(self) -> bool {
!self.is_local()
}

/// Constructs a foreign access from an `AccessKind`
pub fn foreign(acc: AccessKind) -> LastForeignAccess {
match acc {
AccessKind::Read => Self::ForeignRead,
AccessKind::Write => Self::ForeignWrite,
}
}

/// Usually, tree traversals have an `AccessKind` and an `AccessRelatedness`.
/// This methods converts these into the corresponding `LastForeignAccess`, to be used
/// to e.g. invoke `can_skip_foreign_access`.
pub fn of_acc_and_rel(acc: AccessKind, rel: AccessRelatedness) -> LastForeignAccess {
if rel.is_foreign() { Self::foreign(acc) } else { Self::LocalAccess }
}

/// During retags, the SIFA needs to be weakened to account for children with weaker SIFAs being inserted.
/// Thus, this method is called from the bottom up on each parent, until it returns false, which means the
/// "children have stronger SIFAs" invariant is restored.
pub fn ensure_no_stronger_than(&mut self, strongest_allowed: LastForeignAccess) -> bool {
if *self > strongest_allowed {
*self = strongest_allowed;
true
} else {
false
}
}
}
9 changes: 6 additions & 3 deletions src/borrow_tracker/tree_borrows/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ use crate::concurrency::data_race::NaReadType;
use crate::*;

pub mod diagnostics;
mod foreign_access_skipping;
mod perms;
mod tree;
mod unimap;
Expand Down Expand Up @@ -296,12 +297,14 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
this.machine.current_span(),
)?;
// Record the parent-child pair in the tree.
tree_borrows.new_child(orig_tag, new_tag, new_perm.initial_state, range, span)?;
tree_borrows.update_last_accessed_after_retag(
tree_borrows.new_child(
orig_tag,
new_tag,
new_perm.initial_state,
range,
span,
new_perm.protector.is_some(),
);
)?;
drop(tree_borrows);

// Also inform the data race model (but only if any bytes are actually affected).
Expand Down
49 changes: 37 additions & 12 deletions src/borrow_tracker/tree_borrows/perms.rs
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,7 @@ enum PermissionPriv {
Disabled,
}
use self::PermissionPriv::*;
use super::foreign_access_skipping::LastForeignAccess;

impl PartialOrd for PermissionPriv {
/// PermissionPriv is ordered by the reflexive transitive closure of
Expand Down Expand Up @@ -88,25 +89,23 @@ impl PermissionPriv {
!matches!(self, ReservedIM)
}

/// Returns the strongest foreign action this node survives (without change),
/// where `prot` indicates if it is protected.
/// They are ordered as `None` < `Some(Read)` < `Some(Write)`, in order of power.
pub fn strongest_survivable_foreign_action(&self, prot: bool) -> Option<AccessKind> {
/// See `foreign_access_skipping.rs`. Compotes the SIFA of a permission.
fn strongest_idempotent_foreign_access(&self, prot: bool) -> LastForeignAccess {
match self {
// The read will make it conflicted, so it is not invariant under it.
ReservedFrz { conflicted } if prot && !conflicted => None,
ReservedFrz { conflicted } if prot && !conflicted => LastForeignAccess::LocalAccess,
// Otherwise, foreign reads do not affect it
ReservedFrz { .. } => Some(AccessKind::Read),
ReservedFrz { .. } => LastForeignAccess::ForeignRead,
// Famously, ReservedIM survives foreign writes. It is never protected.
ReservedIM => Some(AccessKind::Write),
ReservedIM => LastForeignAccess::ForeignWrite,
// Active changes on any foreign access (becomes Frozen/Disabled).
Active => None,
Active => LastForeignAccess::LocalAccess,
// Frozen survives foreign reads, but not writes.
Frozen => Some(AccessKind::Read),
Frozen => LastForeignAccess::ForeignRead,
// Disabled survives foreign reads and writes. It survives them
// even if protected, because a protected `Disabled` is not initialized
// and does therefore not trigger UB.
Disabled => Some(AccessKind::Write),
Disabled => LastForeignAccess::ForeignWrite,
}
}
}
Expand Down Expand Up @@ -330,8 +329,9 @@ impl Permission {

/// Returns the strongest foreign action this node survives (without change),
/// where `prot` indicates if it is protected.
pub fn strongest_survivable_foreign_action(&self, prot: bool) -> Option<AccessKind> {
self.inner.strongest_survivable_foreign_action(prot)
/// See `foreign_access_skipping`
pub fn strongest_idempotent_foreign_access(&self, prot: bool) -> LastForeignAccess {
self.inner.strongest_idempotent_foreign_access(prot)
}
}

Expand Down Expand Up @@ -662,6 +662,31 @@ mod propagation_optimization_checks {
}
}

#[test]
#[rustfmt::skip]
fn permission_sifa_is_correct() {
// Tests that `strongest_idempotent_foreign_access` is correct. See `foreign_access_skipping.rs`.
for perm in PermissionPriv::exhaustive() {
// Assert that adding a protector makes is less idempotent.
assert!(perm.strongest_idempotent_foreign_access(true) <= perm.strongest_idempotent_foreign_access(false));
for prot in bool::exhaustive() {
if prot {
precondition!(perm.compatible_with_protector());
}
let access = perm.strongest_idempotent_foreign_access(prot);
// We now assert it is idempotent, and never causes UB.
// First, if the SIFA includes foreign reads, assert it is idempotent under foreign reads.
if LastForeignAccess::ForeignRead <= access {
assert_eq!(perm, transition::perform_access(AccessKind::Read, AccessRelatedness::DistantAccess, perm, prot).unwrap());
}
// Then, if the SIFA includes foreign writes, assert it is idempotent under foreign writes.
if LastForeignAccess::ForeignWrite <= access {
assert_eq!(perm, transition::perform_access(AccessKind::Write, AccessRelatedness::DistantAccess, perm, prot).unwrap());
}
}
}
}

#[test]
// Check that all transitions are consistent with the order on PermissionPriv,
// i.e. Reserved -> Active -> Frozen -> Disabled
Expand Down
Loading

0 comments on commit bbbec3a

Please sign in to comment.