mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

data_race: clarify and slightly refactor non-atomic handling

Browse Source
This commit is contained in:
Ralf Jung 2023-10-22 10:32:52 +02:00
parent d32b1583df
commit a4e42ad185
1 changed files with 50 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

95
src/tools/miri/src/concurrency/data_race.rs
View File

@ -220,25 +220,22 @@ fn get_descriptor(self) -> &'static str {
/// for data-race detection. /// for data-race detection.
#[derive(Clone, PartialEq, Eq, Debug)] #[derive(Clone, PartialEq, Eq, Debug)]
struct MemoryCellClocks { struct MemoryCellClocks {
/// The vector-clock timestamp of the last write /// The vector-clock timestamp and the thread that did the last non-atomic write. We don't need
/// corresponding to the writing threads timestamp. /// a full `VClock` here, it's always a single thread and nothing synchronizes, so the effective
write: VTimestamp, /// clock is all-0 except for the thread that did the write.
write: (VectorIdx, VTimestamp),
/// The identifier of the vector index, corresponding to a thread
/// that performed the last write operation.
write_index: VectorIdx,
/// The type of operation that the write index represents, /// The type of operation that the write index represents,
/// either newly allocated memory, a non-atomic write or /// either newly allocated memory, a non-atomic write or
/// a deallocation of memory. /// a deallocation of memory.
write_type: WriteType, write_type: WriteType,
/// The vector-clock of the timestamp of the last read operation /// The vector-clock of all non-atomic reads that happened since the last non-atomic write
/// performed by a thread since the last write operation occurred. /// (i.e., we join together the "singleton" clocks corresponding to each read). It is reset to
/// It is reset to zero on each write operation. /// zero on each write operation.
read: VClock, read: VClock,
/// Atomic acquire & release sequence tracking clocks. /// Atomic access, acquire, release sequence tracking clocks.
/// For non-atomic memory in the common case this /// For non-atomic memory in the common case this
/// value is set to None. /// value is set to None.
atomic_ops: Option<Box<AtomicMemoryCellClocks>>, atomic_ops: Option<Box<AtomicMemoryCellClocks>>,
@ -250,13 +247,24 @@ impl MemoryCellClocks {
fn new(alloc: VTimestamp, alloc_index: VectorIdx) -> Self { fn new(alloc: VTimestamp, alloc_index: VectorIdx) -> Self {
MemoryCellClocks { MemoryCellClocks {
read: VClock::default(), read: VClock::default(),
write: alloc, write: (alloc_index, alloc),
write_index: alloc_index,
write_type: WriteType::Allocate, write_type: WriteType::Allocate,
atomic_ops: None, 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. /// Load the internal atomic memory cells if they exist.
#[inline] #[inline]
fn atomic(&self) -> Option<&AtomicMemoryCellClocks> { fn atomic(&self) -> Option<&AtomicMemoryCellClocks> {
@ -376,7 +384,7 @@ fn atomic_read_detect(
log::trace!("Atomic read with vectors: {:#?} :: {:#?}", self, thread_clocks); log::trace!("Atomic read with vectors: {:#?} :: {:#?}", self, thread_clocks);
let atomic = self.atomic_mut(); let atomic = self.atomic_mut();
atomic.read_vector.set_at_index(&thread_clocks.clock, index); 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 /// 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); log::trace!("Atomic write with vectors: {:#?} :: {:#?}", self, thread_clocks);
let atomic = self.atomic_mut(); let atomic = self.atomic_mut();
atomic.write_vector.set_at_index(&thread_clocks.clock, index); 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(()) Ok(())
} else { } else {
Err(DataRace) Err(DataRace)
@ -408,7 +416,7 @@ fn read_race_detect(
if !current_span.is_dummy() { if !current_span.is_dummy() {
thread_clocks.clock[index].span = current_span; 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() { let race_free = if let Some(atomic) = self.atomic() {
atomic.write_vector <= thread_clocks.clock atomic.write_vector <= thread_clocks.clock
} else { } else {
@ -434,15 +442,14 @@ fn write_race_detect(
if !current_span.is_dummy() { if !current_span.is_dummy() {
thread_clocks.clock[index].span = current_span; 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() { let race_free = if let Some(atomic) = self.atomic() {
atomic.write_vector <= thread_clocks.clock atomic.write_vector <= thread_clocks.clock
&& atomic.read_vector <= thread_clocks.clock && atomic.read_vector <= thread_clocks.clock
} else { } else {
true true
}; };
self.write = thread_clocks.clock[index]; self.write = (index, thread_clocks.clock[index]);
self.write_index = index;
self.write_type = write_type; self.write_type = write_type;
if race_free { if race_free {
self.read.set_zero_vector(); self.read.set_zero_vector();
@ -790,37 +797,35 @@ fn report_data_race<'tcx>(
) -> InterpResult<'tcx> { ) -> InterpResult<'tcx> {
let (current_index, current_clocks) = global.current_thread_state(thread_mgr); let (current_index, current_clocks) = global.current_thread_state(thread_mgr);
let write_clock; let write_clock;
let (other_action, other_thread, other_clock) = if mem_clocks.write #[rustfmt::skip]
> current_clocks.clock[mem_clocks.write_index] let (other_action, other_thread, other_clock) =
{ if mem_clocks.write.1 > current_clocks.clock[mem_clocks.write.0] {
// Convert the write action into the vector clock it write_clock = mem_clocks.write();
// represents for diagnostic purposes. (mem_clocks.write_type.get_descriptor(), mem_clocks.write.0, &write_clock)
write_clock = VClock::new_with_index(mem_clocks.write_index, mem_clocks.write); } else if let Some(idx) = Self::find_gt_index(&mem_clocks.read, &current_clocks.clock) {
(mem_clocks.write_type.get_descriptor(), mem_clocks.write_index, &write_clock) ("Read", idx, &mem_clocks.read)
} else if let Some(idx) = Self::find_gt_index(&mem_clocks.read, &current_clocks.clock) { } else if !is_atomic {
("Read", idx, &mem_clocks.read) if let Some(atomic) = mem_clocks.atomic() {
} else if !is_atomic { if let Some(idx) = Self::find_gt_index(&atomic.write_vector, &current_clocks.clock)
if let Some(atomic) = mem_clocks.atomic() { {
if let Some(idx) = Self::find_gt_index(&atomic.write_vector, &current_clocks.clock) ("Atomic Store", idx, &atomic.write_vector)
{ } else if let Some(idx) =
("Atomic Store", idx, &atomic.write_vector) Self::find_gt_index(&atomic.read_vector, &current_clocks.clock)
} else if let Some(idx) = {
Self::find_gt_index(&atomic.read_vector, &current_clocks.clock) ("Atomic Load", idx, &atomic.read_vector)
{ } else {
("Atomic Load", idx, &atomic.read_vector) unreachable!(
"Failed to report data-race for non-atomic operation: no race found"
)
}
} else { } else {
unreachable!( 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 { } else {
unreachable!( unreachable!("Failed to report data-race for atomic operation")
"Failed to report data-race for non-atomic operation: no atomic component" };
)
}
} else {
unreachable!("Failed to report data-race for atomic operation")
};
// Load elaborated thread information about the racing thread actions. // Load elaborated thread information about the racing thread actions.
let current_thread_info = global.print_thread_metadata(thread_mgr, current_index); let current_thread_info = global.print_thread_metadata(thread_mgr, current_index);