Skip to content

Commit ee674e7

Browse files
committed
tree borrows: consider some retags as writes for the purpose of data races
1 parent f0cbc7d commit ee674e7

15 files changed

+186
-138
lines changed

Diff for: src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -218,7 +218,7 @@ impl<'tcx> Tree {
218218
}
219219
}
220220

221-
#[derive(Debug, Clone, Copy, PartialEq)]
221+
#[derive(Debug, Clone, Copy)]
222222
pub(super) enum TransitionError {
223223
/// This access is not allowed because some parent tag has insufficient permissions.
224224
/// For example, if a tag is `Frozen` and encounters a child write this will

Diff for: src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs

+32-16
Original file line numberDiff line numberDiff line change
@@ -117,7 +117,7 @@ impl<'tcx> NewPermission {
117117
let ty_is_freeze = pointee.is_freeze(*cx.tcx, cx.param_env());
118118
let ty_is_unpin = pointee.is_unpin(*cx.tcx, cx.param_env());
119119
let initial_state = match mutability {
120-
Mutability::Mut if ty_is_unpin => Permission::new_unique_2phase(ty_is_freeze),
120+
Mutability::Mut if ty_is_unpin => Permission::new_reserved(ty_is_freeze),
121121
Mutability::Not if ty_is_freeze => Permission::new_frozen(),
122122
// Raw pointers never enter this function so they are not handled.
123123
// However raw pointers are not the only pointers that take the parent
@@ -146,7 +146,7 @@ impl<'tcx> NewPermission {
146146
let ty_is_freeze = ty.is_freeze(*cx.tcx, cx.param_env());
147147
Self {
148148
zero_size,
149-
initial_state: Permission::new_unique_2phase(ty_is_freeze),
149+
initial_state: Permission::new_reserved(ty_is_freeze),
150150
protector: (kind == RetagKind::FnEntry).then_some(ProtectorKind::WeakProtector),
151151
}
152152
})
@@ -250,6 +250,7 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
250250

