From a4e42ad185aa0dd904d892de14b27e0a9bc36c18 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sun, 22 Oct 2023 10:32:52 +0200 Subject: [PATCH] data_race: clarify and slightly refactor non-atomic handling --- src/tools/miri/src/concurrency/data_race.rs | 95 +++++++++++---------- 1 file changed, 50 insertions(+), 45 deletions(-) diff --git a/src/tools/miri/src/concurrency/data_race.rs b/src/tools/miri/src/concurrency/data_race.rs index e49d62177c5..0ef1f1442ee 100644 --- a/src/tools/miri/src/concurrency/data_race.rs +++ b/src/tools/miri/src/concurrency/data_race.rs @@ -220,25 +220,22 @@ fn get_descriptor(self) -> &'static str { /// for data-race detection. #[derive(Clone, PartialEq, Eq, Debug)] struct MemoryCellClocks { - /// The vector-clock timestamp of the last write - /// corresponding to the writing threads timestamp. - write: VTimestamp, - - /// The identifier of the vector index, corresponding to a thread - /// that performed the last write operation. - write_index: VectorIdx, + /// The vector-clock timestamp and the thread that did the last non-atomic write. We don't need + /// a full `VClock` here, it's always a single thread and nothing synchronizes, so the effective + /// clock is all-0 except for the thread that did the write. + write: (VectorIdx, VTimestamp), /// The type of operation that the write index represents, /// either newly allocated memory, a non-atomic write or /// a deallocation of memory. write_type: WriteType, - /// The vector-clock of the timestamp of the last read operation - /// performed by a thread since the last write operation occurred. - /// It is reset to zero on each write operation. + /// The vector-clock of all non-atomic reads that happened since the last non-atomic write + /// (i.e., we join together the "singleton" clocks corresponding to each read). It is reset to + /// zero on each write operation. read: VClock, - /// Atomic acquire & release sequence tracking clocks. + /// Atomic access, acquire, release sequence tracking clocks. /// For non-atomic memory in the common case this /// value is set to None. atomic_ops: Option>, @@ -250,13 +247,24 @@ impl MemoryCellClocks { fn new(alloc: VTimestamp, alloc_index: VectorIdx) -> Self { MemoryCellClocks { read: VClock::default(), - write: alloc, - write_index: alloc_index, + write: (alloc_index, alloc), write_type: WriteType::Allocate, atomic_ops: None, } } + #[inline] + fn write_was_before(&self, other: &VClock) -> bool { + // This is the same as `self.write() <= other` but + // without actually manifesting a clock for `self.write`. + self.write.1 <= other[self.write.0] + } + + #[inline] + fn write(&self) -> VClock { + VClock::new_with_index(self.write.0, self.write.1) + } + /// Load the internal atomic memory cells if they exist. #[inline] fn atomic(&self) -> Option<&AtomicMemoryCellClocks> { @@ -376,7 +384,7 @@ fn atomic_read_detect( log::trace!("Atomic read with vectors: {:#?} :: {:#?}", self, thread_clocks); let atomic = self.atomic_mut(); atomic.read_vector.set_at_index(&thread_clocks.clock, index); - if self.write <= thread_clocks.clock[self.write_index] { Ok(()) } else { Err(DataRace) } + if self.write_was_before(&thread_clocks.clock) { Ok(()) } else { Err(DataRace) } } /// Detect data-races with an atomic write, either with a non-atomic read or with @@ -389,7 +397,7 @@ fn atomic_write_detect( log::trace!("Atomic write with vectors: {:#?} :: {:#?}", self, thread_clocks); let atomic = self.atomic_mut(); atomic.write_vector.set_at_index(&thread_clocks.clock, index); - if self.write <= thread_clocks.clock[self.write_index] && self.read <= thread_clocks.clock { + if self.write_was_before(&thread_clocks.clock) && self.read <= thread_clocks.clock { Ok(()) } else { Err(DataRace) @@ -408,7 +416,7 @@ fn read_race_detect( if !current_span.is_dummy() { thread_clocks.clock[index].span = current_span; } - if self.write <= thread_clocks.clock[self.write_index] { + if self.write_was_before(&thread_clocks.clock) { let race_free = if let Some(atomic) = self.atomic() { atomic.write_vector <= thread_clocks.clock } else { @@ -434,15 +442,14 @@ fn write_race_detect( if !current_span.is_dummy() { thread_clocks.clock[index].span = current_span; } - if self.write <= thread_clocks.clock[self.write_index] && self.read <= thread_clocks.clock { + if self.write_was_before(&thread_clocks.clock) && self.read <= thread_clocks.clock { let race_free = if let Some(atomic) = self.atomic() { atomic.write_vector <= thread_clocks.clock && atomic.read_vector <= thread_clocks.clock } else { true }; - self.write = thread_clocks.clock[index]; - self.write_index = index; + self.write = (index, thread_clocks.clock[index]); self.write_type = write_type; if race_free { self.read.set_zero_vector(); @@ -790,37 +797,35 @@ fn report_data_race<'tcx>( ) -> InterpResult<'tcx> { let (current_index, current_clocks) = global.current_thread_state(thread_mgr); let write_clock; - let (other_action, other_thread, other_clock) = if mem_clocks.write - > current_clocks.clock[mem_clocks.write_index] - { - // Convert the write action into the vector clock it - // represents for diagnostic purposes. - write_clock = VClock::new_with_index(mem_clocks.write_index, mem_clocks.write); - (mem_clocks.write_type.get_descriptor(), mem_clocks.write_index, &write_clock) - } else if let Some(idx) = Self::find_gt_index(&mem_clocks.read, ¤t_clocks.clock) { - ("Read", idx, &mem_clocks.read) - } else if !is_atomic { - if let Some(atomic) = mem_clocks.atomic() { - if let Some(idx) = Self::find_gt_index(&atomic.write_vector, ¤t_clocks.clock) - { - ("Atomic Store", idx, &atomic.write_vector) - } else if let Some(idx) = - Self::find_gt_index(&atomic.read_vector, ¤t_clocks.clock) - { - ("Atomic Load", idx, &atomic.read_vector) + #[rustfmt::skip] + let (other_action, other_thread, other_clock) = + if mem_clocks.write.1 > current_clocks.clock[mem_clocks.write.0] { + write_clock = mem_clocks.write(); + (mem_clocks.write_type.get_descriptor(), mem_clocks.write.0, &write_clock) + } else if let Some(idx) = Self::find_gt_index(&mem_clocks.read, ¤t_clocks.clock) { + ("Read", idx, &mem_clocks.read) + } else if !is_atomic { + if let Some(atomic) = mem_clocks.atomic() { + if let Some(idx) = Self::find_gt_index(&atomic.write_vector, ¤t_clocks.clock) + { + ("Atomic Store", idx, &atomic.write_vector) + } else if let Some(idx) = + Self::find_gt_index(&atomic.read_vector, ¤t_clocks.clock) + { + ("Atomic Load", idx, &atomic.read_vector) + } else { + unreachable!( + "Failed to report data-race for non-atomic operation: no race found" + ) + } } else { unreachable!( - "Failed to report data-race for non-atomic operation: no race found" + "Failed to report data-race for non-atomic operation: no atomic component" ) } } else { - unreachable!( - "Failed to report data-race for non-atomic operation: no atomic component" - ) - } - } else { - unreachable!("Failed to report data-race for atomic operation") - }; + unreachable!("Failed to report data-race for atomic operation") + }; // Load elaborated thread information about the racing thread actions. let current_thread_info = global.print_thread_metadata(thread_mgr, current_index);