add a flag to print a diagnostic when an outdated value is returned f…

…rom an atomic load

README.md

@@ -377,6 +377,9 @@ to Miri failing to detect cases of undefined behavior in a program.
  happening and where in your code would be a good place to look for it.
  Specifying this argument multiple times does not overwrite the previous
  values, instead it appends its values to the list. Listing a tag multiple times has no effect.
+* `-Zmiri-track-weak-memory-loads` shows a backtrace when weak memory emulation returns an outdated
+ value from a load. This can help diagnose problems that disappear under
+ `-Zmiri-disable-weak-memory-emulation`.
 
 [function ABI]: https://doc.rust-lang.org/reference/items/functions.html#extern-function-qualifier
 

src/bin/miri.rs

@@ -358,6 +358,8 @@ fn main() {
  miri_config.isolated_op = miri::IsolatedOp::Allow;
  } else if arg == "-Zmiri-disable-weak-memory-emulation" {
  miri_config.weak_memory_emulation = false;
+ } else if arg == "-Zmiri-track-weak-memory-loads" {
+ miri_config.track_outdated_loads = true;
  } else if let Some(param) = arg.strip_prefix("-Zmiri-isolation-error=") {
  if matches!(isolation_enabled, Some(false)) {
  panic!("-Zmiri-isolation-error cannot be used along with -Zmiri-disable-isolation");

src/concurrency/data_race.rs

@@ -1187,12 +1187,15 @@ pub struct GlobalState {
 
  /// The timestamp of last SC write performed by each thread
  last_sc_write: RefCell<VClock>,
+
+ /// Track when an outdated (weak memory) load happens.
+ pub track_outdated_loads: bool,
 }
 
 impl GlobalState {
  /// Create a new global state, setup with just thread-id=0
  /// advanced to timestamp = 1.
- pub fn new() -> Self {
+ pub fn new(config: &MiriConfig) -> Self {
  let mut global_state = GlobalState {
  multi_threaded: Cell::new(false),
  ongoing_action_data_race_free: Cell::new(false),
@@ -1203,6 +1206,7 @@ impl GlobalState {
  terminated_threads: RefCell::new(FxHashMap::default()),
  last_sc_fence: RefCell::new(VClock::default()),
  last_sc_write: RefCell::new(VClock::default()),
+ track_outdated_loads: config.track_outdated_loads,
  };
 
  // Setup the main-thread since it is not explicitly created:

src/concurrency/weak_memory.rs

@@ -82,10 +82,7 @@ use rustc_const_eval::interpret::{
 };
 use rustc_data_structures::fx::FxHashMap;
 
-use crate::{
- AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, Provenance, ThreadManager, VClock, VTimestamp,
- VectorIdx,
-};
+use crate::*;
 
 use super::{
  data_race::{GlobalState as DataRaceState, ThreadClockSet},
@@ -113,6 +110,13 @@ pub(super) struct StoreBuffer {
  buffer: VecDeque<StoreElement>,
 }
 
+/// Whether a load returned the latest value or not.
+#[derive(PartialEq, Eq)]
+enum LoadRecency {
+ Latest,
+ Outdated,
+}
+
 #[derive(Debug, Clone, PartialEq, Eq)]
 struct StoreElement {
  /// The identifier of the vector index, corresponding to a thread
@@ -254,11 +258,11 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
  is_seqcst: bool,
  rng: &mut (impl rand::Rng + ?Sized),
  validate: impl FnOnce() -> InterpResult<'tcx>,
- ) -> InterpResult<'tcx, ScalarMaybeUninit<Provenance>> {
+ ) -> InterpResult<'tcx, (ScalarMaybeUninit<Provenance>, LoadRecency)> {
  // Having a live borrow to store_buffer while calling validate_atomic_load is fine
  // because the race detector doesn't touch store_buffer
 
- let store_elem = {
+ let (store_elem, recency) = {
  // The `clocks` we got here must be dropped before calling validate_atomic_load
  // as the race detector will update it
  let (.., clocks) = global.current_thread_state(thread_mgr);
@@ -274,7 +278,7 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
 
  let (index, clocks) = global.current_thread_state(thread_mgr);
  let loaded = store_elem.load_impl(index, &clocks);
- Ok(loaded)
+ Ok((loaded, recency))
  }
 
  fn buffered_write(
@@ -296,7 +300,7 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
  is_seqcst: bool,
  clocks: &ThreadClockSet,
  rng: &mut R,
- ) -> &StoreElement {
+ ) -> (&StoreElement, LoadRecency) {
  use rand::seq::IteratorRandom;
  let mut found_sc = false;
  // FIXME: we want an inclusive take_while (stops after a false predicate, but
@@ -359,9 +363,14 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
  }
  });
 
- candidates
+ let chosen = candidates
  .choose(rng)
- .expect("store buffer cannot be empty, an element is populated on construction")
+ .expect("store buffer cannot be empty");
+ if std::ptr::eq(chosen, self.buffer.back().expect("store buffer cannot be empty")) {
+ (chosen, LoadRecency::Latest)
+ } else {
+ (chosen, LoadRecency::Outdated)
+ }
  }
 
  /// ATOMIC STORE IMPL in the paper (except we don't need the location's vector clock)
@@ -499,13 +508,16 @@ pub(super) trait EvalContextExt<'mir, 'tcx: 'mir>:
  alloc_range(base_offset, place.layout.size),
  latest_in_mo,
  )?;
- let loaded = buffer.buffered_read(
+ let (loaded, recency) = buffer.buffered_read(
  global,
  &this.machine.threads,
  atomic == AtomicReadOrd::SeqCst,
  &mut *rng,
  validate,
  )?;
+ if global.track_outdated_loads && recency == LoadRecency::Outdated {
+ register_diagnostic(NonHaltingDiagnostic::WeakMemoryOutdatedLoad);
+ }
 
  return Ok(loaded);
  }

src/diagnostics.rs

@@ -74,6 +74,7 @@ pub enum NonHaltingDiagnostic {
  Int2Ptr {
  details: bool,
  },
+ WeakMemoryOutdatedLoad,
 }
 
 /// Level of Miri specific diagnostics
@@ -474,6 +475,8 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
  format!("progress report: current operation being executed is here"),
  Int2Ptr { .. } =>
  format!("integer-to-pointer cast"),
+ WeakMemoryOutdatedLoad =>
+ format!("weak memory emulation: outdated value returned from load"),
  };
 
  let (title, diag_level) = match e {
@@ -485,7 +488,9 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
  | CreatedCallId(..)
  | CreatedAlloc(..)
  | FreedAlloc(..)
- | ProgressReport => ("tracking was triggered", DiagLevel::Note),
+ | ProgressReport
+ | WeakMemoryOutdatedLoad =>
+ ("tracking was triggered", DiagLevel::Note),
  };
 
  let helps = match e {

src/eval.rs

@@ -102,6 +102,8 @@ pub struct MiriConfig {
  pub data_race_detector: bool,
  /// Determine if weak memory emulation should be enabled. Requires data race detection to be enabled
  pub weak_memory_emulation: bool,
+ /// Track when an outdated (weak memory) load happens.
+ pub track_outdated_loads: bool,
  /// Rate of spurious failures for compare_exchange_weak atomic operations,
  /// between 0.0 and 1.0, defaulting to 0.8 (80% chance of failure).
  pub cmpxchg_weak_failure_rate: f64,
@@ -143,6 +145,7 @@ impl Default for MiriConfig {
  tracked_alloc_ids: HashSet::default(),
  data_race_detector: true,
  weak_memory_emulation: true,
+ track_outdated_loads: false,
  cmpxchg_weak_failure_rate: 0.8, // 80%
  measureme_out: None,
  panic_on_unsupported: false,

src/machine.rs

@@ -376,8 +376,11 @@ impl<'mir, 'tcx> Evaluator<'mir, 'tcx> {
  } else {
  None
  };
- let data_race =
- if config.data_race_detector { Some(data_race::GlobalState::new()) } else { None };
+ let data_race = if config.data_race_detector {
+ Some(data_race::GlobalState::new(config))
+ } else {
+ None
+ };
  Evaluator {
  stacked_borrows,
  data_race,