Skip to content

Commit a15eb7e

Browse files
borsbors
committed
Auto merge of #3137 - RalfJung:data-race, r=oli-obk
Detect mixed-size and mixed-atomicity non-synchronized accesses Fixes rust-lang/miri#2303
2 parents cc13d04 + 900b5ef commit a15eb7e

19 files changed

+416
-225
lines changed

‎src/tools/miri/ci.sh

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -108,7 +108,7 @@ case $HOST_TARGET in
108108
MIRI_TEST_TARGET=aarch64-unknown-linux-gnu run_tests
109109
MIRI_TEST_TARGET=aarch64-apple-darwin run_tests
110110
MIRI_TEST_TARGET=i686-pc-windows-gnu run_tests
111-
MIRI_TEST_TARGET=x86_64-unknown-freebsd run_tests_minimal hello integer vec panic/panic concurrency/simple atomic data_race env/var
111+
MIRI_TEST_TARGET=x86_64-unknown-freebsd run_tests_minimal hello integer vec panic/panic concurrency/simple atomic env/var
112112
MIRI_TEST_TARGET=aarch64-linux-android run_tests_minimal hello integer vec panic/panic
113113
MIRI_TEST_TARGET=wasm32-wasi run_tests_minimal no_std integer strings wasm
114114
MIRI_TEST_TARGET=wasm32-unknown-unknown run_tests_minimal no_std integer strings wasm

‎src/tools/miri/src/concurrency/data_race.rs

Lines changed: 163 additions & 115 deletions
Large diffs are not rendered by default.

‎src/tools/miri/src/concurrency/weak_memory.rs

Lines changed: 4 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -169,14 +169,6 @@ impl StoreBufferAlloc {
169169
Self { store_buffers: RefCell::new(RangeObjectMap::new()) }
170170
}
171171

