Skip to content

Commit 302e9ae

Browse files
committed
Auto merge of #2424 - RalfJung:weak-memory-debug, r=RalfJung
add a flag to print a diagnostic when an outdated value is returned from an atomic load Helps with #2313. It can still be annoying to figure out *which* outdated load is the important one in case there are many of them (and the issue contains some ideas for how to help with that situation), but having this flag is better than nothing. Thanks to `@cbeuw` for the [original patch](cbeuw@64d738c) that I based this on.
2 parents b9aad98 + 649b216 commit 302e9ae

File tree

7 files changed

+46
-16
lines changed

7 files changed

+46
-16
lines changed

README.md

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -377,6 +377,9 @@ to Miri failing to detect cases of undefined behavior in a program.
377377
happening and where in your code would be a good place to look for it.
378378
Specifying this argument multiple times does not overwrite the previous
379379
values, instead it appends its values to the list. Listing a tag multiple times has no effect.
380+
* `-Zmiri-track-weak-memory-loads` shows a backtrace when weak memory emulation returns an outdated
381+
value from a load. This can help diagnose problems that disappear under
382+
`-Zmiri-disable-weak-memory-emulation`.
380383

381384
[function ABI]: https://doc.rust-lang.org/reference/items/functions.html#extern-function-qualifier
382385

