Skip to content

Commit 0976d10

Browse files
authored
Merge pull request #4006 from JoJoDeveloping/tb-fix-3846-retag
Fix #3846 properly, so that subtrees can be skipped again
2 parents 059704b + 13f790c commit 0976d10

File tree

9 files changed

+329
-90
lines changed

9 files changed

+329
-90
lines changed

bench-cargo-miri/string-replace/Cargo.lock

+7
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
[package]
2+
name = "string-replace"
3+
version = "0.1.0"
4+
edition = "2021"
5+
6+
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
7+
8+
[dependencies]
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
[{"_id":"6724e6fc58417687afba2b85","index":0,"guid":"5c1bd108-2ee2-40bd-bce8-895c206409df","isActive":true,"balance":"$2,927.88","picture":"http://placehold.it/32x32","age":40,"eyeColor":"green","name":"Wynn Bradshaw","gender":"male","company":"ROTODYNE","email":"[email protected]","phone":"+1 (904) 559-3130","address":"287 Bergen Avenue, Sperryville, Alaska, 5392","about":"Adipisicing fugiat aute adipisicing qui esse cillum. Lorem consequat consectetur voluptate id pariatur nostrud incididunt aliquip incididunt laboris aliqua. Magna nulla adipisicing cupidatat ea velit aliquip magna duis duis sunt ipsum. Cillum labore mollit fugiat tempor dolor sit.\r\n","registered":"2017-01-26T01:28:10 -01:00","latitude":46.089504,"longitude":51.763723,"greeting":"Hello, Wynn Bradshaw! You have 6 unread messages.","favoriteFruit":"banana"},{"_id":"6724e6fce8619d86c0389ccf","index":1,"guid":"ced7fbb7-3b1a-419b-9fc7-d47582bbb3ea","isActive":true,"balance":"$1,856.38","picture":"http://placehold.it/32x32","age":21,"eyeColor":"brown","name":"Olsen Larsen","gender":"male","company":"VERBUS","email":"[email protected]","phone":"+1 (936) 480-3749","address":"370 Losee Terrace, Churchill, Maine, 4040","about":"Consequat Lorem in laboris fugiat veniam tempor eiusmod eu incididunt enim do et qui. Sit commodo eu excepteur cillum ex tempor commodo ex ex laboris esse. Aute aute nulla dolore dolor do. Irure esse proident nostrud non. Incididunt velit reprehenderit incididunt laboris do. Consequat nulla est id ex veniam tempor. Sit Lorem magna cillum aliquip irure quis sit minim anim.\r\n","registered":"2016-07-12T02:08:39 -02:00","latitude":-12.843628,"longitude":-124.143829,"greeting":"Hello, Olsen Larsen! You have 1 unread messages.","favoriteFruit":"apple"},{"_id":"6724e6fc01b471965ea560cf","index":2,"guid":"21fde9a3-13ba-46be-baed-fb503f668b9e","isActive":false,"balance":"$2,025.88","picture":"http://placehold.it/32x32","age":29,"eyeColor":"green","name":"Ramirez Kinney","gender":"male","company":"QUAREX","email":"[email protected]","phone":"+1 (852) 447-2930","address":"986 Cornelia Street, Oberlin, Texas, 362","about":"Minim ea proident quis eiusmod aliquip duis excepteur velit minim aute cupidatat. Esse qui ex aliquip laborum id reprehenderit. Anim dolore commodo deserunt laborum nulla duis. Sint quis anim mollit fugiat sit incididunt reprehenderit occaecat aliqua dolor. Ullamco ipsum eiusmod incididunt proident qui exercitation adipisicing voluptate elit aliquip. Tempor duis aute incididunt adipisicing.\r\n","registered":"2016-02-23T05:34:14 -01:00","latitude":-56.21645,"longitude":44.048129,"greeting":"Hello, Ramirez Kinney! You have 9 unread messages.","favoriteFruit":"banana"},{"_id":"6724e6fc3ea8e4182b9e170f","index":3,"guid":"46b20637-eecc-40db-87d7-03da9bcd1cea","isActive":true,"balance":"$3,399.31","picture":"http://placehold.it/32x32","age":39,"eyeColor":"brown","name":"Hansen Kaufman","gender":"male","company":"EVENTAGE","email":"[email protected]","phone":"+1 (827) 483-2303","address":"916 Brighton Court, Sunbury, New Mexico, 3804","about":"Nisi in voluptate aute ullamco ipsum proident fugiat veniam anim reprehenderit. In ad irure dolor labore culpa incididunt veniam mollit Lorem deserunt cupidatat incididunt. Aliquip aliquip proident ut culpa.\r\n","registered":"2023-10-18T07:03:48 -02:00","latitude":-40.239135,"longitude":49.802049,"greeting":"Hello, Hansen Kaufman! You have 10 unread messages.","favoriteFruit":"apple"},{"_id":"6724e6fc721f83a10cf2aa37","index":4,"guid":"3d23743b-1e82-474e-8f7a-855fa46170d1","isActive":false,"balance":"$1,967.87","picture":"http://placehold.it/32x32","age":35,"eyeColor":"green","name":"Imelda Stephens","gender":"female","company":"OHMNET","email":"[email protected]","phone":"+1 (893) 523-2400","address":"391 Wilson Street, Glidden, Kansas, 7226","about":"Officia sunt magna adipisicing id exercitation deserunt deserunt aliquip excepteur Lorem enim fugiat. Nulla culpa ut cupidatat excepteur do deserunt labore id eu laboris ullamco adipisicing ad. Et non nisi adipisicing minim aliquip ea ut qui adipisicing do laboris ex dolore duis.\r\n","registered":"2020-10-20T07:03:38 -02:00","latitude":0.348698,"longitude":-157.961956,"greeting":"Hello, Imelda Stephens! You have 2 unread messages.","favoriteFruit":"strawberry"},{"_id":"6724e6fc7ad7274b9f4c406c","index":5,"guid":"626292b1-ae84-4887-9e29-78e548cd24e6","isActive":true,"balance":"$1,577.44","picture":"http://placehold.it/32x32","age":40,"eyeColor":"brown","name":"Lynne Jarvis","gender":"female","company":"CORECOM","email":"[email protected]","phone":"+1 (899) 556-3876","address":"465 National Drive, Davenport, Palau, 9786","about":"Aliquip elit dolore sint quis do laboris exercitation elit aliqua eiusmod. Excepteur ad aliqua eiusmod incididunt tempor laboris officia consectetur sit. Cupidatat voluptate deserunt ut consectetur qui laborum duis elit incididunt occaecat laborum. Mollit aute velit officia amet aute minim fugiat sit laborum Lorem deserunt in. Exercitation eu sunt nulla adipisicing quis ea aute est. Lorem ea cillum ad labore quis minim et est laboris deserunt proident. Amet ut tempor laborum occaecat exercitation ullamco laborum adipisicing fugiat ea voluptate quis fugiat.\r\n","registered":"2018-11-03T03:53:15 -01:00","latitude":89.827087,"longitude":-136.882799,"greeting":"Hello, Lynne Jarvis! You have 3 unread messages.","favoriteFruit":"strawberry"},{"_id":"6724e6fcef1a1db2cf170762","index":6,"guid":"b8777c06-b90f-49a4-8737-96712fc504a3","isActive":false,"balance":"$2,285.03","picture":"http://placehold.it/32x32","age":37,"eyeColor":"green","name":"Price Bolton","gender":"male","company":"IMANT","email":"[email protected]","phone":"+1 (825) 424-2873","address":"237 Aberdeen Street, Sattley, Montana, 2918","about":"Non cillum irure fugiat consequat ad ex. Magna magna tempor excepteur irure quis. Duis in laboris ipsum adipisicing culpa magna reprehenderit nisi incididunt est veniam quis. Labore culpa ut culpa veniam est est consectetur ipsum ex esse.\r\n","registered":"2014-04-26T01:20:19 -02:00","latitude":70.349258,"longitude":126.810102,"greeting":"Hello, Price Bolton! You have 10 unread messages.","favoriteFruit":"banana"},{"_id":"6724e6fc8bcb952208c159f9","index":7,"guid":"a4e6c6c8-3fe3-42de-ae28-79c16956d309","isActive":false,"balance":"$1,298.07","picture":"http://placehold.it/32x32","age":28,"eyeColor":"blue","name":"Gretchen Wynn","gender":"female","company":"TERASCAPE","email":"[email protected]","phone":"+1 (882) 447-2895","address":"973 Suydam Place, Shindler, Nebraska, 8094","about":"Anim mollit labore magna proident ipsum culpa enim deserunt dolore sunt veniam fugiat. Ad fugiat cupidatat nisi commodo dolore duis commodo nostrud est. Enim proident ullamco non adipisicing magna consequat mollit ad reprehenderit laboris. Ex quis duis anim id non commodo amet sunt est magna officia.\r\n","registered":"2021-08-13T08:51:32 -02:00","latitude":14.551848,"longitude":-27.142242,"greeting":"Hello, Gretchen Wynn! You have 7 unread messages.","favoriteFruit":"apple"},{"_id":"6724e6fcc8243c2dfa47f5d4","index":8,"guid":"27df20d5-c1d8-419b-ad38-bdd1e6094775","isActive":true,"balance":"$3,005.40","picture":"http://placehold.it/32x32","age":33,"eyeColor":"blue","name":"Chen Travis","gender":"male","company":"MEMORA","email":"[email protected]","phone":"+1 (980) 500-2406","address":"182 Dahlgreen Place, Baker, South Carolina, 9817","about":"Ad nisi consequat aliquip eiusmod aute pariatur est sint magna. Ad magna anim esse qui Lorem nulla veniam dolore eiusmod. Cillum consequat sit aliqua est proident exercitation eiusmod irure. Minim eu laboris ad incididunt enim sunt. Sunt in excepteur aute non tempor irure mollit laboris. Eu et duis ullamco dolor sint occaecat officia culpa ipsum anim anim eu veniam aliquip. Exercitation ipsum dolor sint cillum duis incididunt minim quis irure enim reprehenderit do do incididunt.\r\n","registered":"2019-09-01T02:57:37 -02:00","latitude":25.442301,"longitude":48.381036,"greeting":"Hello, Chen Travis! You have 1 unread messages.","favoriteFruit":"banana"}]
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
const TCB_INFO_JSON: &str = include_str!("../data.json");
2+
3+
fn main() {
4+
let tcb_json = TCB_INFO_JSON;
5+
let bad_tcb_json = tcb_json.replace("female", "male");
6+
std::hint::black_box(bad_tcb_json);
7+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
1+
use super::AccessKind;
2+
use super::tree::AccessRelatedness;
3+
4+
/// To speed up tree traversals, we want to skip traversing subtrees when we know the traversal will have no effect.
5+
/// This is often the case for foreign accesses, since usually foreign accesses happen several times in a row, but also
6+
/// foreign accesses are idempotent. In particular, see tests `foreign_read_is_noop_after_foreign_write` and `all_transitions_idempotent`.
7+
/// Thus, for each node we keep track of the "strongest idempotent foreign access" (SIFA), i.e. which foreign access can be skipped.
8+
/// Note that for correctness, it is not required that this is the strongest access, just any access it is idempotent under. In particular, setting
9+
/// it to `None` is always correct, but the point of this optimization is to have it be as strong as possible so that more accesses can be skipped.
10+
/// This enum represents the kinds of values we store:
11+
/// - `None` means that the node (and its subtrees) are not (guaranteed to be) idempotent under any foreign access.
12+
/// - `Read` means that the node (and its subtrees) are idempotent under foreign reads, but not (yet / necessarily) under foreign writes.
13+
/// - `Write` means that the node (and its subtrees) are idempotent under foreign writes. This also implies that it is idempotent under foreign
14+
/// reads, since reads are stronger than writes (see test `foreign_read_is_noop_after_foreign_write`). In other words, this node can be skipped
15+
/// for all foreign accesses.
16+
///
17+
/// Since a traversal does not just visit a node, but instead the entire subtree, the SIFA field for a given node indicates that the access to
18+
/// *the entire subtree* rooted at that node can be skipped. In order for this to work, we maintain the global invariant that at
19+
/// each location, the SIFA at each child must be stronger than that at the parent. For normal reads and writes, this is easily accomplished by
20+
/// tracking each foreign access as it occurs, so that then the next access can be skipped. This also obviously maintains the invariant, because
21+
/// if a node undergoes a foreign access, then all its children also see this as a foreign access. However, the invariant is broken during retags,
22+
/// because retags act across the entire allocation, but only emit a read event across a specific range. This means that for all nodes outside that
23+
/// range, the invariant is potentially broken, since a new child with a weaker SIFA is inserted. Thus, during retags, special care is taken to
24+
/// "manually" reset the parent's SIFA to be at least as strong as the new child's. This is accomplished with the `ensure_no_stronger_than` method.
25+
///
26+
/// Note that we derive Ord and PartialOrd, so the order in which variants are listed below matters:
27+
/// None < Read < Write. Do not change that order. See the `test_order` test.
28+
#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug, Default)]
29+
pub enum IdempotentForeignAccess {
30+
#[default]
31+
None,
32+
Read,
33+
Write,
34+
}
35+
36+
impl IdempotentForeignAccess {
37+
/// Returns true if a node where the strongest idempotent foreign access is `self`
38+
/// can skip the access `happening_next`. Note that if this returns
39+
/// `true`, then the entire subtree will be skipped.
40+
pub fn can_skip_foreign_access(self, happening_next: IdempotentForeignAccess) -> bool {
41+
debug_assert!(happening_next.is_foreign());
42+
// This ordering is correct. Intuitively, if the last access here was
43+
// a foreign write, everything can be skipped, since after a foreign write,
44+
// all further foreign accesses are idempotent
45+
happening_next <= self
46+
}
47+
48+
/// Updates `self` to account for a foreign access.
49+
pub fn record_new(&mut self, just_happened: IdempotentForeignAccess) {
50+
if just_happened.is_local() {
51+
// If the access is local, reset it.
52+
*self = IdempotentForeignAccess::None;
53+
} else {
54+
// Otherwise, keep it or stengthen it.
55+
*self = just_happened.max(*self);
56+
}
57+
}
58+
59+
/// Returns true if this access is local.
60+
pub fn is_local(self) -> bool {
61+
matches!(self, IdempotentForeignAccess::None)
62+
}
63+
64+
/// Returns true if this access is foreign, i.e. not local.
65+
pub fn is_foreign(self) -> bool {
66+
!self.is_local()
67+
}
68+
69+
/// Constructs a foreign access from an `AccessKind`
70+
pub fn from_foreign(acc: AccessKind) -> IdempotentForeignAccess {
71+
match acc {
72+
AccessKind::Read => Self::Read,
73+
AccessKind::Write => Self::Write,
74+
}
75+
}
76+
77+
/// Usually, tree traversals have an `AccessKind` and an `AccessRelatedness`.
78+
/// This methods converts these into the corresponding `IdempotentForeignAccess`, to be used
79+
/// to e.g. invoke `can_skip_foreign_access`.
80+
pub fn from_acc_and_rel(acc: AccessKind, rel: AccessRelatedness) -> IdempotentForeignAccess {
81+
if rel.is_foreign() { Self::from_foreign(acc) } else { Self::None }
82+
}
83+
84+
/// During retags, the SIFA needs to be weakened to account for children with weaker SIFAs being inserted.
85+
/// Thus, this method is called from the bottom up on each parent, until it returns false, which means the
86+
/// "children have stronger SIFAs" invariant is restored.
87+
pub fn ensure_no_stronger_than(&mut self, strongest_allowed: IdempotentForeignAccess) -> bool {
88+
if *self > strongest_allowed {
89+
*self = strongest_allowed;
90+
true
91+
} else {
92+
false
93+
}
94+
}
95+
}
96+
97+
#[cfg(test)]
98+
mod tests {
99+
use super::IdempotentForeignAccess;
100+
101+
#[test]
102+
fn test_order() {
103+
// The internal logic relies on this order.
104+
// Do not change.
105+
assert!(IdempotentForeignAccess::None < IdempotentForeignAccess::Read);
106+
assert!(IdempotentForeignAccess::Read < IdempotentForeignAccess::Write);
107+
}
108+
}

src/borrow_tracker/tree_borrows/mod.rs

+9-1
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ use crate::concurrency::data_race::NaReadType;
99
use crate::*;
1010

1111
pub mod diagnostics;
12+
mod foreign_access_skipping;
1213
mod perms;
1314
mod tree;
1415
mod unimap;
@@ -296,7 +297,14 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
296297
this.machine.current_span(),
297298
)?;
298299
// Record the parent-child pair in the tree.
299-
tree_borrows.new_child(orig_tag, new_tag, new_perm.initial_state, range, span)?;
300+
tree_borrows.new_child(
301+
orig_tag,
302+
new_tag,
303+
new_perm.initial_state,
304+
range,
305+
span,
306+
new_perm.protector.is_some(),
307+
)?;
300308
drop(tree_borrows);
301309

