1 //! Implementation of a data-race detector using Lamport Timestamps / Vector-clocks
2 //! based on the Dynamic Race Detection for C++:
3 //! <https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf>
4 //! which does not report false-positives when fences are used, and gives better
5 //! accuracy in presence of read-modify-write operations.
7 //! The implementation contains modifications to correctly model the changes to the memory model in C++20
8 //! regarding the weakening of release sequences: <http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0982r1.html>.
9 //! Relaxed stores now unconditionally block all currently active release sequences and so per-thread tracking of release
10 //! sequences is not needed.
12 //! The implementation also models races with memory allocation and deallocation via treating allocation and
13 //! deallocation as a type of write internally for detecting data-races.
15 //! Weak memory orders are explored but not all weak behaviours are exhibited, so it can still miss data-races
16 //! but should not report false-positives
18 //! Data-race definition from(<https://en.cppreference.com/w/cpp/language/memory_model#Threads_and_data_races>):
19 //! a data race occurs between two memory accesses if they are on different threads, at least one operation
20 //! is non-atomic, at least one operation is a write and neither access happens-before the other. Read the link
21 //! for full definition.
23 //! This re-uses vector indexes for threads that are known to be unable to report data-races, this is valid
24 //! because it only re-uses vector indexes once all currently-active (not-terminated) threads have an internal
25 //! vector clock that happens-after the join operation of the candidate thread. Threads that have not been joined
26 //! on are not considered. Since the thread's vector clock will only increase and a data-race implies that
27 //! there is some index x where clock\[x\] > thread_clock, when this is true clock\[candidate-idx\] > thread_clock
28 //! can never hold and hence a data-race can never be reported in that vector index again.
29 //! This means that the thread-index can be safely re-used, starting on the next timestamp for the newly created
32 //! The timestamps used in the data-race detector assign each sequence of non-atomic operations
33 //! followed by a single atomic or concurrent operation a single timestamp.
34 //! Write, Read, Write, ThreadJoin will be represented by a single timestamp value on a thread.
35 //! This is because extra increment operations between the operations in the sequence are not
36 //! required for accurate reporting of data-race values.
38 //! As per the paper a threads timestamp is only incremented after a release operation is performed
39 //! so some atomic operations that only perform acquires do not increment the timestamp. Due to shared
40 //! code some atomic operations may increment the timestamp when not necessary but this has no effect
41 //! on the data-race detection code.
44 //! currently we have our own local copy of the currently active thread index and names, this is due
45 //! in part to the inability to access the current location of threads.active_thread inside the AllocExtra
46 //! read, write and deallocate functions and should be cleaned up in the future.
49 cell::{Cell, Ref, RefCell, RefMut},
54 use rustc_data_structures::fx::{FxHashMap, FxHashSet};
55 use rustc_index::vec::{Idx, IndexVec};
56 use rustc_middle::{mir, ty::layout::TyAndLayout};
57 use rustc_target::abi::Size;
61 use super::weak_memory::EvalContextExt as _;
63 pub type AllocExtra = VClockAlloc;
65 /// Valid atomic read-write operations, alias of atomic::Ordering (not non-exhaustive).
66 #[derive(Copy, Clone, PartialEq, Eq, Debug)]
75 /// Valid atomic read operations, subset of atomic::Ordering.
76 #[derive(Copy, Clone, PartialEq, Eq, Debug)]
77 pub enum AtomicReadOp {
83 /// Valid atomic write operations, subset of atomic::Ordering.
84 #[derive(Copy, Clone, PartialEq, Eq, Debug)]
85 pub enum AtomicWriteOp {
91 /// Valid atomic fence operations, subset of atomic::Ordering.
92 #[derive(Copy, Clone, PartialEq, Eq, Debug)]
93 pub enum AtomicFenceOp {
100 /// The current set of vector clocks describing the state
101 /// of a thread, contains the happens-before clock and
102 /// additional metadata to model atomic fence operations.
103 #[derive(Clone, Default, Debug)]
104 pub(super) struct ThreadClockSet {
105 /// The increasing clock representing timestamps
106 /// that happen-before this thread.
107 pub(super) clock: VClock,
109 /// The set of timestamps that will happen-before this
110 /// thread once it performs an acquire fence.
111 fence_acquire: VClock,
113 /// The last timestamp of happens-before relations that
114 /// have been released by this thread by a fence.
115 fence_release: VClock,
117 /// Timestamps of the last SC fence performed by each
118 /// thread, updated when this thread performs an SC fence
119 pub(super) fence_seqcst: VClock,
121 /// Timestamps of the last SC write performed by each
122 /// thread, updated when this thread performs an SC fence
123 pub(super) write_seqcst: VClock,
125 /// Timestamps of the last SC fence performed by each
126 /// thread, updated when this thread performs an SC read
127 pub(super) read_seqcst: VClock,
130 impl ThreadClockSet {
131 /// Apply the effects of a release fence to this
132 /// set of thread vector clocks.
134 fn apply_release_fence(&mut self) {
135 self.fence_release.clone_from(&self.clock);
138 /// Apply the effects of an acquire fence to this
139 /// set of thread vector clocks.
141 fn apply_acquire_fence(&mut self) {
142 self.clock.join(&self.fence_acquire);
145 /// Increment the happens-before clock at a
148 fn increment_clock(&mut self, index: VectorIdx) {
149 self.clock.increment_index(index);
152 /// Join the happens-before clock with that of
153 /// another thread, used to model thread join
155 fn join_with(&mut self, other: &ThreadClockSet) {
156 self.clock.join(&other.clock);
160 /// Error returned by finding a data race
161 /// should be elaborated upon.
162 #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
165 /// Externally stored memory cell clocks
166 /// explicitly to reduce memory usage for the
167 /// common case where no atomic operations
168 /// exists on the memory cell.
169 #[derive(Clone, PartialEq, Eq, Default, Debug)]
170 struct AtomicMemoryCellClocks {
171 /// The clock-vector of the timestamp of the last atomic
172 /// read operation performed by each thread.
173 /// This detects potential data-races between atomic read
174 /// and non-atomic write operations.
177 /// The clock-vector of the timestamp of the last atomic
178 /// write operation performed by each thread.
179 /// This detects potential data-races between atomic write
180 /// and non-atomic read or write operations.
181 write_vector: VClock,
183 /// Synchronization vector for acquire-release semantics
184 /// contains the vector of timestamps that will
185 /// happen-before a thread if an acquire-load is
186 /// performed on the data.
190 /// Type of write operation: allocating memory
191 /// non-atomic writes and deallocating memory
192 /// are all treated as writes for the purpose
193 /// of the data-race detector.
194 #[derive(Copy, Clone, PartialEq, Eq, Debug)]
199 /// Standard unsynchronized write.
202 /// Deallocate memory.
203 /// Note that when memory is deallocated first, later non-atomic accesses
204 /// will be reported as use-after-free, not as data races.
205 /// (Same for `Allocate` above.)
209 fn get_descriptor(self) -> &'static str {
211 WriteType::Allocate => "Allocate",
212 WriteType::Write => "Write",
213 WriteType::Deallocate => "Deallocate",
218 /// Memory Cell vector clock metadata
219 /// for data-race detection.
220 #[derive(Clone, PartialEq, Eq, Debug)]
221 struct MemoryCellClocks {
222 /// The vector-clock timestamp of the last write
223 /// corresponding to the writing threads timestamp.
226 /// The identifier of the vector index, corresponding to a thread
227 /// that performed the last write operation.
228 write_index: VectorIdx,
230 /// The type of operation that the write index represents,
231 /// either newly allocated memory, a non-atomic write or
232 /// a deallocation of memory.
233 write_type: WriteType,
235 /// The vector-clock of the timestamp of the last read operation
236 /// performed by a thread since the last write operation occurred.
237 /// It is reset to zero on each write operation.
240 /// Atomic acquire & release sequence tracking clocks.
241 /// For non-atomic memory in the common case this
242 /// value is set to None.
243 atomic_ops: Option<Box<AtomicMemoryCellClocks>>,
246 impl MemoryCellClocks {
247 /// Create a new set of clocks representing memory allocated
248 /// at a given vector timestamp and index.
249 fn new(alloc: VTimestamp, alloc_index: VectorIdx) -> Self {
251 read: VClock::default(),
253 write_index: alloc_index,
254 write_type: WriteType::Allocate,
259 /// Load the internal atomic memory cells if they exist.
261 fn atomic(&self) -> Option<&AtomicMemoryCellClocks> {
262 match &self.atomic_ops {
263 Some(op) => Some(&*op),
268 /// Load or create the internal atomic memory metadata
269 /// if it does not exist.
271 fn atomic_mut(&mut self) -> &mut AtomicMemoryCellClocks {
272 self.atomic_ops.get_or_insert_with(Default::default)
275 /// Update memory cell data-race tracking for atomic
276 /// load acquire semantics, is a no-op if this memory was
277 /// not used previously as atomic memory.
280 clocks: &mut ThreadClockSet,
282 ) -> Result<(), DataRace> {
283 self.atomic_read_detect(clocks, index)?;
284 if let Some(atomic) = self.atomic() {
285 clocks.clock.join(&atomic.sync_vector);
290 /// Checks if the memory cell write races with any prior atomic read or write
291 fn write_race_free_with_atomic(&mut self, clocks: &ThreadClockSet) -> bool {
292 if let Some(atomic) = self.atomic() {
293 atomic.read_vector <= clocks.clock && atomic.write_vector <= clocks.clock
299 /// Checks if the memory cell read races with any prior atomic write
300 fn read_race_free_with_atomic(&self, clocks: &ThreadClockSet) -> bool {
301 if let Some(atomic) = self.atomic() { atomic.write_vector <= clocks.clock } else { true }
304 /// Update memory cell data-race tracking for atomic
305 /// load relaxed semantics, is a no-op if this memory was
306 /// not used previously as atomic memory.
309 clocks: &mut ThreadClockSet,
311 ) -> Result<(), DataRace> {
312 self.atomic_read_detect(clocks, index)?;
313 if let Some(atomic) = self.atomic() {
314 clocks.fence_acquire.join(&atomic.sync_vector);
319 /// Update the memory cell data-race tracking for atomic
320 /// store release semantics.
321 fn store_release(&mut self, clocks: &ThreadClockSet, index: VectorIdx) -> Result<(), DataRace> {
322 self.atomic_write_detect(clocks, index)?;
323 let atomic = self.atomic_mut();
324 atomic.sync_vector.clone_from(&clocks.clock);
328 /// Update the memory cell data-race tracking for atomic
329 /// store relaxed semantics.
330 fn store_relaxed(&mut self, clocks: &ThreadClockSet, index: VectorIdx) -> Result<(), DataRace> {
331 self.atomic_write_detect(clocks, index)?;
333 // The handling of release sequences was changed in C++20 and so
334 // the code here is different to the paper since now all relaxed
335 // stores block release sequences. The exception for same-thread
336 // relaxed stores has been removed.
337 let atomic = self.atomic_mut();
338 atomic.sync_vector.clone_from(&clocks.fence_release);
342 /// Update the memory cell data-race tracking for atomic
343 /// store release semantics for RMW operations.
344 fn rmw_release(&mut self, clocks: &ThreadClockSet, index: VectorIdx) -> Result<(), DataRace> {
345 self.atomic_write_detect(clocks, index)?;
346 let atomic = self.atomic_mut();
347 atomic.sync_vector.join(&clocks.clock);
351 /// Update the memory cell data-race tracking for atomic
352 /// store relaxed semantics for RMW operations.
353 fn rmw_relaxed(&mut self, clocks: &ThreadClockSet, index: VectorIdx) -> Result<(), DataRace> {
354 self.atomic_write_detect(clocks, index)?;
355 let atomic = self.atomic_mut();
356 atomic.sync_vector.join(&clocks.fence_release);
360 /// Detect data-races with an atomic read, caused by a non-atomic write that does
361 /// not happen-before the atomic-read.
362 fn atomic_read_detect(
364 clocks: &ThreadClockSet,
366 ) -> Result<(), DataRace> {
367 log::trace!("Atomic read with vectors: {:#?} :: {:#?}", self, clocks);
368 if self.write <= clocks.clock[self.write_index] {
369 let atomic = self.atomic_mut();
370 atomic.read_vector.set_at_index(&clocks.clock, index);
377 /// Detect data-races with an atomic write, either with a non-atomic read or with
378 /// a non-atomic write.
379 fn atomic_write_detect(
381 clocks: &ThreadClockSet,
383 ) -> Result<(), DataRace> {
384 log::trace!("Atomic write with vectors: {:#?} :: {:#?}", self, clocks);
385 if self.write <= clocks.clock[self.write_index] && self.read <= clocks.clock {
386 let atomic = self.atomic_mut();
387 atomic.write_vector.set_at_index(&clocks.clock, index);
394 /// Detect races for non-atomic read operations at the current memory cell
395 /// returns true if a data-race is detected.
398 clocks: &ThreadClockSet,
400 ) -> Result<(), DataRace> {
401 log::trace!("Unsynchronized read with vectors: {:#?} :: {:#?}", self, clocks);
402 if self.write <= clocks.clock[self.write_index] {
403 let race_free = if let Some(atomic) = self.atomic() {
404 atomic.write_vector <= clocks.clock
409 self.read.set_at_index(&clocks.clock, index);
419 /// Detect races for non-atomic write operations at the current memory cell
420 /// returns true if a data-race is detected.
421 fn write_race_detect(
423 clocks: &ThreadClockSet,
425 write_type: WriteType,
426 ) -> Result<(), DataRace> {
427 log::trace!("Unsynchronized write with vectors: {:#?} :: {:#?}", self, clocks);
428 if self.write <= clocks.clock[self.write_index] && self.read <= clocks.clock {
429 let race_free = if let Some(atomic) = self.atomic() {
430 atomic.write_vector <= clocks.clock && atomic.read_vector <= clocks.clock
435 self.write = clocks.clock[index];
436 self.write_index = index;
437 self.write_type = write_type;
438 self.read.set_zero_vector();
449 /// Evaluation context extensions.
450 impl<'mir, 'tcx: 'mir> EvalContextExt<'mir, 'tcx> for MiriEvalContext<'mir, 'tcx> {}
451 pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
452 /// Temporarily allow data-races to occur. This should only be used in
453 /// one of these cases:
454 /// - One of the appropriate `validate_atomic` functions will be called to
455 /// to treat a memory access as atomic.
456 /// - The memory being accessed should be treated as internal state, that
457 /// cannot be accessed by the interpreted program.
458 /// - Execution of the interpreted program execution has halted.
460 fn allow_data_races_ref<R>(&self, op: impl FnOnce(&MiriEvalContext<'mir, 'tcx>) -> R) -> R {
461 let this = self.eval_context_ref();
462 if let Some(data_race) = &this.machine.data_race {
463 data_race.ongoing_atomic_access.set(true);
465 let result = op(this);
466 if let Some(data_race) = &this.machine.data_race {
467 data_race.ongoing_atomic_access.set(false);
472 /// Same as `allow_data_races_ref`, this temporarily disables any data-race detection and
473 /// so should only be used for atomic operations or internal state that the program cannot
476 fn allow_data_races_mut<R>(
478 op: impl FnOnce(&mut MiriEvalContext<'mir, 'tcx>) -> R,
480 let this = self.eval_context_mut();
481 if let Some(data_race) = &this.machine.data_race {
482 data_race.ongoing_atomic_access.set(true);
484 let result = op(this);
485 if let Some(data_race) = &this.machine.data_race {
486 data_race.ongoing_atomic_access.set(false);
491 /// Atomic variant of read_scalar_at_offset.
492 fn read_scalar_at_offset_atomic(
494 op: &OpTy<'tcx, Tag>,
496 layout: TyAndLayout<'tcx>,
497 atomic: AtomicReadOp,
498 ) -> InterpResult<'tcx, ScalarMaybeUninit<Tag>> {
499 let this = self.eval_context_ref();
500 let value_place = this.deref_operand_and_offset(op, offset, layout)?;
501 this.read_scalar_atomic(&value_place, atomic)
504 /// Atomic variant of write_scalar_at_offset.
505 fn write_scalar_at_offset_atomic(
507 op: &OpTy<'tcx, Tag>,
509 value: impl Into<ScalarMaybeUninit<Tag>>,
510 layout: TyAndLayout<'tcx>,
511 atomic: AtomicWriteOp,
512 ) -> InterpResult<'tcx> {
513 let this = self.eval_context_mut();
514 let value_place = this.deref_operand_and_offset(op, offset, layout)?;
515 this.write_scalar_atomic(value.into(), &value_place, atomic)
518 /// Perform an atomic read operation at the memory location.
519 fn read_scalar_atomic(
521 place: &MPlaceTy<'tcx, Tag>,
522 atomic: AtomicReadOp,
523 ) -> InterpResult<'tcx, ScalarMaybeUninit<Tag>> {
524 let this = self.eval_context_ref();
525 // This will read from the last store in the modification order of this location. In case
526 // weak memory emulation is enabled, this may not be the store we will pick to actually read from and return.
527 // This is fine with StackedBorrow and race checks because they don't concern metadata on
528 // the *value* (including the associated provenance if this is an AtomicPtr) at this location.
529 // Only metadata on the location itself is used.
530 let scalar = this.allow_data_races_ref(move |this| this.read_scalar(&place.into()))?;
531 this.validate_overlapping_atomic_read(place)?;
532 this.buffered_atomic_read(place, atomic, scalar, || {
533 this.validate_atomic_load(place, atomic)
537 /// Perform an atomic write operation at the memory location.
538 fn write_scalar_atomic(
540 val: ScalarMaybeUninit<Tag>,
541 dest: &MPlaceTy<'tcx, Tag>,
542 atomic: AtomicWriteOp,
543 ) -> InterpResult<'tcx> {
544 let this = self.eval_context_mut();
545 this.validate_overlapping_atomic_write(dest)?;
546 this.allow_data_races_mut(move |this| this.write_scalar(val, &(*dest).into()))?;
547 this.validate_atomic_store(dest, atomic)?;
548 // FIXME: it's not possible to get the value before write_scalar. A read_scalar will cause
549 // side effects from a read the program did not perform. So we have to initialise
550 // the store buffer with the value currently being written
551 // ONCE this is fixed please remove the hack in buffered_atomic_write() in weak_memory.rs
552 this.buffered_atomic_write(val, dest, atomic, val)
555 /// Perform an atomic operation on a memory location.
556 fn atomic_op_immediate(
558 place: &MPlaceTy<'tcx, Tag>,
559 rhs: &ImmTy<'tcx, Tag>,
563 ) -> InterpResult<'tcx, ImmTy<'tcx, Tag>> {
564 let this = self.eval_context_mut();
566 this.validate_overlapping_atomic_write(place)?;
567 let old = this.allow_data_races_mut(|this| this.read_immediate(&place.into()))?;
569 // Atomics wrap around on overflow.
570 let val = this.binary_op(op, &old, rhs)?;
571 let val = if neg { this.unary_op(mir::UnOp::Not, &val)? } else { val };
572 this.allow_data_races_mut(|this| this.write_immediate(*val, &(*place).into()))?;
574 this.validate_atomic_rmw(place, atomic)?;
576 this.buffered_atomic_rmw(
577 val.to_scalar_or_uninit(),
580 old.to_scalar_or_uninit(),
585 /// Perform an atomic exchange with a memory place and a new
586 /// scalar value, the old value is returned.
587 fn atomic_exchange_scalar(
589 place: &MPlaceTy<'tcx, Tag>,
590 new: ScalarMaybeUninit<Tag>,
592 ) -> InterpResult<'tcx, ScalarMaybeUninit<Tag>> {
593 let this = self.eval_context_mut();
595 this.validate_overlapping_atomic_write(place)?;
596 let old = this.allow_data_races_mut(|this| this.read_scalar(&place.into()))?;
597 this.allow_data_races_mut(|this| this.write_scalar(new, &(*place).into()))?;
599 this.validate_atomic_rmw(place, atomic)?;
601 this.buffered_atomic_rmw(new, place, atomic, old)?;
605 /// Perform an conditional atomic exchange with a memory place and a new
606 /// scalar value, the old value is returned.
607 fn atomic_min_max_scalar(
609 place: &MPlaceTy<'tcx, Tag>,
610 rhs: ImmTy<'tcx, Tag>,
613 ) -> InterpResult<'tcx, ImmTy<'tcx, Tag>> {
614 let this = self.eval_context_mut();
616 this.validate_overlapping_atomic_write(place)?;
617 let old = this.allow_data_races_mut(|this| this.read_immediate(&place.into()))?;
618 let lt = this.binary_op(mir::BinOp::Lt, &old, &rhs)?.to_scalar()?.to_bool()?;
620 let new_val = if min {
621 if lt { &old } else { &rhs }
623 if lt { &rhs } else { &old }
626 this.allow_data_races_mut(|this| this.write_immediate(**new_val, &(*place).into()))?;
628 this.validate_atomic_rmw(place, atomic)?;
630 this.buffered_atomic_rmw(
631 new_val.to_scalar_or_uninit(),
634 old.to_scalar_or_uninit(),
637 // Return the old value.
641 /// Perform an atomic compare and exchange at a given memory location.
642 /// On success an atomic RMW operation is performed and on failure
643 /// only an atomic read occurs. If `can_fail_spuriously` is true,
644 /// then we treat it as a "compare_exchange_weak" operation, and
645 /// some portion of the time fail even when the values are actually
647 fn atomic_compare_exchange_scalar(
649 place: &MPlaceTy<'tcx, Tag>,
650 expect_old: &ImmTy<'tcx, Tag>,
651 new: ScalarMaybeUninit<Tag>,
654 can_fail_spuriously: bool,
655 ) -> InterpResult<'tcx, Immediate<Tag>> {
657 let this = self.eval_context_mut();
659 this.validate_overlapping_atomic_write(place)?;
660 // Failure ordering cannot be stronger than success ordering, therefore first attempt
661 // to read with the failure ordering and if successful then try again with the success
662 // read ordering and write in the success case.
663 // Read as immediate for the sake of `binary_op()`
664 let old = this.allow_data_races_mut(|this| this.read_immediate(&(place.into())))?;
665 // `binary_op` will bail if either of them is not a scalar.
666 let eq = this.binary_op(mir::BinOp::Eq, &old, expect_old)?;
667 // If the operation would succeed, but is "weak", fail some portion
668 // of the time, based on `success_rate`.
669 let success_rate = 1.0 - this.machine.cmpxchg_weak_failure_rate;
670 let cmpxchg_success = eq.to_scalar()?.to_bool()?
671 && if can_fail_spuriously {
672 this.machine.rng.get_mut().gen_bool(success_rate)
676 let res = Immediate::ScalarPair(
677 old.to_scalar_or_uninit(),
678 Scalar::from_bool(cmpxchg_success).into(),
681 // Update ptr depending on comparison.
682 // if successful, perform a full rw-atomic validation
683 // otherwise treat this as an atomic load with the fail ordering.
685 this.allow_data_races_mut(|this| this.write_scalar(new, &(*place).into()))?;
686 this.validate_atomic_rmw(place, success)?;
687 this.buffered_atomic_rmw(new, place, success, old.to_scalar_or_uninit())?;
689 this.validate_atomic_load(place, fail)?;
690 // A failed compare exchange is equivalent to a load, reading from the latest store
691 // in the modification order.
692 // Since `old` is only a value and not the store element, we need to separately
693 // find it in our store buffer and perform load_impl on it.
694 this.perform_read_on_buffered_latest(place, fail, old.to_scalar_or_uninit())?;
697 // Return the old value.
701 /// Update the data-race detector for an atomic read occurring at the
702 /// associated memory-place and on the current thread.
703 fn validate_atomic_load(
705 place: &MPlaceTy<'tcx, Tag>,
706 atomic: AtomicReadOp,
707 ) -> InterpResult<'tcx> {
708 let this = self.eval_context_ref();
709 this.validate_overlapping_atomic_read(place)?;
710 this.validate_atomic_op(
714 move |memory, clocks, index, atomic| {
715 if atomic == AtomicReadOp::Relaxed {
716 memory.load_relaxed(&mut *clocks, index)
718 memory.load_acquire(&mut *clocks, index)
724 /// Update the data-race detector for an atomic write occurring at the
725 /// associated memory-place and on the current thread.
726 fn validate_atomic_store(
728 place: &MPlaceTy<'tcx, Tag>,
729 atomic: AtomicWriteOp,
730 ) -> InterpResult<'tcx> {
731 let this = self.eval_context_mut();
732 this.validate_overlapping_atomic_write(place)?;
733 this.validate_atomic_op(
737 move |memory, clocks, index, atomic| {
738 if atomic == AtomicWriteOp::Relaxed {
739 memory.store_relaxed(clocks, index)
741 memory.store_release(clocks, index)
747 /// Update the data-race detector for an atomic read-modify-write occurring
748 /// at the associated memory place and on the current thread.
749 fn validate_atomic_rmw(
751 place: &MPlaceTy<'tcx, Tag>,
753 ) -> InterpResult<'tcx> {
755 let acquire = matches!(atomic, Acquire | AcqRel | SeqCst);
756 let release = matches!(atomic, Release | AcqRel | SeqCst);
757 let this = self.eval_context_mut();
758 this.validate_overlapping_atomic_write(place)?;
759 this.validate_atomic_op(place, atomic, "Atomic RMW", move |memory, clocks, index, _| {
761 memory.load_acquire(clocks, index)?;
763 memory.load_relaxed(clocks, index)?;
766 memory.rmw_release(clocks, index)
768 memory.rmw_relaxed(clocks, index)
773 /// Update the data-race detector for an atomic fence on the current thread.
774 fn validate_atomic_fence(&mut self, atomic: AtomicFenceOp) -> InterpResult<'tcx> {
775 let this = self.eval_context_mut();
776 if let Some(data_race) = &mut this.machine.data_race {
777 data_race.maybe_perform_sync_operation(|index, mut clocks| {
778 log::trace!("Atomic fence on {:?} with ordering {:?}", index, atomic);
780 // Apply data-race detection for the current fences
781 // this treats AcqRel and SeqCst as the same as an acquire
782 // and release fence applied in the same timestamp.
783 if atomic != AtomicFenceOp::Release {
784 // Either Acquire | AcqRel | SeqCst
785 clocks.apply_acquire_fence();
787 if atomic != AtomicFenceOp::Acquire {
788 // Either Release | AcqRel | SeqCst
789 clocks.apply_release_fence();
791 if atomic == AtomicFenceOp::SeqCst {
792 data_race.last_sc_fence.borrow_mut().set_at_index(&clocks.clock, index);
793 clocks.fence_seqcst.join(&data_race.last_sc_fence.borrow());
794 clocks.write_seqcst.join(&data_race.last_sc_write.borrow());
797 // Increment timestamp in case of release semantics.
798 Ok(atomic != AtomicFenceOp::Acquire)
806 /// Vector clock metadata for a logical memory allocation.
807 #[derive(Debug, Clone)]
808 pub struct VClockAlloc {
809 /// Assigning each byte a MemoryCellClocks.
810 alloc_ranges: RefCell<RangeMap<MemoryCellClocks>>,
814 /// Create a new data-race detector for newly allocated memory.
815 pub fn new_allocation(
816 global: &GlobalState,
818 kind: MemoryKind<MiriMemoryKind>,
820 let (alloc_timestamp, alloc_index) = match kind {
821 // User allocated and stack memory should track allocation.
823 MiriMemoryKind::Rust | MiriMemoryKind::C | MiriMemoryKind::WinHeap,
825 | MemoryKind::Stack => {
826 let (alloc_index, clocks) = global.current_thread_state();
827 let alloc_timestamp = clocks.clock[alloc_index];
828 (alloc_timestamp, alloc_index)
830 // Other global memory should trace races but be allocated at the 0 timestamp.
832 MiriMemoryKind::Global
833 | MiriMemoryKind::Machine
834 | MiriMemoryKind::Runtime
835 | MiriMemoryKind::ExternStatic
836 | MiriMemoryKind::Tls,
838 | MemoryKind::CallerLocation => (0, VectorIdx::MAX_INDEX),
841 alloc_ranges: RefCell::new(RangeMap::new(
843 MemoryCellClocks::new(alloc_timestamp, alloc_index),
848 // Find an index, if one exists where the value
849 // in `l` is greater than the value in `r`.
850 fn find_gt_index(l: &VClock, r: &VClock) -> Option<VectorIdx> {
851 log::trace!("Find index where not {:?} <= {:?}", l, r);
852 let l_slice = l.as_slice();
853 let r_slice = r.as_slice();
858 .find_map(|(idx, (&l, &r))| if l > r { Some(idx) } else { None })
860 if l_slice.len() > r_slice.len() {
861 // By invariant, if l_slice is longer
862 // then one element must be larger.
863 // This just validates that this is true
864 // and reports earlier elements first.
865 let l_remainder_slice = &l_slice[r_slice.len()..];
866 let idx = l_remainder_slice
869 .find_map(|(idx, &r)| if r == 0 { None } else { Some(idx) })
870 .expect("Invalid VClock Invariant");
871 Some(idx + r_slice.len())
879 /// Report a data-race found in the program.
880 /// This finds the two racing threads and the type
881 /// of data-race that occurred. This will also
882 /// return info about the memory location the data-race
886 fn report_data_race<'tcx>(
887 global: &GlobalState,
888 range: &MemoryCellClocks,
891 ptr_dbg: Pointer<AllocId>,
892 ) -> InterpResult<'tcx> {
893 let (current_index, current_clocks) = global.current_thread_state();
895 let (other_action, other_thread, other_clock) = if range.write
896 > current_clocks.clock[range.write_index]
898 // Convert the write action into the vector clock it
899 // represents for diagnostic purposes.
900 write_clock = VClock::new_with_index(range.write_index, range.write);
901 (range.write_type.get_descriptor(), range.write_index, &write_clock)
902 } else if let Some(idx) = Self::find_gt_index(&range.read, ¤t_clocks.clock) {
903 ("Read", idx, &range.read)
904 } else if !is_atomic {
905 if let Some(atomic) = range.atomic() {
906 if let Some(idx) = Self::find_gt_index(&atomic.write_vector, ¤t_clocks.clock)
908 ("Atomic Store", idx, &atomic.write_vector)
909 } else if let Some(idx) =
910 Self::find_gt_index(&atomic.read_vector, ¤t_clocks.clock)
912 ("Atomic Load", idx, &atomic.read_vector)
915 "Failed to report data-race for non-atomic operation: no race found"
920 "Failed to report data-race for non-atomic operation: no atomic component"
924 unreachable!("Failed to report data-race for atomic operation")
927 // Load elaborated thread information about the racing thread actions.
928 let current_thread_info = global.print_thread_metadata(current_index);
929 let other_thread_info = global.print_thread_metadata(other_thread);
931 // Throw the data-race detection.
933 "Data race detected between {} on {} and {} on {} at {:?} (current vector clock = {:?}, conflicting timestamp = {:?})",
939 current_clocks.clock,
944 /// Detect racing atomic writes (not data races)
945 /// on every byte of the current access range
946 pub(super) fn read_race_free_with_atomic<'tcx>(
949 global: &GlobalState,
951 if global.race_detecting() {
952 let (_, clocks) = global.current_thread_state();
953 let alloc_ranges = self.alloc_ranges.borrow();
954 for (_, range) in alloc_ranges.iter(range.start, range.size) {
955 if !range.read_race_free_with_atomic(&clocks) {
963 /// Detect racing atomic read and writes (not data races)
964 /// on every byte of the current access range
965 pub(super) fn write_race_free_with_atomic<'tcx>(
968 global: &GlobalState,
970 if global.race_detecting() {
971 let (_, clocks) = global.current_thread_state();
972 let alloc_ranges = self.alloc_ranges.get_mut();
973 for (_, range) in alloc_ranges.iter_mut(range.start, range.size) {
974 if !range.write_race_free_with_atomic(&clocks) {
982 /// Detect data-races for an unsynchronized read operation, will not perform
983 /// data-race detection if `race_detecting()` is false, either due to no threads
984 /// being created or if it is temporarily disabled during a racy read or write
985 /// operation for which data-race detection is handled separately, for example
986 /// atomic read operations.
991 global: &GlobalState,
992 ) -> InterpResult<'tcx> {
993 if global.race_detecting() {
994 let (index, clocks) = global.current_thread_state();
995 let mut alloc_ranges = self.alloc_ranges.borrow_mut();
996 for (offset, range) in alloc_ranges.iter_mut(range.start, range.size) {
997 if let Err(DataRace) = range.read_race_detect(&*clocks, index) {
999 return Self::report_data_race(
1004 Pointer::new(alloc_id, offset),
1014 // Shared code for detecting data-races on unique access to a section of memory
1015 fn unique_access<'tcx>(
1019 write_type: WriteType,
1020 global: &mut GlobalState,
1021 ) -> InterpResult<'tcx> {
1022 if global.race_detecting() {
1023 let (index, clocks) = global.current_thread_state();
1024 for (offset, range) in self.alloc_ranges.get_mut().iter_mut(range.start, range.size) {
1025 if let Err(DataRace) = range.write_race_detect(&*clocks, index, write_type) {
1027 return Self::report_data_race(
1030 write_type.get_descriptor(),
1032 Pointer::new(alloc_id, offset),
1042 /// Detect data-races for an unsynchronized write operation, will not perform
1043 /// data-race threads if `race_detecting()` is false, either due to no threads
1044 /// being created or if it is temporarily disabled during a racy read or write
1050 global: &mut GlobalState,
1051 ) -> InterpResult<'tcx> {
1052 self.unique_access(alloc_id, range, WriteType::Write, global)
1055 /// Detect data-races for an unsynchronized deallocate operation, will not perform
1056 /// data-race threads if `race_detecting()` is false, either due to no threads
1057 /// being created or if it is temporarily disabled during a racy read or write
1059 pub fn deallocate<'tcx>(
1063 global: &mut GlobalState,
1064 ) -> InterpResult<'tcx> {
1065 self.unique_access(alloc_id, range, WriteType::Deallocate, global)
1069 impl<'mir, 'tcx: 'mir> EvalContextPrivExt<'mir, 'tcx> for MiriEvalContext<'mir, 'tcx> {}
1070 trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
1071 /// Generic atomic operation implementation
1072 fn validate_atomic_op<A: Debug + Copy>(
1074 place: &MPlaceTy<'tcx, Tag>,
1078 &mut MemoryCellClocks,
1079 &mut ThreadClockSet,
1082 ) -> Result<(), DataRace>,
1083 ) -> InterpResult<'tcx> {
1084 let this = self.eval_context_ref();
1085 if let Some(data_race) = &this.machine.data_race {
1086 if data_race.race_detecting() {
1087 let size = place.layout.size;
1088 let (alloc_id, base_offset, _tag) = this.ptr_get_alloc_id(place.ptr)?;
1089 // Load and log the atomic operation.
1090 // Note that atomic loads are possible even from read-only allocations, so `get_alloc_extra_mut` is not an option.
1091 let alloc_meta = this.get_alloc_extra(alloc_id)?.data_race.as_ref().unwrap();
1093 "Atomic op({}) with ordering {:?} on {:?} (size={})",
1100 // Perform the atomic operation.
1101 data_race.maybe_perform_sync_operation(|index, mut clocks| {
1102 for (offset, range) in
1103 alloc_meta.alloc_ranges.borrow_mut().iter_mut(base_offset, size)
1105 if let Err(DataRace) = op(range, &mut *clocks, index, atomic) {
1107 return VClockAlloc::report_data_race(
1112 Pointer::new(alloc_id, offset),
1118 // This conservatively assumes all operations have release semantics
1122 // Log changes to atomic memory.
1123 if log::log_enabled!(log::Level::Trace) {
1124 for (_offset, range) in alloc_meta.alloc_ranges.borrow().iter(base_offset, size)
1127 "Updated atomic memory({:?}, size={}) to {:#?}",
1140 /// Extra metadata associated with a thread.
1141 #[derive(Debug, Clone, Default)]
1142 struct ThreadExtraState {
1143 /// The current vector index in use by the
1144 /// thread currently, this is set to None
1145 /// after the vector index has been re-used
1146 /// and hence the value will never need to be
1147 /// read during data-race reporting.
1148 vector_index: Option<VectorIdx>,
1150 /// The name of the thread, updated for better
1151 /// diagnostics when reporting detected data
1153 thread_name: Option<Box<str>>,
1155 /// Thread termination vector clock, this
1156 /// is set on thread termination and is used
1157 /// for joining on threads since the vector_index
1158 /// may be re-used when the join operation occurs.
1159 termination_vector_clock: Option<VClock>,
1162 /// Global data-race detection state, contains the currently
1163 /// executing thread as well as the vector-clocks associated
1164 /// with each of the threads.
1165 // FIXME: it is probably better to have one large RefCell, than to have so many small ones.
1166 #[derive(Debug, Clone)]
1167 pub struct GlobalState {
1168 /// Set to true once the first additional
1169 /// thread has launched, due to the dependency
1170 /// between before and after a thread launch.
1171 /// Any data-races must be recorded after this
1172 /// so concurrent execution can ignore recording
1174 multi_threaded: Cell<bool>,
1176 /// A flag to mark we are currently performing
1177 /// an atomic access to supress data race detection
1178 ongoing_atomic_access: Cell<bool>,
1180 /// Mapping of a vector index to a known set of thread
1181 /// clocks, this is not directly mapping from a thread id
1182 /// since it may refer to multiple threads.
1183 vector_clocks: RefCell<IndexVec<VectorIdx, ThreadClockSet>>,
1185 /// Mapping of a given vector index to the current thread
1186 /// that the execution is representing, this may change
1187 /// if a vector index is re-assigned to a new thread.
1188 vector_info: RefCell<IndexVec<VectorIdx, ThreadId>>,
1190 /// The mapping of a given thread to associated thread metadata.
1191 thread_info: RefCell<IndexVec<ThreadId, ThreadExtraState>>,
1193 /// The current vector index being executed.
1194 current_index: Cell<VectorIdx>,
1196 /// Potential vector indices that could be re-used on thread creation
1197 /// values are inserted here on after the thread has terminated and
1198 /// been joined with, and hence may potentially become free
1199 /// for use as the index for a new thread.
1200 /// Elements in this set may still require the vector index to
1201 /// report data-races, and can only be re-used after all
1202 /// active vector-clocks catch up with the threads timestamp.
1203 reuse_candidates: RefCell<FxHashSet<VectorIdx>>,
1205 /// Counts the number of threads that are currently active
1206 /// if the number of active threads reduces to 1 and then
1207 /// a join operation occurs with the remaining main thread
1208 /// then multi-threaded execution may be disabled.
1209 active_thread_count: Cell<usize>,
1211 /// This contains threads that have terminated, but not yet joined
1212 /// and so cannot become re-use candidates until a join operation
1214 /// The associated vector index will be moved into re-use candidates
1215 /// after the join operation occurs.
1216 terminated_threads: RefCell<FxHashMap<ThreadId, VectorIdx>>,
1218 /// The timestamp of last SC fence performed by each thread
1219 last_sc_fence: RefCell<VClock>,
1221 /// The timestamp of last SC write performed by each thread
1222 last_sc_write: RefCell<VClock>,
1226 /// Create a new global state, setup with just thread-id=0
1227 /// advanced to timestamp = 1.
1228 pub fn new() -> Self {
1229 let mut global_state = GlobalState {
1230 multi_threaded: Cell::new(false),
1231 ongoing_atomic_access: Cell::new(false),
1232 vector_clocks: RefCell::new(IndexVec::new()),
1233 vector_info: RefCell::new(IndexVec::new()),
1234 thread_info: RefCell::new(IndexVec::new()),
1235 current_index: Cell::new(VectorIdx::new(0)),
1236 active_thread_count: Cell::new(1),
1237 reuse_candidates: RefCell::new(FxHashSet::default()),
1238 terminated_threads: RefCell::new(FxHashMap::default()),
1239 last_sc_fence: RefCell::new(VClock::default()),
1240 last_sc_write: RefCell::new(VClock::default()),
1243 // Setup the main-thread since it is not explicitly created:
1244 // uses vector index and thread-id 0, also the rust runtime gives
1245 // the main-thread a name of "main".
1246 let index = global_state.vector_clocks.get_mut().push(ThreadClockSet::default());
1247 global_state.vector_info.get_mut().push(ThreadId::new(0));
1248 global_state.thread_info.get_mut().push(ThreadExtraState {
1249 vector_index: Some(index),
1250 thread_name: Some("main".to_string().into_boxed_str()),
1251 termination_vector_clock: None,
1257 // We perform data race detection when there are more than 1 active thread
1258 // and we are not currently in the middle of an atomic acces where data race
1260 fn race_detecting(&self) -> bool {
1261 self.multi_threaded.get() && !self.ongoing_atomic_access.get()
1264 pub fn ongoing_atomic_access(&self) -> bool {
1265 self.ongoing_atomic_access.get()
1268 // Try to find vector index values that can potentially be re-used
1269 // by a new thread instead of a new vector index being created.
1270 fn find_vector_index_reuse_candidate(&self) -> Option<VectorIdx> {
1271 let mut reuse = self.reuse_candidates.borrow_mut();
1272 let vector_clocks = self.vector_clocks.borrow();
1273 let vector_info = self.vector_info.borrow();
1274 let terminated_threads = self.terminated_threads.borrow();
1275 for &candidate in reuse.iter() {
1276 let target_timestamp = vector_clocks[candidate].clock[candidate];
1277 if vector_clocks.iter_enumerated().all(|(clock_idx, clock)| {
1278 // The thread happens before the clock, and hence cannot report
1279 // a data-race with this the candidate index.
1280 let no_data_race = clock.clock[candidate] >= target_timestamp;
1282 // The vector represents a thread that has terminated and hence cannot
1283 // report a data-race with the candidate index.
1284 let thread_id = vector_info[clock_idx];
1285 let vector_terminated =
1286 reuse.contains(&clock_idx) || terminated_threads.contains_key(&thread_id);
1288 // The vector index cannot report a race with the candidate index
1289 // and hence allows the candidate index to be re-used.
1290 no_data_race || vector_terminated
1292 // All vector clocks for each vector index are equal to
1293 // the target timestamp, and the thread is known to have
1294 // terminated, therefore this vector clock index cannot
1295 // report any more data-races.
1296 assert!(reuse.remove(&candidate));
1297 return Some(candidate);
1303 // Hook for thread creation, enabled multi-threaded execution and marks
1304 // the current thread timestamp as happening-before the current thread.
1306 pub fn thread_created(&mut self, thread: ThreadId) {
1307 let current_index = self.current_index();
1309 // Increment the number of active threads.
1310 let active_threads = self.active_thread_count.get();
1311 self.active_thread_count.set(active_threads + 1);
1313 // Enable multi-threaded execution, there are now two threads
1314 // so data-races are now possible.
1315 self.multi_threaded.set(true);
1317 // Load and setup the associated thread metadata
1318 let mut thread_info = self.thread_info.borrow_mut();
1319 thread_info.ensure_contains_elem(thread, Default::default);
1321 // Assign a vector index for the thread, attempting to re-use an old
1322 // vector index that can no longer report any data-races if possible.
1323 let created_index = if let Some(reuse_index) = self.find_vector_index_reuse_candidate() {
1324 // Now re-configure the re-use candidate, increment the clock
1325 // for the new sync use of the vector.
1326 let vector_clocks = self.vector_clocks.get_mut();
1327 vector_clocks[reuse_index].increment_clock(reuse_index);
1329 // Locate the old thread the vector was associated with and update
1330 // it to represent the new thread instead.
1331 let vector_info = self.vector_info.get_mut();
1332 let old_thread = vector_info[reuse_index];
1333 vector_info[reuse_index] = thread;
1335 // Mark the thread the vector index was associated with as no longer
1336 // representing a thread index.
1337 thread_info[old_thread].vector_index = None;
1341 // No vector re-use candidates available, instead create
1342 // a new vector index.
1343 let vector_info = self.vector_info.get_mut();
1344 vector_info.push(thread)
1347 log::trace!("Creating thread = {:?} with vector index = {:?}", thread, created_index);
1349 // Mark the chosen vector index as in use by the thread.
1350 thread_info[thread].vector_index = Some(created_index);
1352 // Create a thread clock set if applicable.
1353 let vector_clocks = self.vector_clocks.get_mut();
1354 if created_index == vector_clocks.next_index() {
1355 vector_clocks.push(ThreadClockSet::default());
1358 // Now load the two clocks and configure the initial state.
1359 let (current, created) = vector_clocks.pick2_mut(current_index, created_index);
1361 // Join the created with current, since the current threads
1362 // previous actions happen-before the created thread.
1363 created.join_with(current);
1365 // Advance both threads after the synchronized operation.
1366 // Both operations are considered to have release semantics.
1367 current.increment_clock(current_index);
1368 created.increment_clock(created_index);
1371 /// Hook on a thread join to update the implicit happens-before relation
1372 /// between the joined thread and the current thread.
1374 pub fn thread_joined(&mut self, current_thread: ThreadId, join_thread: ThreadId) {
1375 let clocks_vec = self.vector_clocks.get_mut();
1376 let thread_info = self.thread_info.get_mut();
1378 // Load the vector clock of the current thread.
1379 let current_index = thread_info[current_thread]
1381 .expect("Performed thread join on thread with no assigned vector");
1382 let current = &mut clocks_vec[current_index];
1384 // Load the associated vector clock for the terminated thread.
1385 let join_clock = thread_info[join_thread]
1386 .termination_vector_clock
1388 .expect("Joined with thread but thread has not terminated");
1390 // The join thread happens-before the current thread
1391 // so update the current vector clock.
1392 // Is not a release operation so the clock is not incremented.
1393 current.clock.join(join_clock);
1395 // Check the number of active threads, if the value is 1
1396 // then test for potentially disabling multi-threaded execution.
1397 let active_threads = self.active_thread_count.get();
1398 if active_threads == 1 {
1399 // May potentially be able to disable multi-threaded execution.
1400 let current_clock = &clocks_vec[current_index];
1403 .all(|(idx, clocks)| clocks.clock[idx] <= current_clock.clock[idx])
1405 // All thread terminations happen-before the current clock
1406 // therefore no data-races can be reported until a new thread
1407 // is created, so disable multi-threaded execution.
1408 self.multi_threaded.set(false);
1412 // If the thread is marked as terminated but not joined
1413 // then move the thread to the re-use set.
1414 let termination = self.terminated_threads.get_mut();
1415 if let Some(index) = termination.remove(&join_thread) {
1416 let reuse = self.reuse_candidates.get_mut();
1417 reuse.insert(index);
1421 /// On thread termination, the vector-clock may re-used
1422 /// in the future once all remaining thread-clocks catch
1423 /// up with the time index of the terminated thread.
1424 /// This assigns thread termination with a unique index
1425 /// which will be used to join the thread
1426 /// This should be called strictly before any calls to
1427 /// `thread_joined`.
1429 pub fn thread_terminated(&mut self) {
1430 let current_index = self.current_index();
1432 // Increment the clock to a unique termination timestamp.
1433 let vector_clocks = self.vector_clocks.get_mut();
1434 let current_clocks = &mut vector_clocks[current_index];
1435 current_clocks.increment_clock(current_index);
1437 // Load the current thread id for the executing vector.
1438 let vector_info = self.vector_info.get_mut();
1439 let current_thread = vector_info[current_index];
1441 // Load the current thread metadata, and move to a terminated
1442 // vector state. Setting up the vector clock all join operations
1444 let thread_info = self.thread_info.get_mut();
1445 let current = &mut thread_info[current_thread];
1446 current.termination_vector_clock = Some(current_clocks.clock.clone());
1448 // Add this thread as a candidate for re-use after a thread join
1450 let termination = self.terminated_threads.get_mut();
1451 termination.insert(current_thread, current_index);
1453 // Reduce the number of active threads, now that a thread has
1455 let mut active_threads = self.active_thread_count.get();
1456 active_threads -= 1;
1457 self.active_thread_count.set(active_threads);
1460 /// Hook for updating the local tracker of the currently
1461 /// enabled thread, should always be updated whenever
1462 /// `active_thread` in thread.rs is updated.
1464 pub fn thread_set_active(&self, thread: ThreadId) {
1465 let thread_info = self.thread_info.borrow();
1466 let vector_idx = thread_info[thread]
1468 .expect("Setting thread active with no assigned vector");
1469 self.current_index.set(vector_idx);
1472 /// Hook for updating the local tracker of the threads name
1473 /// this should always mirror the local value in thread.rs
1474 /// the thread name is used for improved diagnostics
1475 /// during a data-race.
1477 pub fn thread_set_name(&mut self, thread: ThreadId, name: String) {
1478 let name = name.into_boxed_str();
1479 let thread_info = self.thread_info.get_mut();
1480 thread_info[thread].thread_name = Some(name);
1483 /// Attempt to perform a synchronized operation, this
1484 /// will perform no operation if multi-threading is
1485 /// not currently enabled.
1486 /// Otherwise it will increment the clock for the current
1487 /// vector before and after the operation for data-race
1488 /// detection between any happens-before edges the
1489 /// operation may create.
1490 fn maybe_perform_sync_operation<'tcx>(
1492 op: impl FnOnce(VectorIdx, RefMut<'_, ThreadClockSet>) -> InterpResult<'tcx, bool>,
1493 ) -> InterpResult<'tcx> {
1494 if self.multi_threaded.get() {
1495 let (index, clocks) = self.current_thread_state_mut();
1496 if op(index, clocks)? {
1497 let (_, mut clocks) = self.current_thread_state_mut();
1498 clocks.increment_clock(index);
1504 /// Internal utility to identify a thread stored internally
1505 /// returns the id and the name for better diagnostics.
1506 fn print_thread_metadata(&self, vector: VectorIdx) -> String {
1507 let thread = self.vector_info.borrow()[vector];
1508 let thread_name = &self.thread_info.borrow()[thread].thread_name;
1509 if let Some(name) = thread_name {
1510 let name: &str = name;
1511 format!("Thread(id = {:?}, name = {:?})", thread.to_u32(), &*name)
1513 format!("Thread(id = {:?})", thread.to_u32())
1517 /// Acquire a lock, express that the previous call of
1518 /// `validate_lock_release` must happen before this.
1519 /// As this is an acquire operation, the thread timestamp is not
1521 pub fn validate_lock_acquire(&self, lock: &VClock, thread: ThreadId) {
1522 let (_, mut clocks) = self.load_thread_state_mut(thread);
1523 clocks.clock.join(lock);
1526 /// Release a lock handle, express that this happens-before
1527 /// any subsequent calls to `validate_lock_acquire`.
1528 /// For normal locks this should be equivalent to `validate_lock_release_shared`
1529 /// since an acquire operation should have occurred before, however
1530 /// for futex & condvar operations this is not the case and this
1531 /// operation must be used.
1532 pub fn validate_lock_release(&self, lock: &mut VClock, thread: ThreadId) {
1533 let (index, mut clocks) = self.load_thread_state_mut(thread);
1534 lock.clone_from(&clocks.clock);
1535 clocks.increment_clock(index);
1538 /// Release a lock handle, express that this happens-before
1539 /// any subsequent calls to `validate_lock_acquire` as well
1540 /// as any previous calls to this function after any
1541 /// `validate_lock_release` calls.
1542 /// For normal locks this should be equivalent to `validate_lock_release`.
1543 /// This function only exists for joining over the set of concurrent readers
1544 /// in a read-write lock and should not be used for anything else.
1545 pub fn validate_lock_release_shared(&self, lock: &mut VClock, thread: ThreadId) {
1546 let (index, mut clocks) = self.load_thread_state_mut(thread);
1547 lock.join(&clocks.clock);
1548 clocks.increment_clock(index);
1551 /// Load the vector index used by the given thread as well as the set of vector clocks
1552 /// used by the thread.
1554 fn load_thread_state_mut(&self, thread: ThreadId) -> (VectorIdx, RefMut<'_, ThreadClockSet>) {
1555 let index = self.thread_info.borrow()[thread]
1557 .expect("Loading thread state for thread with no assigned vector");
1558 let ref_vector = self.vector_clocks.borrow_mut();
1559 let clocks = RefMut::map(ref_vector, |vec| &mut vec[index]);
1563 /// Load the current vector clock in use and the current set of thread clocks
1564 /// in use for the vector.
1566 pub(super) fn current_thread_state(&self) -> (VectorIdx, Ref<'_, ThreadClockSet>) {
1567 let index = self.current_index();
1568 let ref_vector = self.vector_clocks.borrow();
1569 let clocks = Ref::map(ref_vector, |vec| &vec[index]);
1573 /// Load the current vector clock in use and the current set of thread clocks
1574 /// in use for the vector mutably for modification.
1576 pub(super) fn current_thread_state_mut(&self) -> (VectorIdx, RefMut<'_, ThreadClockSet>) {
1577 let index = self.current_index();
1578 let ref_vector = self.vector_clocks.borrow_mut();
1579 let clocks = RefMut::map(ref_vector, |vec| &mut vec[index]);
1583 /// Return the current thread, should be the same
1584 /// as the data-race active thread.
1586 fn current_index(&self) -> VectorIdx {
1587 self.current_index.get()
1590 // SC ATOMIC STORE rule in the paper.
1591 pub(super) fn sc_write(&self) {
1592 let (index, clocks) = self.current_thread_state();
1593 self.last_sc_write.borrow_mut().set_at_index(&clocks.clock, index);
1596 // SC ATOMIC READ rule in the paper.
1597 pub(super) fn sc_read(&self) {
1598 let (.., mut clocks) = self.current_thread_state_mut();
1599 clocks.read_seqcst.join(&self.last_sc_fence.borrow());