src/bin/miri.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -358,6 +358,8 @@ fn main() {
358358
miri_config.isolated_op = miri::IsolatedOp::Allow;
359359
} else if arg == "-Zmiri-disable-weak-memory-emulation" {
360360
miri_config.weak_memory_emulation = false;
361+
} else if arg == "-Zmiri-track-weak-memory-loads" {
362+
miri_config.track_outdated_loads = true;
361363
} else if let Some(param) = arg.strip_prefix("-Zmiri-isolation-error=") {
362364
if matches!(isolation_enabled, Some(false)) {
363365
panic!("-Zmiri-isolation-error cannot be used along with -Zmiri-disable-isolation");

src/concurrency/data_race.rs

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1187,12 +1187,15 @@ pub struct GlobalState {
11871187

11881188
/// The timestamp of last SC write performed by each thread
11891189
last_sc_write: RefCell<VClock>,
1190+
1191+
/// Track when an outdated (weak memory) load happens.
1192+
pub track_outdated_loads: bool,
11901193
}
11911194

11921195
impl GlobalState {
11931196
/// Create a new global state, setup with just thread-id=0
11941197
/// advanced to timestamp = 1.
1195-
pub fn new() -> Self {
1198+
pub fn new(config: &MiriConfig) -> Self {
11961199
let mut global_state = GlobalState {
11971200
multi_threaded: Cell::new(false),
11981201
ongoing_action_data_race_free: Cell::new(false),
@@ -1203,6 +1206,7 @@ impl GlobalState {
12031206
terminated_threads: RefCell::new(FxHashMap::default()),
12041207
last_sc_fence: RefCell::new(VClock::default()),
12051208
last_sc_write: RefCell::new(VClock::default()),
1209+
track_outdated_loads: config.track_outdated_loads,
12061210
};
12071211

12081212
// Setup the main-thread since it is not explicitly created:

src/concurrency/weak_memory.rs

Lines changed: 22 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -82,10 +82,7 @@ use rustc_const_eval::interpret::{
8282
};
8383
use rustc_data_structures::fx::FxHashMap;
8484

85-
use crate::{
86-
AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, Provenance, ThreadManager, VClock, VTimestamp,
87-
VectorIdx,
88-
};
85+
use crate::*;
8986

9087
use super::{
9188
data_race::{GlobalState as DataRaceState, ThreadClockSet},
@@ -113,6 +110,13 @@ pub(super) struct StoreBuffer {
113110
buffer: VecDeque<StoreElement>,
114111
}
115112

113+
/// Whether a load returned the latest value or not.
114+
#[derive(PartialEq, Eq)]
115+
enum LoadRecency {
116+
Latest,
117+
Outdated,
118+
}
119+
116120
#[derive(Debug, Clone, PartialEq, Eq)]
117121
struct StoreElement {
118122
/// The identifier of the vector index, corresponding to a thread
@@ -254,11 +258,11 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
254258
is_seqcst: bool,
255259
rng: &mut (impl rand::Rng + ?Sized),
256260
validate: impl FnOnce() -> InterpResult<'tcx>,
257-
) -> InterpResult<'tcx, ScalarMaybeUninit<Provenance>> {
261+
) -> InterpResult<'tcx, (ScalarMaybeUninit<Provenance>, LoadRecency)> {
258262
// Having a live borrow to store_buffer while calling validate_atomic_load is fine
259263
// because the race detector doesn't touch store_buffer
260264

261-
let store_elem = {
265+
let (store_elem, recency) = {
262266
// The `clocks` we got here must be dropped before calling validate_atomic_load
263267
// as the race detector will update it
264268
let (.., clocks) = global.current_thread_state(thread_mgr);
@@ -274,7 +278,7 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
274278

275279
let (index, clocks) = global.current_thread_state(thread_mgr);
276280
let loaded = store_elem.load_impl(index, &clocks);
277-
Ok(loaded)
281+
Ok((loaded, recency))
278282
}
279283

280284
fn buffered_write(
@@ -296,7 +300,7 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
296300
is_seqcst: bool,
297301
clocks: &ThreadClockSet,
298302
rng: &mut R,
299-
) -> &StoreElement {
303+
) -> (&StoreElement, LoadRecency) {
300304
use rand::seq::IteratorRandom;
301305
let mut found_sc = false;
302306
// FIXME: we want an inclusive take_while (stops after a false predicate, but
@@ -359,9 +363,12 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
359363
}
360364
});
361365

362-
candidates
363-
.choose(rng)
364-
.expect("store buffer cannot be empty, an element is populated on construction")
366+
let chosen = candidates.choose(rng).expect("store buffer cannot be empty");
367+
if std::ptr::eq(chosen, self.buffer.back().expect("store buffer cannot be empty")) {
368+
(chosen, LoadRecency::Latest)
369+
} else {
370+
(chosen, LoadRecency::Outdated)
371+
}
365372
}
366373

367374
/// ATOMIC STORE IMPL in the paper (except we don't need the location's vector clock)
@@ -499,13 +506,16 @@ pub(super) trait EvalContextExt<'mir, 'tcx: 'mir>:
499506
alloc_range(base_offset, place.layout.size),
500507
latest_in_mo,
501508
)?;
502-
let loaded = buffer.buffered_read(
509+
let (loaded, recency) = buffer.buffered_read(
503510
global,
504511
&this.machine.threads,
505512
atomic == AtomicReadOrd::SeqCst,
506513
&mut *rng,
507514
validate,
508515
)?;
516+
if global.track_outdated_loads && recency == LoadRecency::Outdated {
517+
register_diagnostic(NonHaltingDiagnostic::WeakMemoryOutdatedLoad);
518+
}
509519

510520
return Ok(loaded);
511521
}

src/diagnostics.rs

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,7 @@ pub enum NonHaltingDiagnostic {
7474
Int2Ptr {
7575
details: bool,
7676
},
77+
WeakMemoryOutdatedLoad,
7778
}
7879

7980
/// Level of Miri specific diagnostics
@@ -474,6 +475,8 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
474475
format!("progress report: current operation being executed is here"),
475476
Int2Ptr { .. } =>
476477
format!("integer-to-pointer cast"),
478+
WeakMemoryOutdatedLoad =>
479+
format!("weak memory emulation: outdated value returned from load"),
477480
};
478481

479482
let (title, diag_level) = match e {
@@ -485,7 +488,9 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
485488
| CreatedCallId(..)
486489
| CreatedAlloc(..)
487490
| FreedAlloc(..)
488-
| ProgressReport => ("tracking was triggered", DiagLevel::Note),
491+
| ProgressReport
492+
| WeakMemoryOutdatedLoad =>
493+
("tracking was triggered", DiagLevel::Note),
489494
};
490495

491496
let helps = match e {

src/eval.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,8 @@ pub struct MiriConfig {
102102
pub data_race_detector: bool,
103103
/// Determine if weak memory emulation should be enabled. Requires data race detection to be enabled
104104
pub weak_memory_emulation: bool,
105+
/// Track when an outdated (weak memory) load happens.
106+
pub track_outdated_loads: bool,
105107
/// Rate of spurious failures for compare_exchange_weak atomic operations,
106108
/// between 0.0 and 1.0, defaulting to 0.8 (80% chance of failure).
107109
pub cmpxchg_weak_failure_rate: f64,
@@ -143,6 +145,7 @@ impl Default for MiriConfig {
143145
tracked_alloc_ids: HashSet::default(),
144146
data_race_detector: true,
145147
weak_memory_emulation: true,
148+
track_outdated_loads: false,
146149
cmpxchg_weak_failure_rate: 0.8, // 80%
147150
measureme_out: None,
148151
panic_on_unsupported: false,

src/machine.rs

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -376,8 +376,11 @@ impl<'mir, 'tcx> Evaluator<'mir, 'tcx> {
376376
} else {
377377
None
378378
};
379-
let data_race =
380-
if config.data_race_detector { Some(data_race::GlobalState::new()) } else { None };
379+
let data_race = if config.data_race_detector {
380+
Some(data_race::GlobalState::new(config))
381+
} else {
382+
None
383+
};
381384
Evaluator {
382385
stacked_borrows,
383386
data_race,

0 commit comments

Comments
 (0)