Skip to content
This repository was archived by the owner on May 28, 2025. It is now read-only.

Commit a15eb7e

Browse files
borsbors
committed
Auto merge of rust-lang#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+

0 commit comments

Comments
 (0)