302310
// Also inform the data race model (but only if any bytes are actually affected).

src/borrow_tracker/tree_borrows/perms.rs

+60-1
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,7 @@ enum PermissionPriv {
4848
Disabled,
4949
}
5050
use self::PermissionPriv::*;
51+
use super::foreign_access_skipping::IdempotentForeignAccess;
5152

5253
impl PartialOrd for PermissionPriv {
5354
/// PermissionPriv is ordered by the reflexive transitive closure of
@@ -87,6 +88,28 @@ impl PermissionPriv {
8788
fn compatible_with_protector(&self) -> bool {
8889
!matches!(self, ReservedIM)
8990
}
91+
92+
/// See `foreign_access_skipping.rs`. Computes the SIFA of a permission.
93+
fn strongest_idempotent_foreign_access(&self, prot: bool) -> IdempotentForeignAccess {
94+
match self {
95+
// A protected non-conflicted Reserved will become conflicted under a foreign read,
96+
// and is hence not idempotent under it.
97+
ReservedFrz { conflicted } if prot && !conflicted => IdempotentForeignAccess::None,
98+
// Otherwise, foreign reads do not affect Reserved
99+
ReservedFrz { .. } => IdempotentForeignAccess::Read,
100+
// Famously, ReservedIM survives foreign writes. It is never protected.
101+
ReservedIM if prot => unreachable!("Protected ReservedIM should not exist!"),
102+
ReservedIM => IdempotentForeignAccess::Write,
103+
// Active changes on any foreign access (becomes Frozen/Disabled).
104+
Active => IdempotentForeignAccess::None,
105+
// Frozen survives foreign reads, but not writes.
106+
Frozen => IdempotentForeignAccess::Read,
107+
// Disabled survives foreign reads and writes. It survives them
108+
// even if protected, because a protected `Disabled` is not initialized
109+
// and does therefore not trigger UB.
110+
Disabled => IdempotentForeignAccess::Write,
111+
}
112+
}
90113
}
91114

92115
/// This module controls how each permission individually reacts to an access.
@@ -305,6 +328,13 @@ impl Permission {
305328
(Disabled, _) => false,
306329
}
307330
}
331+
332+
/// Returns the strongest foreign action this node survives (without change),
333+
/// where `prot` indicates if it is protected.
334+
/// See `foreign_access_skipping`
335+
pub fn strongest_idempotent_foreign_access(&self, prot: bool) -> IdempotentForeignAccess {
336+
self.inner.strongest_idempotent_foreign_access(prot)
337+
}
308338
}
309339