172-
/// Checks if the range imperfectly overlaps with existing buffers
173-
/// Used to determine if mixed-size atomic accesses
174-
fn is_overlapping(&self, range: AllocRange) -> bool {
175-
let buffers = self.store_buffers.borrow();
176-
let access_type = buffers.access_type(range);
177-
matches!(access_type, AccessType::ImperfectlyOverlapping(_))
178-
}
179-
180172
/// When a non-atomic access happens on a location that has been atomically accessed
181173
/// before without data race, we can determine that the non-atomic access fully happens
182174
/// after all the prior atomic accesses so the location no longer needs to exhibit
@@ -190,6 +182,8 @@ impl StoreBufferAlloc {
190182
buffers.remove_from_pos(pos);
191183
}
192184
AccessType::ImperfectlyOverlapping(pos_range) => {
185+
// We rely on the data-race check making sure this is synchronized.
186+
// Therefore we can forget about the old data here.
193187
buffers.remove_pos_range(pos_range);
194188
}
195189
AccessType::Empty(_) => {
@@ -215,7 +209,7 @@ impl StoreBufferAlloc {
215209
pos
216210
}
217211
AccessType::ImperfectlyOverlapping(pos_range) => {
218-
// Once we reach here we would've already checked that this access is not racy
212+
// Once we reach here we would've already checked that this access is not racy.
219213
let mut buffers = self.store_buffers.borrow_mut();
220214
buffers.remove_pos_range(pos_range.clone());
221215
buffers.insert_at_pos(pos_range.start, range, StoreBuffer::new(init));
@@ -240,6 +234,7 @@ impl StoreBufferAlloc {
240234
pos
241235
}
242236
AccessType::ImperfectlyOverlapping(pos_range) => {
237+
// Once we reach here we would've already checked that this access is not racy.
243238
buffers.remove_pos_range(pos_range.clone());
244239
buffers.insert_at_pos(pos_range.start, range, StoreBuffer::new(init));
245240
pos_range.start
@@ -473,37 +468,6 @@ impl<'mir, 'tcx: 'mir> EvalContextExt<'mir, 'tcx> for crate::MiriInterpCx<'mir,
473468
pub(super) trait EvalContextExt<'mir, 'tcx: 'mir>:
474469
crate::MiriInterpCxExt<'mir, 'tcx>
475470
{
476-
// If weak memory emulation is enabled, check if this atomic op imperfectly overlaps with a previous
477-
// atomic read or write. If it does, then we require it to be ordered (non-racy) with all previous atomic
478-
// accesses on all the bytes in range
479-
fn validate_overlapping_atomic(
480-
&self,
481-
place: &MPlaceTy<'tcx, Provenance>,
482-
) -> InterpResult<'tcx> {
483-
let this = self.eval_context_ref();
484-
let (alloc_id, base_offset, ..) = this.ptr_get_alloc_id(place.ptr())?;
485-
if let crate::AllocExtra {
486-
weak_memory: Some(alloc_buffers),
487-
data_race: Some(alloc_clocks),
488-
..
489-
} = this.get_alloc_extra(alloc_id)?
490-
{
491-
let range = alloc_range(base_offset, place.layout.size);
492-
if alloc_buffers.is_overlapping(range)
493-
&& !alloc_clocks.race_free_with_atomic(
494-
range,
495-
this.machine.data_race.as_ref().unwrap(),
496-
&this.machine.threads,
497-
)
498-
{
499-
throw_unsup_format!(
500-
"racy imperfectly overlapping atomic access is not possible in the C++20 memory model, and not supported by Miri's weak memory emulation"
501-
);
502-
}
503-
}
504-
Ok(())
505-
}
506-
507471
fn buffered_atomic_rmw(
508472
&mut self,
509473
new_val: Scalar<Provenance>,

‎src/tools/miri/src/diagnostics.rs

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -43,9 +43,10 @@ pub enum TerminationInfo {
4343
span: SpanData,
4444
},
4545
DataRace {
46+
involves_non_atomic: bool,
47+
ptr: Pointer,
4648
op1: RacingOp,
4749
op2: RacingOp,
48-
ptr: Pointer,
4950
},
5051
}
5152

@@ -74,11 +75,15 @@ impl fmt::Display for TerminationInfo {
7475
write!(f, "multiple definitions of symbol `{link_name}`"),
7576
SymbolShimClashing { link_name, .. } =>
7677
write!(f, "found `{link_name}` symbol definition that clashes with a built-in shim",),
77-
DataRace { ptr, op1, op2 } =>
78+
DataRace { involves_non_atomic, ptr, op1, op2 } =>
7879
write!(
7980
f,
80-
"Data race detected between (1) {} on {} and (2) {} on {} at {ptr:?}. (2) just happened here",
81-
op1.action, op1.thread_info, op2.action, op2.thread_info
81+
"{} detected between (1) {} on {} and (2) {} on {} at {ptr:?}. (2) just happened here",
82+
if *involves_non_atomic { "Data race" } else { "Race condition" },
83+
op1.action,
84+
op1.thread_info,
85+
op2.action,
86+
op2.thread_info
8287
),
8388
}
8489
}

‎src/tools/miri/tests/fail/data_race/mixed_size_read.rs

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
//@compile-flags: -Zmiri-preemption-rate=0.0 -Zmiri-disable-weak-memory-emulation
2+
use std::sync::atomic::{AtomicU16, AtomicU8, Ordering};
3+
use std::thread;
4+
5+
fn convert(a: &AtomicU16) -> &[AtomicU8; 2] {
6+
unsafe { std::mem::transmute(a) }
7+
}
8+
9+
// We can't allow mixed-size accesses; they are not possible in C++ and even
10+
// Intel says you shouldn't do it.
11+
fn main() {
12+
let a = AtomicU16::new(0);
13+
let a16 = &a;
14+
let a8 = convert(a16);
15+
16+
thread::scope(|s| {
17+
s.spawn(|| {
18+
a16.load(Ordering::SeqCst);
19+
});
20+
s.spawn(|| {
21+
a8[0].load(Ordering::SeqCst);
22+
//~^ ERROR: Race condition detected between (1) 2-byte Atomic Load on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Load on thread `<unnamed>`
23+
});
24+
});
25+
}

‎src/tools/miri/tests/fail/data_race/mixed_size_read.stderr

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
error: Undefined Behavior: Race condition detected between (1) 2-byte Atomic Load on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
2+
--> $DIR/mixed_size_read.rs:LL:CC
3+
|
4+
LL | a8[0].load(Ordering::SeqCst);
5+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 2-byte Atomic Load on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
6+
|
7+
help: and (1) occurred earlier here
8+
--> $DIR/mixed_size_read.rs:LL:CC
9+
|
10+
LL | a16.load(Ordering::SeqCst);
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/mixed_size_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+

‎src/tools/miri/tests/fail/data_race/mixed_size_write.rs

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
//@compile-flags: -Zmiri-preemption-rate=0.0 -Zmiri-disable-weak-memory-emulation
2+
use std::sync::atomic::{AtomicU16, AtomicU8, Ordering};
3+
use std::thread;
4+
5+
fn convert(a: &AtomicU16) -> &[AtomicU8; 2] {
6+
unsafe { std::mem::transmute(a) }
7+
}
8+
9+
// We can't allow mixed-size accesses; they are not possible in C++ and even
10+
// Intel says you shouldn't do it.
11+
fn main() {
12+
let a = AtomicU16::new(0);
13+
let a16 = &a;
14+
let a8 = convert(a16);
15+
16+
thread::scope(|s| {
17+
s.spawn(|| {
18+
a16.store(1, Ordering::SeqCst);
19+
});
20+
s.spawn(|| {
21+
a8[0].store(1, Ordering::SeqCst);
22+
//~^ ERROR: Race condition detected between (1) 2-byte Atomic Store on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Store on thread `<unnamed>`
23+
});
24+
});
25+
}

‎src/tools/miri/tests/fail/data_race/mixed_size_write.stderr

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
error: Undefined Behavior: Race condition detected between (1) 2-byte Atomic Store on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Store on thread `<unnamed>` at ALLOC. (2) just happened here
2+
--> $DIR/mixed_size_write.rs:LL:CC
3+
|
4+
LL | a8[0].store(1, Ordering::SeqCst);
5+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 2-byte Atomic Store on thread `<unnamed>` and (2) 1-byte (different-size) Atomic Store on thread `<unnamed>` at ALLOC. (2) just happened here
6+
|
7+
help: and (1) occurred earlier here
8+
--> $DIR/mixed_size_write.rs:LL:CC
9+
|
10+
LL | a16.store(1, Ordering::SeqCst);
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/mixed_size_write.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+

‎src/tools/miri/tests/fail/data_race/read_read_race1.rs

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
//@compile-flags: -Zmiri-preemption-rate=0.0
2+
use std::sync::atomic::{AtomicU16, Ordering};
3+
use std::thread;
4+
5+
// Make sure races between atomic and non-atomic reads are detected.
6+
// This seems harmless but C++ does not allow them, so we can't allow them for now either.
7+
// This test coverse the case where the non-atomic access come first.
8+
fn main() {
9+
let a = AtomicU16::new(0);
10+
11+
thread::scope(|s| {
12+
s.spawn(|| {
13+
let ptr = &a as *const AtomicU16 as *mut u16;
14+
unsafe { ptr.read() };
15+
});
16+
s.spawn(|| {
17+
thread::yield_now();
18+
19+
// We also put a non-atomic access here, but that should *not* be reported.
20+
let ptr = &a as *const AtomicU16 as *mut u16;
21+
unsafe { ptr.read() };
22+
// Then do the atomic access.
23+
a.load(Ordering::SeqCst);
24+
//~^ ERROR: Data race detected between (1) Read on thread `<unnamed>` and (2) Atomic Load on thread `<unnamed>`
25+
});
26+
});
27+
}

‎src/tools/miri/tests/fail/data_race/read_read_race1.stderr

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
error: Undefined Behavior: Data race detected between (1) Read on thread `<unnamed>` and (2) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
2+
--> $DIR/read_read_race1.rs:LL:CC
3+
|
4+
LL | a.load(Ordering::SeqCst);
5+
| ^^^^^^^^^^^^^^^^^^^^^^^^ Data race detected between (1) Read on thread `<unnamed>` and (2) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
6+
|
7+
help: and (1) occurred earlier here
8+
--> $DIR/read_read_race1.rs:LL:CC
9+
|
10+
LL | unsafe { ptr.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/read_read_race1.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+

‎src/tools/miri/tests/fail/data_race/read_read_race2.rs

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
//@compile-flags: -Zmiri-preemption-rate=0.0
2+
use std::sync::atomic::{AtomicU16, Ordering};
3+
use std::thread;
4+
5+
// Make sure races between atomic and non-atomic reads are detected.
6+
// This seems harmless but C++ does not allow them, so we can't allow them for now either.
7+
// This test coverse the case where the atomic access come first.
8+
fn main() {
9+
let a = AtomicU16::new(0);
10+
11+
thread::scope(|s| {
12+
s.spawn(|| {
13+
// We also put a non-atomic access here, but that should *not* be reported.
14+
let ptr = &a as *const AtomicU16 as *mut u16;
15+
unsafe { ptr.read() };
16+
// Then do the atomic access.
17+
a.load(Ordering::SeqCst);
18+
});
19+
s.spawn(|| {
20+
thread::yield_now();
21+
22+
let ptr = &a as *const AtomicU16 as *mut u16;
23+
unsafe { ptr.read() };
24+
//~^ ERROR: Data race detected between (1) Atomic Load on thread `<unnamed>` and (2) Read on thread `<unnamed>`
25+
});
26+
});
27+
}

‎src/tools/miri/tests/fail/data_race/read_read_race2.stderr

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
error: Undefined Behavior: Data race detected between (1) Atomic Load on thread `<unnamed>` and (2) Read on thread `<unnamed>` at ALLOC. (2) just happened here
2+
--> $DIR/read_read_race2.rs:LL:CC
3+
|
4+
LL | unsafe { ptr.read() };
5+
| ^^^^^^^^^^ Data race detected between (1) Atomic Load on thread `<unnamed>` and (2) Read on thread `<unnamed>` at ALLOC. (2) just happened here
6+
|
7+
help: and (1) occurred earlier here
8+
--> $DIR/read_read_race2.rs:LL:CC
9+
|
10+
LL | a.load(Ordering::SeqCst);
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/read_read_race2.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+

‎src/tools/miri/tests/fail/weak_memory/racing_mixed_size.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ fn split_u32_ptr(dword: *const u32) -> *const [u16; 2] {
1919

2020
// Wine's SRWLock implementation does this, which is definitely undefined in C++ memory model
2121
// https://github.com/wine-mirror/wine/blob/303f8042f9db508adaca02ef21f8de4992cb9c03/dlls/ntdll/sync.c#L543-L566
22-
// Though it probably works just fine on x86
22+
// It probably works just fine on x86, but Intel does document this as "don't do it!"
2323
pub fn main() {
2424
let x = static_atomic_u32(0);
2525
let j1 = spawn(move || {
@@ -31,7 +31,7 @@ pub fn main() {
3131
let x_split = split_u32_ptr(x_ptr);
3232
unsafe {
3333
let hi = ptr::addr_of!((*x_split)[0]);
34-
std::intrinsics::atomic_load_relaxed(hi); //~ ERROR: imperfectly overlapping
34+
std::intrinsics::atomic_load_relaxed(hi); //~ ERROR: different-size
3535
}
3636
});
3737

‎src/tools/miri/tests/fail/weak_memory/racing_mixed_size.stderr

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,17 @@
1-
error: unsupported operation: racy imperfectly overlapping atomic access is not possible in the C++20 memory model, and not supported by Miri's weak memory emulation
1+
error: Undefined Behavior: Race condition detected between (1) 4-byte Atomic Store on thread `<unnamed>` and (2) 2-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
22
--> $DIR/racing_mixed_size.rs:LL:CC
33
|
44
LL | std::intrinsics::atomic_load_relaxed(hi);
5-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ racy imperfectly overlapping atomic access is not possible in the C++20 memory model, and not supported by Miri's weak memory emulation
5+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 4-byte Atomic Store on thread `<unnamed>` and (2) 2-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
66
|
7-
= help: this is likely not a bug in the program; it indicates that the program performed an operation that the interpreter does not support
8-
= note: BACKTRACE:
7+
help: and (1) occurred earlier here
8+
--> $DIR/racing_mixed_size.rs:LL:CC
9+
|
10+
LL | x.store(1, Relaxed);
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):
915
= note: inside closure at $DIR/racing_mixed_size.rs:LL:CC
1016

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

‎src/tools/miri/tests/fail/weak_memory/racing_mixed_size_read.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ fn split_u32_ptr(dword: *const u32) -> *const [u16; 2] {
1616

1717
// Racing mixed size reads may cause two loads to read-from
1818
// the same store but observe different values, which doesn't make
19-
// sense under the formal model so we forbade this.
19+
// sense under the formal model so we forbid this.
2020
pub fn main() {
2121
let x = static_atomic(0);
2222

@@ -29,7 +29,7 @@ pub fn main() {
2929
let x_split = split_u32_ptr(x_ptr);
3030
unsafe {
3131
let hi = x_split as *const u16 as *const AtomicU16;
32-
(*hi).load(Relaxed); //~ ERROR: imperfectly overlapping
32+
(*hi).load(Relaxed); //~ ERROR: different-size
3333
}
3434
});
3535

‎src/tools/miri/tests/fail/weak_memory/racing_mixed_size_read.stderr

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,17 @@
1-
error: unsupported operation: racy imperfectly overlapping atomic access is not possible in the C++20 memory model, and not supported by Miri's weak memory emulation
1+
error: Undefined Behavior: Race condition detected between (1) 4-byte Atomic Load on thread `<unnamed>` and (2) 2-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
22
--> $DIR/racing_mixed_size_read.rs:LL:CC
33
|
44
LL | (*hi).load(Relaxed);
5-
| ^^^^^^^^^^^^^^^^^^^ racy imperfectly overlapping atomic access is not possible in the C++20 memory model, and not supported by Miri's weak memory emulation
5+
| ^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 4-byte Atomic Load on thread `<unnamed>` and (2) 2-byte (different-size) Atomic Load on thread `<unnamed>` at ALLOC. (2) just happened here
66
|
7-
= help: this is likely not a bug in the program; it indicates that the program performed an operation that the interpreter does not support
8-
= note: BACKTRACE:
7+
help: and (1) occurred earlier here
8+
--> $DIR/racing_mixed_size_read.rs:LL:CC
9+
|
10+
LL | x.load(Relaxed);
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):
915
= note: inside closure at $DIR/racing_mixed_size_read.rs:LL:CC
1016

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

0 commit comments

Comments
 (0)