251251
let alloc_kind = this.get_alloc_info(alloc_id).2;
252252
if !matches!(alloc_kind, AllocKind::LiveData) {
253+
assert_eq!(ptr_size, Size::ZERO); // we did the deref check above, size has to be 0 here
253254
// There's not actually any bytes here where accesses could even be tracked.
254255
// Just produce the new provenance, nothing else to do.
255256
return Ok(Some(Provenance::Concrete { alloc_id, tag: new_tag }));
@@ -261,24 +262,39 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
261262
let mut tree_borrows = alloc_extra.borrow_tracker_tb().borrow_mut();
262263

263264
// All reborrows incur a (possibly zero-sized) read access to the parent
264-
{
265-
let global = &this.machine.borrow_tracker.as_ref().unwrap();
266-
let span = this.machine.current_span();
267-
tree_borrows.perform_access(
268-
AccessKind::Read,
269-
orig_tag,
270-
range,
271-
global,
272-
span,
273-
diagnostics::AccessCause::Reborrow,
274-
)?;
265+
tree_borrows.perform_access(
266+
AccessKind::Read,
267+
orig_tag,
268+
range,
269+
this.machine.borrow_tracker.as_ref().unwrap(),
270+
this.machine.current_span(),
271+
diagnostics::AccessCause::Reborrow,
272+
)?;
273+
// Record the parent-child pair in the tree.
274+
tree_borrows.new_child(orig_tag, new_tag, new_perm.initial_state, range, span)?;
275+
drop(tree_borrows);
276+
277+
// Also inform the data race model (but only if any bytes are actually affected).
278+
if range.size.bytes() > 0 {
275279
if let Some(data_race) = alloc_extra.data_race.as_ref() {
276-
data_race.read(alloc_id, range, &this.machine)?;
280+
// We sometimes need to make it a write, since not all retags commute with reads!
281+
// FIXME: Is that truly the semantics we want? Some optimizations are likely to be
282+
// very unhappy without this. We'd tsill ge some UB just by picking a suitable
283+
// interleaving, but wether UB happens can depend on whether a write occurs in the
284+
// future...
285+
let is_write = new_perm.initial_state.is_active()
286+
|| (new_perm.initial_state.is_resrved() && new_perm.protector.is_some());
287+
if is_write {
288+
// Need to get mutable access to alloc_extra.
289+
// (Cannot always do this as we can do read-only reborrowing on read-only allocations.)
290+
let (alloc_extra, machine) = this.get_alloc_extra_mut(alloc_id)?;
291+
alloc_extra.data_race.as_mut().unwrap().write(alloc_id, range, machine)?;
292+
} else {
293+
data_race.read(alloc_id, range, &this.machine)?;
294+
}
277295
}
278296
}
279297

280-
// Record the parent-child pair in the tree.
281-
tree_borrows.new_child(orig_tag, new_tag, new_perm.initial_state, range, span)?;
282298
Ok(Some(Provenance::Concrete { alloc_id, tag: new_tag }))
283299
}
284300

Diff for: src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs

+14-7
Original file line numberDiff line numberDiff line change
@@ -134,25 +134,32 @@ pub struct PermTransition {
134134

135135
impl Permission {
136136
/// Default initial permission of the root of a new tree.
137-
pub fn new_root() -> Self {
137+
pub fn new_active() -> Self {
138138
Self { inner: Active }
139139
}
140140

141141
/// Default initial permission of a reborrowed mutable reference.
142-
pub fn new_unique_2phase(ty_is_freeze: bool) -> Self {
142+
pub fn new_reserved(ty_is_freeze: bool) -> Self {
143143
Self { inner: Reserved { ty_is_freeze } }
144144
}
145145

146-
/// Default initial permission for return place.
147-
pub fn new_active() -> Self {
148-
Self { inner: Active }
149-
}
150-
151146
/// Default initial permission of a reborrowed shared reference
152147
pub fn new_frozen() -> Self {
153148
Self { inner: Frozen }
154149
}
155150

151+
pub fn is_active(self) -> bool {
152+
matches!(self.inner, Active)
153+
}
154+
155+
pub fn is_resrved(self) -> bool {
156+
matches!(self.inner, Reserved { .. })
157+
}
158+
159+
pub fn is_frozen(self) -> bool {
160+
matches!(self.inner, Frozen)
161+
}
162+
156163
/// Apply the transition to the inner PermissionPriv.
157164
pub fn perform_access(
158165
kind: AccessKind,

Diff for: src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -376,7 +376,7 @@ where {
376376
impl Tree {
377377
/// Create a new tree, with only a root pointer.
378378
pub fn new(root_tag: BorTag, size: Size, span: Span) -> Self {
379-
let root_perm = Permission::new_root();
379+
let root_perm = Permission::new_active();
380380
let mut tag_mapping = UniKeyMap::default();
381381
let root_idx = tag_mapping.insert(root_tag);
382382
let nodes = {
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
//@revisions: stack tree
2+
//@compile-flags: -Zmiri-preemption-rate=0
3+
//@[tree]compile-flags: -Zmiri-tree-borrows
4+
use std::thread;
5+
6+
#[derive(Copy, Clone)]
7+
struct SendPtr(*mut i32);
8+
unsafe impl Send for SendPtr {}
9+
10+
fn main() {
11+
let mut mem = 0;
12+
let ptr = SendPtr(&mut mem as *mut _);
13+
14+
let t = thread::spawn(move || {
15+
let ptr = ptr;
16+
// We do a protected 2phase retag (but no write!) in this thread.
17+
fn retag(_x: &mut i32) {} //~[tree]ERROR: Data race detected between (1) Read on thread `main` and (2) Write on thread `<unnamed>`
18+
retag(unsafe { &mut *ptr.0 }); //~[stack]ERROR: Data race detected between (1) Read on thread `main` and (2) Write on thread `<unnamed>`
19+
});
20+
21+
// We do a read in the main thread.
22+
unsafe { ptr.0.read() };
23+
24+
// These two operations do not commute -- if the read happens after the retag, the retagged pointer
25+
// gets frozen! So we want this to be considered UB so that we can still freely move the read around
26+
// in this thread without worrying about reordering with retags in other threads.
27+
28+
t.join().unwrap();
29+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
error: Undefined Behavior: Data race detected between (1) Read on thread `main` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
2+
--> $DIR/retag_data_race_protected_read.rs:LL:CC
3+
|
4+
LL | retag(unsafe { &mut *ptr.0 });
5+
| ^^^^^^^^^^^ Data race detected between (1) Read on thread `main` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
6+
|
7+
help: and (1) occurred earlier here
8+
--> $DIR/retag_data_race_protected_read.rs:LL:CC
9+
|
10+
LL | unsafe { ptr.0.read() };
11+
| ^^^^^^^^^^^^
12+
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
13+
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
14+
= note: BACKTRACE (of the first span):
15+
= note: inside closure at $DIR/retag_data_race_protected_read.rs:LL:CC
16+
17+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
18+
19+
error: aborting due to previous error
20+
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
error: Undefined Behavior: Data race detected between (1) Read on thread `main` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
2+
--> $DIR/retag_data_race_protected_read.rs:LL:CC
3+
|
4+
LL | fn retag(_x: &mut i32) {}
5+
| ^^ Data race detected between (1) Read on thread `main` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
6+
|
7+
help: and (1) occurred earlier here
8+
--> $DIR/retag_data_race_protected_read.rs:LL:CC
9+
|
10+
LL | unsafe { ptr.0.read() };
11+
| ^^^^^^^^^^^^
12+
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
13+
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
14+
= note: BACKTRACE (of the first span):
15+
= note: inside `main::{closure#0}::retag` at $DIR/retag_data_race_protected_read.rs:LL:CC
16+
note: inside closure
17+
--> $DIR/retag_data_race_protected_read.rs:LL:CC
18+
|
19+
LL | ... retag(unsafe { &mut *ptr.0 });
20+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
21+
22+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
23+
24+
error: aborting due to previous error
25+

Diff for: src/tools/miri/tests/fail/stacked_borrows/retag_data_race_write.rs renamed to src/tools/miri/tests/fail/both_borrows/retag_data_race_write.rs

+3-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
//! Make sure that a retag acts like a write for the data race model.
2+
//@revisions: stack tree
23
//@compile-flags: -Zmiri-preemption-rate=0
4+
//@[tree]compile-flags: -Zmiri-tree-borrows
35
#[derive(Copy, Clone)]
46
struct SendPtr(*mut u8);
57

@@ -15,7 +17,7 @@ fn thread_1(p: SendPtr) {
1517
fn thread_2(p: SendPtr) {
1618
let p = p.0;
1719
unsafe {
18-
*p = 5; //~ ERROR: Data race detected between (1) Write on thread `<unnamed>` and (2) Write on thread `<unnamed>`
20+
*p = 5; //~ ERROR: /Data race detected between \(1\) (Read|Write) on thread `<unnamed>` and \(2\) Write on thread `<unnamed>`/
1921
}
2022
}
2123

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
error: Undefined Behavior: Data race detected between (1) Read on thread `<unnamed>` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
2+
--> $DIR/retag_data_race_write.rs:LL:CC
3+
|
4+
LL | *p = 5;
5+
| ^^^^^^ Data race detected between (1) Read on thread `<unnamed>` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
6+
|
7+
help: and (1) occurred earlier here
8+
--> $DIR/retag_data_race_write.rs:LL:CC
9+
|
10+
LL | let _r = &mut *p;
11+
| ^^^^^^^
12+
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
13+
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
14+
= note: BACKTRACE (of the first span):
15+
= note: inside `thread_2` at $DIR/retag_data_race_write.rs:LL:CC
16+
note: inside closure
17+
--> $DIR/retag_data_race_write.rs:LL:CC
18+
|
19+
LL | let t2 = std::thread::spawn(move || thread_2(p));
20+
| ^^^^^^^^^^^
21+
22+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
23+
24+
error: aborting due to previous error
25+

Diff for: src/tools/miri/tests/fail/tree_borrows/retag-data-race.stderr renamed to src/tools/miri/tests/fail/stacked_borrows/retag_data_race_read.stack.stderr

+10-10
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,23 @@
11
error: Undefined Behavior: Data race detected between (1) Read on thread `<unnamed>` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
2-
--> $DIR/retag-data-race.rs:LL:CC
2+
--> $DIR/retag_data_race_read.rs:LL:CC
33
|
4-
LL | *p = 5;
5-
| ^^^^^^ Data race detected between (1) Read on thread `<unnamed>` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
4+
LL | *p = 5;
5+
| ^^^^^^ Data race detected between (1) Read on thread `<unnamed>` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
66
|
77
help: and (1) occurred earlier here
8-
--> $DIR/retag-data-race.rs:LL:CC
8+
--> $DIR/retag_data_race_read.rs:LL:CC
99
|
10-
LL | let _r = &*p;
11-
| ^^^
10+
LL | let _r = &*p;
11+
| ^^^
1212
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
1313
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
1414
= note: BACKTRACE (of the first span):
15-
= note: inside `thread_2` at $DIR/retag-data-race.rs:LL:CC
15+
= note: inside `thread_2` at $DIR/retag_data_race_read.rs:LL:CC
1616
note: inside closure
17-
--> $DIR/retag-data-race.rs:LL:CC
17+
--> $DIR/retag_data_race_read.rs:LL:CC
1818
|
19-
LL | let t2 = std::thread::spawn(move || unsafe { thread_2(p) });
20-
| ^^^^^^^^^^^
19+
LL | let t2 = std::thread::spawn(move || thread_2(p));
20+
| ^^^^^^^^^^^
2121

2222
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
2323

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
error: Undefined Behavior: reborrow through <TAG> (root of the allocation) is forbidden
2+
--> RUSTLIB/std/src/rt.rs:LL:CC
3+
|
4+
LL | panic::catch_unwind(move || unsafe { init(argc, argv, sigpipe) }).map_err(rt_abort)?;
5+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ reborrow through <TAG> (root of the allocation) is forbidden
6+
|
7+
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
8+
= help: the accessed tag <TAG> (root of the allocation) is foreign to the protected tag <TAG> (i.e., it is not a child)
9+
= help: this reborrow (acting as a foreign read access) would cause the protected tag <TAG> (currently Active) to become Disabled
10+
= help: protected tags must never be Disabled
11+
help: the accessed tag <TAG> was created here
12+
--> RUSTLIB/std/src/rt.rs:LL:CC
13+
|
14+
LL | panic::catch_unwind(move || unsafe { init(argc, argv, sigpipe) }).map_err(rt_abort)?;
15+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
16+
help: the protected tag <TAG> was created here, in the initial state Active
17+
--> RUSTLIB/std/src/panic.rs:LL:CC
18+
|
19+
LL | pub fn catch_unwind<F: FnOnce() -> R + UnwindSafe, R>(f: F) -> Result<R> {
20+
| ^
21+
= note: BACKTRACE (of the first span):
22+
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
23+
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
24+
25+
error: aborting due to previous error
26+

Diff for: src/tools/miri/tests/fail/tree_borrows/fragile-data-race.rs

-42
This file was deleted.

Diff for: src/tools/miri/tests/fail/tree_borrows/fragile-data-race.stderr

-32
This file was deleted.

0 commit comments

Comments
 (0)