310340
impl PermTransition {
@@ -575,7 +605,7 @@ mod propagation_optimization_checks {
575605
impl Exhaustive for AccessRelatedness {
576606
fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
577607
use AccessRelatedness::*;
578-
Box::new(vec![This, StrictChildAccess, AncestorAccess, DistantAccess].into_iter())
608+
Box::new(vec![This, StrictChildAccess, AncestorAccess, CousinAccess].into_iter())
579609
}
580610
}
581611

@@ -634,6 +664,35 @@ mod propagation_optimization_checks {
634664
}
635665
}
636666

667+
#[test]
668+
#[rustfmt::skip]
669+
fn permission_sifa_is_correct() {
670+
// Tests that `strongest_idempotent_foreign_access` is correct. See `foreign_access_skipping.rs`.
671+
for perm in PermissionPriv::exhaustive() {
672+
// Assert that adding a protector makes it less idempotent.
673+
if perm.compatible_with_protector() {
674+
assert!(perm.strongest_idempotent_foreign_access(true) <= perm.strongest_idempotent_foreign_access(false));
675+
}
676+
for prot in bool::exhaustive() {
677+
if prot {
678+
precondition!(perm.compatible_with_protector());
679+
}
680+
let access = perm.strongest_idempotent_foreign_access(prot);
681+
// We now assert it is idempotent, and never causes UB.
682+
// First, if the SIFA includes foreign reads, assert it is idempotent under foreign reads.
683+
if access >= IdempotentForeignAccess::Read {
684+
// We use `CousinAccess` here. We could also use `AncestorAccess`, since `transition::perform_access` treats these the same.
685+
// The only place they are treated differently is in protector end accesses, but these are not handled here.
686+
assert_eq!(perm, transition::perform_access(AccessKind::Read, AccessRelatedness::CousinAccess, perm, prot).unwrap());
687+
}
688+
// Then, if the SIFA includes foreign writes, assert it is idempotent under foreign writes.
689+
if access >= IdempotentForeignAccess::Write {
690+
assert_eq!(perm, transition::perform_access(AccessKind::Write, AccessRelatedness::CousinAccess, perm, prot).unwrap());
691+
}
692+
}
693+
}
694+
}
695+
637696
#[test]
638697
// Check that all transitions are consistent with the order on PermissionPriv,
639698
// i.e. Reserved -> Active -> Frozen -> Disabled

0 commit comments

Comments
 (0)