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 //! This does not explore weak memory orders and so 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 sequentially consistent ordering corresponds to the ordering that the threads
33 //! are currently scheduled, this means that the data-race detector has no additional
34 //! logic for sequentially consistent accesses at the moment since they are indistinguishable
35 //! from acquire/release operations. If weak memory orderings are explored then this
36 //! may need to change or be updated accordingly.
38 //! Per the C++ spec for the memory model a sequentially consistent operation:
39 //! "A load operation with this memory order performs an acquire operation,
40 //! a store performs a release operation, and read-modify-write performs
41 //! both an acquire operation and a release operation, plus a single total
42 //! order exists in which all threads observe all modifications in the same
43 //! order (see Sequentially-consistent ordering below) "
44 //! So in the absence of weak memory effects a seq-cst load & a seq-cst store is identical
45 //! to a acquire load and a release store given the global sequentially consistent order
48 //! The timestamps used in the data-race detector assign each sequence of non-atomic operations
49 //! followed by a single atomic or concurrent operation a single timestamp.
50 //! Write, Read, Write, ThreadJoin will be represented by a single timestamp value on a thread.
51 //! This is because extra increment operations between the operations in the sequence are not
52 //! required for accurate reporting of data-race values.
54 //! As per the paper a threads timestamp is only incremented after a release operation is performed
55 //! so some atomic operations that only perform acquires do not increment the timestamp. Due to shared
56 //! code some atomic operations may increment the timestamp when not necessary but this has no effect
57 //! on the data-race detection code.
60 //! currently we have our own local copy of the currently active thread index and names, this is due
61 //! in part to the inability to access the current location of threads.active_thread inside the AllocExtra
62 //! read, write and deallocate functions and should be cleaned up in the future.
65 cell::{Cell, Ref, RefCell, RefMut},
70 use rustc_data_structures::fx::{FxHashMap, FxHashSet};
71 use rustc_index::vec::{Idx, IndexVec};
72 use rustc_middle::{mir, ty::layout::TyAndLayout};
73 use rustc_target::abi::Size;
76 ImmTy, Immediate, InterpResult, MPlaceTy, MemPlaceMeta, MemoryKind, MiriEvalContext,
77 MiriEvalContextExt, MiriMemoryKind, OpTy, Pointer, RangeMap, Scalar, ScalarMaybeUninit, Tag,
78 ThreadId, VClock, VTimestamp, VectorIdx,
81 pub type AllocExtra = VClockAlloc;
82 pub type MemoryExtra = GlobalState;
84 /// Valid atomic read-write operations, alias of atomic::Ordering (not non-exhaustive).
85 #[derive(Copy, Clone, PartialEq, Eq, Debug)]
94 /// Valid atomic read operations, subset of atomic::Ordering.
95 #[derive(Copy, Clone, PartialEq, Eq, Debug)]
96 pub enum AtomicReadOp {
102 /// Valid atomic write operations, subset of atomic::Ordering.
103 #[derive(Copy, Clone, PartialEq, Eq, Debug)]
104 pub enum AtomicWriteOp {
110 /// Valid atomic fence operations, subset of atomic::Ordering.
111 #[derive(Copy, Clone, PartialEq, Eq, Debug)]
112 pub enum AtomicFenceOp {
119 /// The current set of vector clocks describing the state
120 /// of a thread, contains the happens-before clock and
121 /// additional metadata to model atomic fence operations.
122 #[derive(Clone, Default, Debug)]
123 struct ThreadClockSet {
124 /// The increasing clock representing timestamps
125 /// that happen-before this thread.
128 /// The set of timestamps that will happen-before this
129 /// thread once it performs an acquire fence.
130 fence_acquire: VClock,
132 /// The last timestamp of happens-before relations that
133 /// have been released by this thread by a fence.
134 fence_release: VClock,
137 impl ThreadClockSet {
138 /// Apply the effects of a release fence to this
139 /// set of thread vector clocks.
141 fn apply_release_fence(&mut self) {
142 self.fence_release.clone_from(&self.clock);
145 /// Apply the effects of a acquire fence to this
146 /// set of thread vector clocks.
148 fn apply_acquire_fence(&mut self) {
149 self.clock.join(&self.fence_acquire);
152 /// Increment the happens-before clock at a
155 fn increment_clock(&mut self, index: VectorIdx) {
156 self.clock.increment_index(index);
159 /// Join the happens-before clock with that of
160 /// another thread, used to model thread join
162 fn join_with(&mut self, other: &ThreadClockSet) {
163 self.clock.join(&other.clock);
167 /// Error returned by finding a data race
168 /// should be elaborated upon.
169 #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
172 /// Externally stored memory cell clocks
173 /// explicitly to reduce memory usage for the
174 /// common case where no atomic operations
175 /// exists on the memory cell.
176 #[derive(Clone, PartialEq, Eq, Default, Debug)]
177 struct AtomicMemoryCellClocks {
178 /// The clock-vector of the timestamp of the last atomic
179 /// read operation performed by each thread.
180 /// This detects potential data-races between atomic read
181 /// and non-atomic write operations.
184 /// The clock-vector of the timestamp of the last atomic
185 /// write operation performed by each thread.
186 /// This detects potential data-races between atomic write
187 /// and non-atomic read or write operations.
188 write_vector: VClock,
190 /// Synchronization vector for acquire-release semantics
191 /// contains the vector of timestamps that will
192 /// happen-before a thread if an acquire-load is
193 /// performed on the data.
197 /// Type of write operation: allocating memory
198 /// non-atomic writes and deallocating memory
199 /// are all treated as writes for the purpose
200 /// of the data-race detector.
201 #[derive(Copy, Clone, PartialEq, Eq, Debug)]
206 /// Standard unsynchronized write.
209 /// Deallocate memory.
210 /// Note that when memory is deallocated first, later non-atomic accesses
211 /// will be reported as use-after-free, not as data races.
212 /// (Same for `Allocate` above.)
216 fn get_descriptor(self) -> &'static str {
218 WriteType::Allocate => "Allocate",
219 WriteType::Write => "Write",
220 WriteType::Deallocate => "Deallocate",
225 /// Memory Cell vector clock metadata
226 /// for data-race detection.
227 #[derive(Clone, PartialEq, Eq, Debug)]
228 struct MemoryCellClocks {
229 /// The vector-clock timestamp of the last write
230 /// corresponding to the writing threads timestamp.
233 /// The identifier of the vector index, corresponding to a thread
234 /// that performed the last write operation.
235 write_index: VectorIdx,
237 /// The type of operation that the write index represents,
238 /// either newly allocated memory, a non-atomic write or
239 /// a deallocation of memory.
240 write_type: WriteType,
242 /// The vector-clock of the timestamp of the last read operation
243 /// performed by a thread since the last write operation occurred.
244 /// It is reset to zero on each write operation.
247 /// Atomic acquire & release sequence tracking clocks.
248 /// For non-atomic memory in the common case this
249 /// value is set to None.
250 atomic_ops: Option<Box<AtomicMemoryCellClocks>>,
253 impl MemoryCellClocks {
254 /// Create a new set of clocks representing memory allocated
255 /// at a given vector timestamp and index.
256 fn new(alloc: VTimestamp, alloc_index: VectorIdx) -> Self {
258 read: VClock::default(),
260 write_index: alloc_index,
261 write_type: WriteType::Allocate,
266 /// Load the internal atomic memory cells if they exist.
268 fn atomic(&self) -> Option<&AtomicMemoryCellClocks> {
269 match &self.atomic_ops {
270 Some(op) => Some(&*op),
275 /// Load or create the internal atomic memory metadata
276 /// if it does not exist.
278 fn atomic_mut(&mut self) -> &mut AtomicMemoryCellClocks {
279 self.atomic_ops.get_or_insert_with(Default::default)
282 /// Update memory cell data-race tracking for atomic
283 /// load acquire semantics, is a no-op if this memory was
284 /// not used previously as atomic memory.
287 clocks: &mut ThreadClockSet,
289 ) -> Result<(), DataRace> {
290 self.atomic_read_detect(clocks, index)?;
291 if let Some(atomic) = self.atomic() {
292 clocks.clock.join(&atomic.sync_vector);
297 /// Update memory cell data-race tracking for atomic
298 /// load relaxed semantics, is a no-op if this memory was
299 /// not used previously as atomic memory.
302 clocks: &mut ThreadClockSet,
304 ) -> Result<(), DataRace> {
305 self.atomic_read_detect(clocks, index)?;
306 if let Some(atomic) = self.atomic() {
307 clocks.fence_acquire.join(&atomic.sync_vector);
312 /// Update the memory cell data-race tracking for atomic
313 /// store release semantics.
314 fn store_release(&mut self, clocks: &ThreadClockSet, index: VectorIdx) -> Result<(), DataRace> {
315 self.atomic_write_detect(clocks, index)?;
316 let atomic = self.atomic_mut();
317 atomic.sync_vector.clone_from(&clocks.clock);
321 /// Update the memory cell data-race tracking for atomic
322 /// store relaxed semantics.
323 fn store_relaxed(&mut self, clocks: &ThreadClockSet, index: VectorIdx) -> Result<(), DataRace> {
324 self.atomic_write_detect(clocks, index)?;
326 // The handling of release sequences was changed in C++20 and so
327 // the code here is different to the paper since now all relaxed
328 // stores block release sequences. The exception for same-thread
329 // relaxed stores has been removed.
330 let atomic = self.atomic_mut();
331 atomic.sync_vector.clone_from(&clocks.fence_release);
335 /// Update the memory cell data-race tracking for atomic
336 /// store release semantics for RMW operations.
337 fn rmw_release(&mut self, clocks: &ThreadClockSet, index: VectorIdx) -> Result<(), DataRace> {
338 self.atomic_write_detect(clocks, index)?;
339 let atomic = self.atomic_mut();
340 atomic.sync_vector.join(&clocks.clock);
344 /// Update the memory cell data-race tracking for atomic
345 /// store relaxed semantics for RMW operations.
346 fn rmw_relaxed(&mut self, clocks: &ThreadClockSet, index: VectorIdx) -> Result<(), DataRace> {
347 self.atomic_write_detect(clocks, index)?;
348 let atomic = self.atomic_mut();
349 atomic.sync_vector.join(&clocks.fence_release);
353 /// Detect data-races with an atomic read, caused by a non-atomic write that does
354 /// not happen-before the atomic-read.
355 fn atomic_read_detect(
357 clocks: &ThreadClockSet,
359 ) -> Result<(), DataRace> {
360 log::trace!("Atomic read with vectors: {:#?} :: {:#?}", self, clocks);
361 if self.write <= clocks.clock[self.write_index] {
362 let atomic = self.atomic_mut();
363 atomic.read_vector.set_at_index(&clocks.clock, index);
370 /// Detect data-races with an atomic write, either with a non-atomic read or with
371 /// a non-atomic write.
372 fn atomic_write_detect(
374 clocks: &ThreadClockSet,
376 ) -> Result<(), DataRace> {
377 log::trace!("Atomic write with vectors: {:#?} :: {:#?}", self, clocks);
378 if self.write <= clocks.clock[self.write_index] && self.read <= clocks.clock {
379 let atomic = self.atomic_mut();
380 atomic.write_vector.set_at_index(&clocks.clock, index);
387 /// Detect races for non-atomic read operations at the current memory cell
388 /// returns true if a data-race is detected.
391 clocks: &ThreadClockSet,
393 ) -> Result<(), DataRace> {
394 log::trace!("Unsynchronized read with vectors: {:#?} :: {:#?}", self, clocks);
395 if self.write <= clocks.clock[self.write_index] {
396 let race_free = if let Some(atomic) = self.atomic() {
397 atomic.write_vector <= clocks.clock
402 self.read.set_at_index(&clocks.clock, index);
412 /// Detect races for non-atomic write operations at the current memory cell
413 /// returns true if a data-race is detected.
414 fn write_race_detect(
416 clocks: &ThreadClockSet,
418 write_type: WriteType,
419 ) -> Result<(), DataRace> {
420 log::trace!("Unsynchronized write with vectors: {:#?} :: {:#?}", self, clocks);
421 if self.write <= clocks.clock[self.write_index] && self.read <= clocks.clock {
422 let race_free = if let Some(atomic) = self.atomic() {
423 atomic.write_vector <= clocks.clock && atomic.read_vector <= clocks.clock
428 self.write = clocks.clock[index];
429 self.write_index = index;
430 self.write_type = write_type;
431 self.read.set_zero_vector();
442 /// Evaluation context extensions.
443 impl<'mir, 'tcx: 'mir> EvalContextExt<'mir, 'tcx> for MiriEvalContext<'mir, 'tcx> {}
444 pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
445 /// Atomic variant of read_scalar_at_offset.
446 fn read_scalar_at_offset_atomic(
448 op: &OpTy<'tcx, Tag>,
450 layout: TyAndLayout<'tcx>,
451 atomic: AtomicReadOp,
452 ) -> InterpResult<'tcx, ScalarMaybeUninit<Tag>> {
453 let this = self.eval_context_ref();
454 let op_place = this.deref_operand(op)?;
455 let offset = Size::from_bytes(offset);
457 // Ensure that the following read at an offset is within bounds.
458 assert!(op_place.layout.size >= offset + layout.size);
459 let value_place = op_place.offset(offset, MemPlaceMeta::None, layout, this)?;
460 this.read_scalar_atomic(&value_place, atomic)
463 /// Atomic variant of write_scalar_at_offset.
464 fn write_scalar_at_offset_atomic(
466 op: &OpTy<'tcx, Tag>,
468 value: impl Into<ScalarMaybeUninit<Tag>>,
469 layout: TyAndLayout<'tcx>,
470 atomic: AtomicWriteOp,
471 ) -> InterpResult<'tcx> {
472 let this = self.eval_context_mut();
473 let op_place = this.deref_operand(op)?;
474 let offset = Size::from_bytes(offset);
476 // Ensure that the following read at an offset is within bounds.
477 assert!(op_place.layout.size >= offset + layout.size);
478 let value_place = op_place.offset(offset, MemPlaceMeta::None, layout, this)?;
479 this.write_scalar_atomic(value.into(), &value_place, atomic)
482 /// Perform an atomic read operation at the memory location.
483 fn read_scalar_atomic(
485 place: &MPlaceTy<'tcx, Tag>,
486 atomic: AtomicReadOp,
487 ) -> InterpResult<'tcx, ScalarMaybeUninit<Tag>> {
488 let this = self.eval_context_ref();
489 let scalar = this.allow_data_races_ref(move |this| this.read_scalar(&place.into()))?;
490 this.validate_atomic_load(place, atomic)?;
494 /// Perform an atomic write operation at the memory location.
495 fn write_scalar_atomic(
497 val: ScalarMaybeUninit<Tag>,
498 dest: &MPlaceTy<'tcx, Tag>,
499 atomic: AtomicWriteOp,
500 ) -> InterpResult<'tcx> {
501 let this = self.eval_context_mut();
502 this.allow_data_races_mut(move |this| this.write_scalar(val, &(*dest).into()))?;
503 this.validate_atomic_store(dest, atomic)
506 /// Perform a atomic operation on a memory location.
507 fn atomic_op_immediate(
509 place: &MPlaceTy<'tcx, Tag>,
510 rhs: &ImmTy<'tcx, Tag>,
514 ) -> InterpResult<'tcx, ImmTy<'tcx, Tag>> {
515 let this = self.eval_context_mut();
517 let old = this.allow_data_races_mut(|this| this.read_immediate(&place.into()))?;
519 // Atomics wrap around on overflow.
520 let val = this.binary_op(op, &old, rhs)?;
521 let val = if neg { this.unary_op(mir::UnOp::Not, &val)? } else { val };
522 this.allow_data_races_mut(|this| this.write_immediate(*val, &(*place).into()))?;
524 this.validate_atomic_rmw(place, atomic)?;
528 /// Perform an atomic exchange with a memory place and a new
529 /// scalar value, the old value is returned.
530 fn atomic_exchange_scalar(
532 place: &MPlaceTy<'tcx, Tag>,
533 new: ScalarMaybeUninit<Tag>,
535 ) -> InterpResult<'tcx, ScalarMaybeUninit<Tag>> {
536 let this = self.eval_context_mut();
538 let old = this.allow_data_races_mut(|this| this.read_scalar(&place.into()))?;
539 this.allow_data_races_mut(|this| this.write_scalar(new, &(*place).into()))?;
540 this.validate_atomic_rmw(place, atomic)?;
544 /// Perform an conditional atomic exchange with a memory place and a new
545 /// scalar value, the old value is returned.
546 fn atomic_min_max_scalar(
548 place: &MPlaceTy<'tcx, Tag>,
549 rhs: ImmTy<'tcx, Tag>,
552 ) -> InterpResult<'tcx, ImmTy<'tcx, Tag>> {
553 let this = self.eval_context_mut();
555 let old = this.allow_data_races_mut(|this| this.read_immediate(&place.into()))?;
556 let lt = this.overflowing_binary_op(mir::BinOp::Lt, &old, &rhs)?.0.to_bool()?;
558 let new_val = if min {
559 if lt { &old } else { &rhs }
561 if lt { &rhs } else { &old }
564 this.allow_data_races_mut(|this| this.write_immediate_to_mplace(**new_val, place))?;
566 this.validate_atomic_rmw(&place, atomic)?;
568 // Return the old value.
572 /// Perform an atomic compare and exchange at a given memory location.
573 /// On success an atomic RMW operation is performed and on failure
574 /// only an atomic read occurs. If `can_fail_spuriously` is true,
575 /// then we treat it as a "compare_exchange_weak" operation, and
576 /// some portion of the time fail even when the values are actually
578 fn atomic_compare_exchange_scalar(
580 place: &MPlaceTy<'tcx, Tag>,
581 expect_old: &ImmTy<'tcx, Tag>,
582 new: ScalarMaybeUninit<Tag>,
585 can_fail_spuriously: bool,
586 ) -> InterpResult<'tcx, Immediate<Tag>> {
588 let this = self.eval_context_mut();
590 // Failure ordering cannot be stronger than success ordering, therefore first attempt
591 // to read with the failure ordering and if successful then try again with the success
592 // read ordering and write in the success case.
593 // Read as immediate for the sake of `binary_op()`
594 let old = this.allow_data_races_mut(|this| this.read_immediate(&(place.into())))?;
595 // `binary_op` will bail if either of them is not a scalar.
596 let eq = this.overflowing_binary_op(mir::BinOp::Eq, &old, expect_old)?.0;
597 // If the operation would succeed, but is "weak", fail some portion
598 // of the time, based on `rate`.
599 let rate = this.memory.extra.cmpxchg_weak_failure_rate;
600 let cmpxchg_success = eq.to_bool()?
601 && (!can_fail_spuriously || this.memory.extra.rng.borrow_mut().gen::<f64>() < rate);
602 let res = Immediate::ScalarPair(
603 old.to_scalar_or_uninit(),
604 Scalar::from_bool(cmpxchg_success).into(),
607 // Update ptr depending on comparison.
608 // if successful, perform a full rw-atomic validation
609 // otherwise treat this as an atomic load with the fail ordering.
611 this.allow_data_races_mut(|this| this.write_scalar(new, &(*place).into()))?;
612 this.validate_atomic_rmw(place, success)?;
614 this.validate_atomic_load(place, fail)?;
617 // Return the old value.
621 /// Update the data-race detector for an atomic read occurring at the
622 /// associated memory-place and on the current thread.
623 fn validate_atomic_load(
625 place: &MPlaceTy<'tcx, Tag>,
626 atomic: AtomicReadOp,
627 ) -> InterpResult<'tcx> {
628 let this = self.eval_context_ref();
629 this.validate_atomic_op(
633 move |memory, clocks, index, atomic| {
634 if atomic == AtomicReadOp::Relaxed {
635 memory.load_relaxed(&mut *clocks, index)
637 memory.load_acquire(&mut *clocks, index)
643 /// Update the data-race detector for an atomic write occurring at the
644 /// associated memory-place and on the current thread.
645 fn validate_atomic_store(
647 place: &MPlaceTy<'tcx, Tag>,
648 atomic: AtomicWriteOp,
649 ) -> InterpResult<'tcx> {
650 let this = self.eval_context_ref();
651 this.validate_atomic_op(
655 move |memory, clocks, index, atomic| {
656 if atomic == AtomicWriteOp::Relaxed {
657 memory.store_relaxed(clocks, index)
659 memory.store_release(clocks, index)
665 /// Update the data-race detector for an atomic read-modify-write occurring
666 /// at the associated memory place and on the current thread.
667 fn validate_atomic_rmw(
669 place: &MPlaceTy<'tcx, Tag>,
671 ) -> InterpResult<'tcx> {
673 let acquire = matches!(atomic, Acquire | AcqRel | SeqCst);
674 let release = matches!(atomic, Release | AcqRel | SeqCst);
675 let this = self.eval_context_ref();
676 this.validate_atomic_op(place, atomic, "Atomic RMW", move |memory, clocks, index, _| {
678 memory.load_acquire(clocks, index)?;
680 memory.load_relaxed(clocks, index)?;
683 memory.rmw_release(clocks, index)
685 memory.rmw_relaxed(clocks, index)
690 /// Update the data-race detector for an atomic fence on the current thread.
691 fn validate_atomic_fence(&mut self, atomic: AtomicFenceOp) -> InterpResult<'tcx> {
692 let this = self.eval_context_mut();
693 if let Some(data_race) = &this.memory.extra.data_race {
694 data_race.maybe_perform_sync_operation(move |index, mut clocks| {
695 log::trace!("Atomic fence on {:?} with ordering {:?}", index, atomic);
697 // Apply data-race detection for the current fences
698 // this treats AcqRel and SeqCst as the same as a acquire
699 // and release fence applied in the same timestamp.
700 if atomic != AtomicFenceOp::Release {
701 // Either Acquire | AcqRel | SeqCst
702 clocks.apply_acquire_fence();
704 if atomic != AtomicFenceOp::Acquire {
705 // Either Release | AcqRel | SeqCst
706 clocks.apply_release_fence();
709 // Increment timestamp in case of release semantics.
710 Ok(atomic != AtomicFenceOp::Acquire)
717 fn reset_vector_clocks(&mut self, ptr: Pointer<Tag>, size: Size) -> InterpResult<'tcx> {
718 let this = self.eval_context_mut();
719 if let Some(data_race) = &mut this.memory.extra.data_race {
720 if data_race.multi_threaded.get() {
722 this.memory.get_alloc_extra_mut(ptr.alloc_id)?.0.data_race.as_mut().unwrap();
723 alloc_meta.reset_clocks(ptr.offset, size);
730 /// Vector clock metadata for a logical memory allocation.
731 #[derive(Debug, Clone)]
732 pub struct VClockAlloc {
733 /// Assigning each byte a MemoryCellClocks.
734 alloc_ranges: RefCell<RangeMap<MemoryCellClocks>>,
738 /// Create a new data-race detector for newly allocated memory.
739 pub fn new_allocation(
740 global: &MemoryExtra,
742 kind: MemoryKind<MiriMemoryKind>,
744 let (alloc_timestamp, alloc_index) = match kind {
745 // User allocated and stack memory should track allocation.
747 MiriMemoryKind::Rust | MiriMemoryKind::C | MiriMemoryKind::WinHeap,
749 | MemoryKind::Stack => {
750 let (alloc_index, clocks) = global.current_thread_state();
751 let alloc_timestamp = clocks.clock[alloc_index];
752 (alloc_timestamp, alloc_index)
754 // Other global memory should trace races but be allocated at the 0 timestamp.
756 MiriMemoryKind::Global
757 | MiriMemoryKind::Machine
758 | MiriMemoryKind::Env
759 | MiriMemoryKind::ExternStatic
760 | MiriMemoryKind::Tls,
762 | MemoryKind::CallerLocation
763 | MemoryKind::Vtable => (0, VectorIdx::MAX_INDEX),
766 alloc_ranges: RefCell::new(RangeMap::new(
768 MemoryCellClocks::new(alloc_timestamp, alloc_index),
773 fn reset_clocks(&mut self, offset: Size, len: Size) {
774 let mut alloc_ranges = self.alloc_ranges.borrow_mut();
775 for (_, range) in alloc_ranges.iter_mut(offset, len) {
776 // Reset the portion of the range
777 *range = MemoryCellClocks::new(0, VectorIdx::MAX_INDEX);
781 // Find an index, if one exists where the value
782 // in `l` is greater than the value in `r`.
783 fn find_gt_index(l: &VClock, r: &VClock) -> Option<VectorIdx> {
784 log::trace!("Find index where not {:?} <= {:?}", l, r);
785 let l_slice = l.as_slice();
786 let r_slice = r.as_slice();
791 .find_map(|(idx, (&l, &r))| if l > r { Some(idx) } else { None })
793 if l_slice.len() > r_slice.len() {
794 // By invariant, if l_slice is longer
795 // then one element must be larger.
796 // This just validates that this is true
797 // and reports earlier elements first.
798 let l_remainder_slice = &l_slice[r_slice.len()..];
799 let idx = l_remainder_slice
802 .find_map(|(idx, &r)| if r == 0 { None } else { Some(idx) })
803 .expect("Invalid VClock Invariant");
804 Some(idx + r_slice.len())
809 .map(|idx| VectorIdx::new(idx))
812 /// Report a data-race found in the program.
813 /// This finds the two racing threads and the type
814 /// of data-race that occurred. This will also
815 /// return info about the memory location the data-race
819 fn report_data_race<'tcx>(
820 global: &MemoryExtra,
821 range: &MemoryCellClocks,
824 pointer: Pointer<Tag>,
826 ) -> InterpResult<'tcx> {
827 let (current_index, current_clocks) = global.current_thread_state();
829 let (other_action, other_thread, other_clock) = if range.write
830 > current_clocks.clock[range.write_index]
832 // Convert the write action into the vector clock it
833 // represents for diagnostic purposes.
834 write_clock = VClock::new_with_index(range.write_index, range.write);
835 (range.write_type.get_descriptor(), range.write_index, &write_clock)
836 } else if let Some(idx) = Self::find_gt_index(&range.read, ¤t_clocks.clock) {
837 ("Read", idx, &range.read)
838 } else if !is_atomic {
839 if let Some(atomic) = range.atomic() {
840 if let Some(idx) = Self::find_gt_index(&atomic.write_vector, ¤t_clocks.clock)
842 ("Atomic Store", idx, &atomic.write_vector)
843 } else if let Some(idx) =
844 Self::find_gt_index(&atomic.read_vector, ¤t_clocks.clock)
846 ("Atomic Load", idx, &atomic.read_vector)
849 "Failed to report data-race for non-atomic operation: no race found"
854 "Failed to report data-race for non-atomic operation: no atomic component"
858 unreachable!("Failed to report data-race for atomic operation")
861 // Load elaborated thread information about the racing thread actions.
862 let current_thread_info = global.print_thread_metadata(current_index);
863 let other_thread_info = global.print_thread_metadata(other_thread);
865 // Throw the data-race detection.
867 "Data race detected between {} on {} and {} on {}, memory({:?},offset={},size={})\
868 \n(current vector clock = {:?}, conflicting timestamp = {:?})",
874 pointer.offset.bytes(),
876 current_clocks.clock,
881 /// Detect data-races for an unsynchronized read operation, will not perform
882 /// data-race detection if `multi-threaded` is false, either due to no threads
883 /// being created or if it is temporarily disabled during a racy read or write
884 /// operation for which data-race detection is handled separately, for example
885 /// atomic read operations.
888 pointer: Pointer<Tag>,
890 global: &GlobalState,
891 ) -> InterpResult<'tcx> {
892 if global.multi_threaded.get() {
893 let (index, clocks) = global.current_thread_state();
894 let mut alloc_ranges = self.alloc_ranges.borrow_mut();
895 for (_, range) in alloc_ranges.iter_mut(pointer.offset, len) {
896 if let Err(DataRace) = range.read_race_detect(&*clocks, index) {
898 return Self::report_data_race(global, range, "Read", false, pointer, len);
907 // Shared code for detecting data-races on unique access to a section of memory
908 fn unique_access<'tcx>(
910 pointer: Pointer<Tag>,
912 write_type: WriteType,
913 global: &mut GlobalState,
914 ) -> InterpResult<'tcx> {
915 if global.multi_threaded.get() {
916 let (index, clocks) = global.current_thread_state();
917 for (_, range) in self.alloc_ranges.get_mut().iter_mut(pointer.offset, len) {
918 if let Err(DataRace) = range.write_race_detect(&*clocks, index, write_type) {
920 return Self::report_data_race(
923 write_type.get_descriptor(),
936 /// Detect data-races for an unsynchronized write operation, will not perform
937 /// data-race threads if `multi-threaded` is false, either due to no threads
938 /// being created or if it is temporarily disabled during a racy read or write
942 pointer: Pointer<Tag>,
944 global: &mut GlobalState,
945 ) -> InterpResult<'tcx> {
946 self.unique_access(pointer, len, WriteType::Write, global)
949 /// Detect data-races for an unsynchronized deallocate operation, will not perform
950 /// data-race threads if `multi-threaded` is false, either due to no threads
951 /// being created or if it is temporarily disabled during a racy read or write
953 pub fn deallocate<'tcx>(
955 pointer: Pointer<Tag>,
957 global: &mut GlobalState,
958 ) -> InterpResult<'tcx> {
959 self.unique_access(pointer, len, WriteType::Deallocate, global)
963 impl<'mir, 'tcx: 'mir> EvalContextPrivExt<'mir, 'tcx> for MiriEvalContext<'mir, 'tcx> {}
964 trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
965 // Temporarily allow data-races to occur, this should only be
966 // used if either one of the appropriate `validate_atomic` functions
967 // will be called to treat a memory access as atomic or if the memory
968 // being accessed should be treated as internal state, that cannot be
969 // accessed by the interpreted program.
971 fn allow_data_races_ref<R>(&self, op: impl FnOnce(&MiriEvalContext<'mir, 'tcx>) -> R) -> R {
972 let this = self.eval_context_ref();
973 let old = if let Some(data_race) = &this.memory.extra.data_race {
974 data_race.multi_threaded.replace(false)
978 let result = op(this);
979 if let Some(data_race) = &this.memory.extra.data_race {
980 data_race.multi_threaded.set(old);
985 /// Same as `allow_data_races_ref`, this temporarily disables any data-race detection and
986 /// so should only be used for atomic operations or internal state that the program cannot
989 fn allow_data_races_mut<R>(
991 op: impl FnOnce(&mut MiriEvalContext<'mir, 'tcx>) -> R,
993 let this = self.eval_context_mut();
994 let old = if let Some(data_race) = &this.memory.extra.data_race {
995 data_race.multi_threaded.replace(false)
999 let result = op(this);
1000 if let Some(data_race) = &this.memory.extra.data_race {
1001 data_race.multi_threaded.set(old);
1006 /// Generic atomic operation implementation,
1007 /// this accesses memory via get_raw instead of
1008 /// get_raw_mut, due to issues calling get_raw_mut
1009 /// for atomic loads from read-only memory.
1010 /// FIXME: is this valid, or should get_raw_mut be used for
1011 /// atomic-stores/atomic-rmw?
1012 fn validate_atomic_op<A: Debug + Copy>(
1014 place: &MPlaceTy<'tcx, Tag>,
1018 &mut MemoryCellClocks,
1019 &mut ThreadClockSet,
1022 ) -> Result<(), DataRace>,
1023 ) -> InterpResult<'tcx> {
1024 let this = self.eval_context_ref();
1025 if let Some(data_race) = &this.memory.extra.data_race {
1026 if data_race.multi_threaded.get() {
1027 // Load and log the atomic operation.
1028 let place_ptr = place.ptr.assert_ptr();
1029 let size = place.layout.size;
1031 &this.memory.get_alloc_extra(place_ptr.alloc_id)?.data_race.as_ref().unwrap();
1033 "Atomic op({}) with ordering {:?} on memory({:?}, offset={}, size={})",
1037 place_ptr.offset.bytes(),
1041 // Perform the atomic operation.
1042 data_race.maybe_perform_sync_operation(|index, mut clocks| {
1044 alloc_meta.alloc_ranges.borrow_mut().iter_mut(place_ptr.offset, size)
1046 if let Err(DataRace) = op(range, &mut *clocks, index, atomic) {
1048 return VClockAlloc::report_data_race(
1060 // This conservatively assumes all operations have release semantics
1064 // Log changes to atomic memory.
1065 if log::log_enabled!(log::Level::Trace) {
1066 for (_, range) in alloc_meta.alloc_ranges.borrow().iter(place_ptr.offset, size)
1069 "Updated atomic memory({:?}, offset={}, size={}) to {:#?}",
1070 place.ptr.assert_ptr().alloc_id,
1071 place_ptr.offset.bytes(),
1083 /// Extra metadata associated with a thread.
1084 #[derive(Debug, Clone, Default)]
1085 struct ThreadExtraState {
1086 /// The current vector index in use by the
1087 /// thread currently, this is set to None
1088 /// after the vector index has been re-used
1089 /// and hence the value will never need to be
1090 /// read during data-race reporting.
1091 vector_index: Option<VectorIdx>,
1093 /// The name of the thread, updated for better
1094 /// diagnostics when reporting detected data
1096 thread_name: Option<Box<str>>,
1098 /// Thread termination vector clock, this
1099 /// is set on thread termination and is used
1100 /// for joining on threads since the vector_index
1101 /// may be re-used when the join operation occurs.
1102 termination_vector_clock: Option<VClock>,
1105 /// Global data-race detection state, contains the currently
1106 /// executing thread as well as the vector-clocks associated
1107 /// with each of the threads.
1108 #[derive(Debug, Clone)]
1109 pub struct GlobalState {
1110 /// Set to true once the first additional
1111 /// thread has launched, due to the dependency
1112 /// between before and after a thread launch.
1113 /// Any data-races must be recorded after this
1114 /// so concurrent execution can ignore recording
1116 multi_threaded: Cell<bool>,
1118 /// Mapping of a vector index to a known set of thread
1119 /// clocks, this is not directly mapping from a thread id
1120 /// since it may refer to multiple threads.
1121 vector_clocks: RefCell<IndexVec<VectorIdx, ThreadClockSet>>,
1123 /// Mapping of a given vector index to the current thread
1124 /// that the execution is representing, this may change
1125 /// if a vector index is re-assigned to a new thread.
1126 vector_info: RefCell<IndexVec<VectorIdx, ThreadId>>,
1128 /// The mapping of a given thread to associated thread metadata.
1129 thread_info: RefCell<IndexVec<ThreadId, ThreadExtraState>>,
1131 /// The current vector index being executed.
1132 current_index: Cell<VectorIdx>,
1134 /// Potential vector indices that could be re-used on thread creation
1135 /// values are inserted here on after the thread has terminated and
1136 /// been joined with, and hence may potentially become free
1137 /// for use as the index for a new thread.
1138 /// Elements in this set may still require the vector index to
1139 /// report data-races, and can only be re-used after all
1140 /// active vector-clocks catch up with the threads timestamp.
1141 reuse_candidates: RefCell<FxHashSet<VectorIdx>>,
1143 /// Counts the number of threads that are currently active
1144 /// if the number of active threads reduces to 1 and then
1145 /// a join operation occurs with the remaining main thread
1146 /// then multi-threaded execution may be disabled.
1147 active_thread_count: Cell<usize>,
1149 /// This contains threads that have terminated, but not yet joined
1150 /// and so cannot become re-use candidates until a join operation
1152 /// The associated vector index will be moved into re-use candidates
1153 /// after the join operation occurs.
1154 terminated_threads: RefCell<FxHashMap<ThreadId, VectorIdx>>,
1158 /// Create a new global state, setup with just thread-id=0
1159 /// advanced to timestamp = 1.
1160 pub fn new() -> Self {
1161 let global_state = GlobalState {
1162 multi_threaded: Cell::new(false),
1163 vector_clocks: RefCell::new(IndexVec::new()),
1164 vector_info: RefCell::new(IndexVec::new()),
1165 thread_info: RefCell::new(IndexVec::new()),
1166 current_index: Cell::new(VectorIdx::new(0)),
1167 active_thread_count: Cell::new(1),
1168 reuse_candidates: RefCell::new(FxHashSet::default()),
1169 terminated_threads: RefCell::new(FxHashMap::default()),
1172 // Setup the main-thread since it is not explicitly created:
1173 // uses vector index and thread-id 0, also the rust runtime gives
1174 // the main-thread a name of "main".
1175 let index = global_state.vector_clocks.borrow_mut().push(ThreadClockSet::default());
1176 global_state.vector_info.borrow_mut().push(ThreadId::new(0));
1177 global_state.thread_info.borrow_mut().push(ThreadExtraState {
1178 vector_index: Some(index),
1179 thread_name: Some("main".to_string().into_boxed_str()),
1180 termination_vector_clock: None,
1186 // Try to find vector index values that can potentially be re-used
1187 // by a new thread instead of a new vector index being created.
1188 fn find_vector_index_reuse_candidate(&self) -> Option<VectorIdx> {
1189 let mut reuse = self.reuse_candidates.borrow_mut();
1190 let vector_clocks = self.vector_clocks.borrow();
1191 let vector_info = self.vector_info.borrow();
1192 let terminated_threads = self.terminated_threads.borrow();
1193 for &candidate in reuse.iter() {
1194 let target_timestamp = vector_clocks[candidate].clock[candidate];
1195 if vector_clocks.iter_enumerated().all(|(clock_idx, clock)| {
1196 // The thread happens before the clock, and hence cannot report
1197 // a data-race with this the candidate index.
1198 let no_data_race = clock.clock[candidate] >= target_timestamp;
1200 // The vector represents a thread that has terminated and hence cannot
1201 // report a data-race with the candidate index.
1202 let thread_id = vector_info[clock_idx];
1203 let vector_terminated =
1204 reuse.contains(&clock_idx) || terminated_threads.contains_key(&thread_id);
1206 // The vector index cannot report a race with the candidate index
1207 // and hence allows the candidate index to be re-used.
1208 no_data_race || vector_terminated
1210 // All vector clocks for each vector index are equal to
1211 // the target timestamp, and the thread is known to have
1212 // terminated, therefore this vector clock index cannot
1213 // report any more data-races.
1214 assert!(reuse.remove(&candidate));
1215 return Some(candidate);
1221 // Hook for thread creation, enabled multi-threaded execution and marks
1222 // the current thread timestamp as happening-before the current thread.
1224 pub fn thread_created(&self, thread: ThreadId) {
1225 let current_index = self.current_index();
1227 // Increment the number of active threads.
1228 let active_threads = self.active_thread_count.get();
1229 self.active_thread_count.set(active_threads + 1);
1231 // Enable multi-threaded execution, there are now two threads
1232 // so data-races are now possible.
1233 self.multi_threaded.set(true);
1235 // Load and setup the associated thread metadata
1236 let mut thread_info = self.thread_info.borrow_mut();
1237 thread_info.ensure_contains_elem(thread, Default::default);
1239 // Assign a vector index for the thread, attempting to re-use an old
1240 // vector index that can no longer report any data-races if possible.
1241 let created_index = if let Some(reuse_index) = self.find_vector_index_reuse_candidate() {
1242 // Now re-configure the re-use candidate, increment the clock
1243 // for the new sync use of the vector.
1244 let mut vector_clocks = self.vector_clocks.borrow_mut();
1245 vector_clocks[reuse_index].increment_clock(reuse_index);
1247 // Locate the old thread the vector was associated with and update
1248 // it to represent the new thread instead.
1249 let mut vector_info = self.vector_info.borrow_mut();
1250 let old_thread = vector_info[reuse_index];
1251 vector_info[reuse_index] = thread;
1253 // Mark the thread the vector index was associated with as no longer
1254 // representing a thread index.
1255 thread_info[old_thread].vector_index = None;
1259 // No vector re-use candidates available, instead create
1260 // a new vector index.
1261 let mut vector_info = self.vector_info.borrow_mut();
1262 vector_info.push(thread)
1265 log::trace!("Creating thread = {:?} with vector index = {:?}", thread, created_index);
1267 // Mark the chosen vector index as in use by the thread.
1268 thread_info[thread].vector_index = Some(created_index);
1270 // Create a thread clock set if applicable.
1271 let mut vector_clocks = self.vector_clocks.borrow_mut();
1272 if created_index == vector_clocks.next_index() {
1273 vector_clocks.push(ThreadClockSet::default());
1276 // Now load the two clocks and configure the initial state.
1277 let (current, created) = vector_clocks.pick2_mut(current_index, created_index);
1279 // Join the created with current, since the current threads
1280 // previous actions happen-before the created thread.
1281 created.join_with(current);
1283 // Advance both threads after the synchronized operation.
1284 // Both operations are considered to have release semantics.
1285 current.increment_clock(current_index);
1286 created.increment_clock(created_index);
1289 /// Hook on a thread join to update the implicit happens-before relation
1290 /// between the joined thread and the current thread.
1292 pub fn thread_joined(&self, current_thread: ThreadId, join_thread: ThreadId) {
1293 let mut clocks_vec = self.vector_clocks.borrow_mut();
1294 let thread_info = self.thread_info.borrow();
1296 // Load the vector clock of the current thread.
1297 let current_index = thread_info[current_thread]
1299 .expect("Performed thread join on thread with no assigned vector");
1300 let current = &mut clocks_vec[current_index];
1302 // Load the associated vector clock for the terminated thread.
1303 let join_clock = thread_info[join_thread]
1304 .termination_vector_clock
1306 .expect("Joined with thread but thread has not terminated");
1308 // The join thread happens-before the current thread
1309 // so update the current vector clock.
1310 // Is not a release operation so the clock is not incremented.
1311 current.clock.join(join_clock);
1313 // Check the number of active threads, if the value is 1
1314 // then test for potentially disabling multi-threaded execution.
1315 let active_threads = self.active_thread_count.get();
1316 if active_threads == 1 {
1317 // May potentially be able to disable multi-threaded execution.
1318 let current_clock = &clocks_vec[current_index];
1321 .all(|(idx, clocks)| clocks.clock[idx] <= current_clock.clock[idx])
1323 // All thread terminations happen-before the current clock
1324 // therefore no data-races can be reported until a new thread
1325 // is created, so disable multi-threaded execution.
1326 self.multi_threaded.set(false);
1330 // If the thread is marked as terminated but not joined
1331 // then move the thread to the re-use set.
1332 let mut termination = self.terminated_threads.borrow_mut();
1333 if let Some(index) = termination.remove(&join_thread) {
1334 let mut reuse = self.reuse_candidates.borrow_mut();
1335 reuse.insert(index);
1339 /// On thread termination, the vector-clock may re-used
1340 /// in the future once all remaining thread-clocks catch
1341 /// up with the time index of the terminated thread.
1342 /// This assigns thread termination with a unique index
1343 /// which will be used to join the thread
1344 /// This should be called strictly before any calls to
1345 /// `thread_joined`.
1347 pub fn thread_terminated(&self) {
1348 let current_index = self.current_index();
1350 // Increment the clock to a unique termination timestamp.
1351 let mut vector_clocks = self.vector_clocks.borrow_mut();
1352 let current_clocks = &mut vector_clocks[current_index];
1353 current_clocks.increment_clock(current_index);
1355 // Load the current thread id for the executing vector.
1356 let vector_info = self.vector_info.borrow();
1357 let current_thread = vector_info[current_index];
1359 // Load the current thread metadata, and move to a terminated
1360 // vector state. Setting up the vector clock all join operations
1362 let mut thread_info = self.thread_info.borrow_mut();
1363 let current = &mut thread_info[current_thread];
1364 current.termination_vector_clock = Some(current_clocks.clock.clone());
1366 // Add this thread as a candidate for re-use after a thread join
1368 let mut termination = self.terminated_threads.borrow_mut();
1369 termination.insert(current_thread, current_index);
1371 // Reduce the number of active threads, now that a thread has
1373 let mut active_threads = self.active_thread_count.get();
1374 active_threads -= 1;
1375 self.active_thread_count.set(active_threads);
1378 /// Hook for updating the local tracker of the currently
1379 /// enabled thread, should always be updated whenever
1380 /// `active_thread` in thread.rs is updated.
1382 pub fn thread_set_active(&self, thread: ThreadId) {
1383 let thread_info = self.thread_info.borrow();
1384 let vector_idx = thread_info[thread]
1386 .expect("Setting thread active with no assigned vector");
1387 self.current_index.set(vector_idx);
1390 /// Hook for updating the local tracker of the threads name
1391 /// this should always mirror the local value in thread.rs
1392 /// the thread name is used for improved diagnostics
1393 /// during a data-race.
1395 pub fn thread_set_name(&self, thread: ThreadId, name: String) {
1396 let name = name.into_boxed_str();
1397 let mut thread_info = self.thread_info.borrow_mut();
1398 thread_info[thread].thread_name = Some(name);
1401 /// Attempt to perform a synchronized operation, this
1402 /// will perform no operation if multi-threading is
1403 /// not currently enabled.
1404 /// Otherwise it will increment the clock for the current
1405 /// vector before and after the operation for data-race
1406 /// detection between any happens-before edges the
1407 /// operation may create.
1408 fn maybe_perform_sync_operation<'tcx>(
1410 op: impl FnOnce(VectorIdx, RefMut<'_, ThreadClockSet>) -> InterpResult<'tcx, bool>,
1411 ) -> InterpResult<'tcx> {
1412 if self.multi_threaded.get() {
1413 let (index, clocks) = self.current_thread_state_mut();
1414 if op(index, clocks)? {
1415 let (_, mut clocks) = self.current_thread_state_mut();
1416 clocks.increment_clock(index);
1422 /// Internal utility to identify a thread stored internally
1423 /// returns the id and the name for better diagnostics.
1424 fn print_thread_metadata(&self, vector: VectorIdx) -> String {
1425 let thread = self.vector_info.borrow()[vector];
1426 let thread_name = &self.thread_info.borrow()[thread].thread_name;
1427 if let Some(name) = thread_name {
1428 let name: &str = name;
1429 format!("Thread(id = {:?}, name = {:?})", thread.to_u32(), &*name)
1431 format!("Thread(id = {:?})", thread.to_u32())
1435 /// Acquire a lock, express that the previous call of
1436 /// `validate_lock_release` must happen before this.
1437 /// As this is an acquire operation, the thread timestamp is not
1439 pub fn validate_lock_acquire(&self, lock: &VClock, thread: ThreadId) {
1440 let (_, mut clocks) = self.load_thread_state_mut(thread);
1441 clocks.clock.join(&lock);
1444 /// Release a lock handle, express that this happens-before
1445 /// any subsequent calls to `validate_lock_acquire`.
1446 /// For normal locks this should be equivalent to `validate_lock_release_shared`
1447 /// since an acquire operation should have occurred before, however
1448 /// for futex & condvar operations this is not the case and this
1449 /// operation must be used.
1450 pub fn validate_lock_release(&self, lock: &mut VClock, thread: ThreadId) {
1451 let (index, mut clocks) = self.load_thread_state_mut(thread);
1452 lock.clone_from(&clocks.clock);
1453 clocks.increment_clock(index);
1456 /// Release a lock handle, express that this happens-before
1457 /// any subsequent calls to `validate_lock_acquire` as well
1458 /// as any previous calls to this function after any
1459 /// `validate_lock_release` calls.
1460 /// For normal locks this should be equivalent to `validate_lock_release`.
1461 /// This function only exists for joining over the set of concurrent readers
1462 /// in a read-write lock and should not be used for anything else.
1463 pub fn validate_lock_release_shared(&self, lock: &mut VClock, thread: ThreadId) {
1464 let (index, mut clocks) = self.load_thread_state_mut(thread);
1465 lock.join(&clocks.clock);
1466 clocks.increment_clock(index);
1469 /// Load the vector index used by the given thread as well as the set of vector clocks
1470 /// used by the thread.
1472 fn load_thread_state_mut(&self, thread: ThreadId) -> (VectorIdx, RefMut<'_, ThreadClockSet>) {
1473 let index = self.thread_info.borrow()[thread]
1475 .expect("Loading thread state for thread with no assigned vector");
1476 let ref_vector = self.vector_clocks.borrow_mut();
1477 let clocks = RefMut::map(ref_vector, |vec| &mut vec[index]);
1481 /// Load the current vector clock in use and the current set of thread clocks
1482 /// in use for the vector.
1484 fn current_thread_state(&self) -> (VectorIdx, Ref<'_, ThreadClockSet>) {
1485 let index = self.current_index();
1486 let ref_vector = self.vector_clocks.borrow();
1487 let clocks = Ref::map(ref_vector, |vec| &vec[index]);
1491 /// Load the current vector clock in use and the current set of thread clocks
1492 /// in use for the vector mutably for modification.
1494 fn current_thread_state_mut(&self) -> (VectorIdx, RefMut<'_, ThreadClockSet>) {
1495 let index = self.current_index();
1496 let ref_vector = self.vector_clocks.borrow_mut();
1497 let clocks = RefMut::map(ref_vector, |vec| &mut vec[index]);
1501 /// Return the current thread, should be the same
1502 /// as the data-race active thread.
1504 fn current_index(&self) -> VectorIdx {
1505 self.current_index.get()