miri/concurrency/
data_race.rs

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.
6//!
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.
11//!
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.
14//!
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
17//!
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.
22//!
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
30//! thread.
31//!
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.
37//!
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.
42
43use std::cell::{Cell, Ref, RefCell, RefMut};
44use std::fmt::Debug;
45use std::mem;
46
47use rustc_abi::{Align, HasDataLayout, Size};
48use rustc_ast::Mutability;
49use rustc_data_structures::fx::{FxHashMap, FxHashSet};
50use rustc_index::{Idx, IndexVec};
51use rustc_log::tracing;
52use rustc_middle::mir;
53use rustc_middle::ty::Ty;
54use rustc_span::Span;
55
56use super::vector_clock::{VClock, VTimestamp, VectorIdx};
57use super::weak_memory::EvalContextExt as _;
58use crate::concurrency::GlobalDataRaceHandler;
59use crate::diagnostics::RacingOp;
60use crate::intrinsics::AtomicRmwOp;
61use crate::*;
62
63pub type AllocState = VClockAlloc;
64
65/// Valid atomic read-write orderings, alias of atomic::Ordering (not non-exhaustive).
66#[derive(Copy, Clone, PartialEq, Eq, Debug)]
67pub enum AtomicRwOrd {
68    Relaxed,
69    Acquire,
70    Release,
71    AcqRel,
72    SeqCst,
73}
74
75/// Valid atomic read orderings, subset of atomic::Ordering.
76#[derive(Copy, Clone, PartialEq, Eq, Debug)]
77pub enum AtomicReadOrd {
78    Relaxed,
79    Acquire,
80    SeqCst,
81}
82
83/// Valid atomic write orderings, subset of atomic::Ordering.
84#[derive(Copy, Clone, PartialEq, Eq, Debug)]
85pub enum AtomicWriteOrd {
86    Relaxed,
87    Release,
88    SeqCst,
89}
90
91/// Valid atomic fence orderings, subset of atomic::Ordering.
92#[derive(Copy, Clone, PartialEq, Eq, Debug)]
93pub enum AtomicFenceOrd {
94    Acquire,
95    Release,
96    AcqRel,
97    SeqCst,
98}
99
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)]
104pub(super) struct ThreadClockSet {
105    /// The increasing clock representing timestamps
106    /// that happen-before this thread.
107    pub(super) clock: VClock,
108
109    /// The set of timestamps that will happen-before this
110    /// thread once it performs an acquire fence.
111    fence_acquire: VClock,
112
113    /// The last timestamp of happens-before relations that
114    /// have been released by this thread by a release fence.
115    fence_release: VClock,
116
117    /// Timestamps of the last SC write performed by each
118    /// thread, updated when this thread performs an SC fence.
119    /// This is never acquired into the thread's clock, it
120    /// just limits which old writes can be seen in weak memory emulation.
121    pub(super) write_seqcst: VClock,
122
123    /// Timestamps of the last SC fence performed by each
124    /// thread, updated when this thread performs an SC read.
125    /// This is never acquired into the thread's clock, it
126    /// just limits which old writes can be seen in weak memory emulation.
127    pub(super) read_seqcst: VClock,
128}
129
130impl ThreadClockSet {
131    /// Apply the effects of a release fence to this
132    /// set of thread vector clocks.
133    #[inline]
134    fn apply_release_fence(&mut self) {
135        self.fence_release.clone_from(&self.clock);
136    }
137
138    /// Apply the effects of an acquire fence to this
139    /// set of thread vector clocks.
140    #[inline]
141    fn apply_acquire_fence(&mut self) {
142        self.clock.join(&self.fence_acquire);
143    }
144
145    /// Increment the happens-before clock at a
146    /// known index.
147    #[inline]
148    fn increment_clock(&mut self, index: VectorIdx, current_span: Span) {
149        self.clock.increment_index(index, current_span);
150    }
151
152    /// Join the happens-before clock with that of
153    /// another thread, used to model thread join
154    /// operations.
155    fn join_with(&mut self, other: &ThreadClockSet) {
156        self.clock.join(&other.clock);
157    }
158}
159
160/// Error returned by finding a data race
161/// should be elaborated upon.
162#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
163pub struct DataRace;
164
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, Debug)]
170struct 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.
175    read_vector: VClock,
176
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,
182
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.
187    ///
188    /// With weak memory emulation, this is the clock of the most recent write. It is then only used
189    /// for release sequences, to integrate the most recent clock into the next one for RMWs.
190    sync_vector: VClock,
191
192    /// The size of accesses to this atomic location.
193    /// We use this to detect non-synchronized mixed-size accesses. Since all accesses must be
194    /// aligned to their size, this is sufficient to detect imperfectly overlapping accesses.
195    /// `None` indicates that we saw multiple different sizes, which is okay as long as all accesses are reads.
196    size: Option<Size>,
197}
198
199#[derive(Copy, Clone, PartialEq, Eq, Debug)]
200enum AtomicAccessType {
201    Load(AtomicReadOrd),
202    Store,
203    Rmw,
204}
205
206/// Type of a non-atomic read operation.
207#[derive(Copy, Clone, PartialEq, Eq, Debug)]
208pub enum NaReadType {
209    /// Standard unsynchronized write.
210    Read,
211
212    // An implicit read generated by a retag.
213    Retag,
214}
215
216impl NaReadType {
217    fn description(self) -> &'static str {
218        match self {
219            NaReadType::Read => "non-atomic read",
220            NaReadType::Retag => "retag read",
221        }
222    }
223}
224
225/// Type of a non-atomic write operation: allocating memory, non-atomic writes, and
226/// deallocating memory are all treated as writes for the purpose of the data-race detector.
227#[derive(Copy, Clone, PartialEq, Eq, Debug)]
228pub enum NaWriteType {
229    /// Allocate memory.
230    Allocate,
231
232    /// Standard unsynchronized write.
233    Write,
234
235    // An implicit write generated by a retag.
236    Retag,
237
238    /// Deallocate memory.
239    /// Note that when memory is deallocated first, later non-atomic accesses
240    /// will be reported as use-after-free, not as data races.
241    /// (Same for `Allocate` above.)
242    Deallocate,
243}
244
245impl NaWriteType {
246    fn description(self) -> &'static str {
247        match self {
248            NaWriteType::Allocate => "creating a new allocation",
249            NaWriteType::Write => "non-atomic write",
250            NaWriteType::Retag => "retag write",
251            NaWriteType::Deallocate => "deallocation",
252        }
253    }
254}
255
256#[derive(Copy, Clone, PartialEq, Eq, Debug)]
257enum AccessType {
258    NaRead(NaReadType),
259    NaWrite(NaWriteType),
260    AtomicLoad,
261    AtomicStore,
262    AtomicRmw,
263}
264
265/// Per-byte vector clock metadata for data-race detection.
266#[derive(Clone, PartialEq, Eq, Debug)]
267struct MemoryCellClocks {
268    /// The vector clock timestamp and the thread that did the last non-atomic write. We don't need
269    /// a full `VClock` here, it's always a single thread and nothing synchronizes, so the effective
270    /// clock is all-0 except for the thread that did the write.
271    write: (VectorIdx, VTimestamp),
272
273    /// The type of operation that the write index represents,
274    /// either newly allocated memory, a non-atomic write or
275    /// a deallocation of memory.
276    write_type: NaWriteType,
277
278    /// The vector clock of all non-atomic reads that happened since the last non-atomic write
279    /// (i.e., we join together the "singleton" clocks corresponding to each read). It is reset to
280    /// zero on each write operation.
281    read: VClock,
282
283    /// Atomic access tracking clocks.
284    /// For non-atomic memory this value is set to None.
285    /// For atomic memory, each byte carries this information.
286    atomic_ops: Option<Box<AtomicMemoryCellClocks>>,
287}
288
289/// Extra metadata associated with a thread.
290#[derive(Debug, Clone, Default)]
291struct ThreadExtraState {
292    /// The current vector index in use by the
293    /// thread currently, this is set to None
294    /// after the vector index has been re-used
295    /// and hence the value will never need to be
296    /// read during data-race reporting.
297    vector_index: Option<VectorIdx>,
298
299    /// Thread termination vector clock, this
300    /// is set on thread termination and is used
301    /// for joining on threads since the vector_index
302    /// may be re-used when the join operation occurs.
303    termination_vector_clock: Option<VClock>,
304}
305
306/// Global data-race detection state, contains the currently
307/// executing thread as well as the vector clocks associated
308/// with each of the threads.
309// FIXME: it is probably better to have one large RefCell, than to have so many small ones.
310#[derive(Debug, Clone)]
311pub struct GlobalState {
312    /// Set to true once the first additional
313    /// thread has launched, due to the dependency
314    /// between before and after a thread launch.
315    /// Any data-races must be recorded after this
316    /// so concurrent execution can ignore recording
317    /// any data-races.
318    multi_threaded: Cell<bool>,
319
320    /// A flag to mark we are currently performing
321    /// a data race free action (such as atomic access)
322    /// to suppress the race detector
323    ongoing_action_data_race_free: Cell<bool>,
324
325    /// Mapping of a vector index to a known set of thread
326    /// clocks, this is not directly mapping from a thread id
327    /// since it may refer to multiple threads.
328    vector_clocks: RefCell<IndexVec<VectorIdx, ThreadClockSet>>,
329
330    /// Mapping of a given vector index to the current thread
331    /// that the execution is representing, this may change
332    /// if a vector index is re-assigned to a new thread.
333    vector_info: RefCell<IndexVec<VectorIdx, ThreadId>>,
334
335    /// The mapping of a given thread to associated thread metadata.
336    thread_info: RefCell<IndexVec<ThreadId, ThreadExtraState>>,
337
338    /// Potential vector indices that could be re-used on thread creation
339    /// values are inserted here on after the thread has terminated and
340    /// been joined with, and hence may potentially become free
341    /// for use as the index for a new thread.
342    /// Elements in this set may still require the vector index to
343    /// report data-races, and can only be re-used after all
344    /// active vector clocks catch up with the threads timestamp.
345    reuse_candidates: RefCell<FxHashSet<VectorIdx>>,
346
347    /// We make SC fences act like RMWs on a global location.
348    /// To implement that, they all release and acquire into this clock.
349    last_sc_fence: RefCell<VClock>,
350
351    /// The timestamp of last SC write performed by each thread.
352    /// Threads only update their own index here!
353    last_sc_write_per_thread: RefCell<VClock>,
354
355    /// Track when an outdated (weak memory) load happens.
356    pub track_outdated_loads: bool,
357
358    /// Whether weak memory emulation is enabled
359    pub weak_memory: bool,
360}
361
362impl VisitProvenance for GlobalState {
363    fn visit_provenance(&self, _visit: &mut VisitWith<'_>) {
364        // We don't have any tags.
365    }
366}
367
368impl AccessType {
369    fn description(self, ty: Option<Ty<'_>>, size: Option<Size>) -> String {
370        let mut msg = String::new();
371
372        if let Some(size) = size {
373            if size == Size::ZERO {
374                // In this case there were multiple read accesss with different sizes and then a write.
375                // We will be reporting *one* of the other reads, but we don't have enough information
376                // to determine which one had which size.
377                assert!(self == AccessType::AtomicLoad);
378                assert!(ty.is_none());
379                return format!("multiple differently-sized atomic loads, including one load");
380            }
381            msg.push_str(&format!("{}-byte {}", size.bytes(), msg))
382        }
383
384        msg.push_str(match self {
385            AccessType::NaRead(w) => w.description(),
386            AccessType::NaWrite(w) => w.description(),
387            AccessType::AtomicLoad => "atomic load",
388            AccessType::AtomicStore => "atomic store",
389            AccessType::AtomicRmw => "atomic read-modify-write",
390        });
391
392        if let Some(ty) = ty {
393            msg.push_str(&format!(" of type `{ty}`"));
394        }
395
396        msg
397    }
398
399    fn is_atomic(self) -> bool {
400        match self {
401            AccessType::AtomicLoad | AccessType::AtomicStore | AccessType::AtomicRmw => true,
402            AccessType::NaRead(_) | AccessType::NaWrite(_) => false,
403        }
404    }
405
406    fn is_read(self) -> bool {
407        match self {
408            AccessType::AtomicLoad | AccessType::NaRead(_) => true,
409            AccessType::NaWrite(_) | AccessType::AtomicStore | AccessType::AtomicRmw => false,
410        }
411    }
412
413    fn is_retag(self) -> bool {
414        matches!(
415            self,
416            AccessType::NaRead(NaReadType::Retag) | AccessType::NaWrite(NaWriteType::Retag)
417        )
418    }
419}
420
421impl AtomicMemoryCellClocks {
422    fn new(size: Size) -> Self {
423        AtomicMemoryCellClocks {
424            read_vector: Default::default(),
425            write_vector: Default::default(),
426            sync_vector: Default::default(),
427            size: Some(size),
428        }
429    }
430}
431
432impl MemoryCellClocks {
433    /// Create a new set of clocks representing memory allocated
434    ///  at a given vector timestamp and index.
435    fn new(alloc: VTimestamp, alloc_index: VectorIdx) -> Self {
436        MemoryCellClocks {
437            read: VClock::default(),
438            write: (alloc_index, alloc),
439            write_type: NaWriteType::Allocate,
440            atomic_ops: None,
441        }
442    }
443
444    #[inline]
445    fn write_was_before(&self, other: &VClock) -> bool {
446        // This is the same as `self.write() <= other` but
447        // without actually manifesting a clock for `self.write`.
448        self.write.1 <= other[self.write.0]
449    }
450
451    #[inline]
452    fn write(&self) -> VClock {
453        VClock::new_with_index(self.write.0, self.write.1)
454    }
455
456    /// Load the internal atomic memory cells if they exist.
457    #[inline]
458    fn atomic(&self) -> Option<&AtomicMemoryCellClocks> {
459        self.atomic_ops.as_deref()
460    }
461
462    /// Load the internal atomic memory cells if they exist.
463    #[inline]
464    fn atomic_mut_unwrap(&mut self) -> &mut AtomicMemoryCellClocks {
465        self.atomic_ops.as_deref_mut().unwrap()
466    }
467
468    /// Load or create the internal atomic memory metadata if it does not exist. Also ensures we do
469    /// not do mixed-size atomic accesses, and updates the recorded atomic access size.
470    fn atomic_access(
471        &mut self,
472        thread_clocks: &ThreadClockSet,
473        size: Size,
474        write: bool,
475    ) -> Result<&mut AtomicMemoryCellClocks, DataRace> {
476        match self.atomic_ops {
477            Some(ref mut atomic) => {
478                // We are good if the size is the same or all atomic accesses are before our current time.
479                if atomic.size == Some(size) {
480                    Ok(atomic)
481                } else if atomic.read_vector <= thread_clocks.clock
482                    && atomic.write_vector <= thread_clocks.clock
483                {
484                    // We are fully ordered after all previous accesses, so we can change the size.
485                    atomic.size = Some(size);
486                    Ok(atomic)
487                } else if !write && atomic.write_vector <= thread_clocks.clock {
488                    // This is a read, and it is ordered after the last write. It's okay for the
489                    // sizes to mismatch, as long as no writes with a different size occur later.
490                    atomic.size = None;
491                    Ok(atomic)
492                } else {
493                    Err(DataRace)
494                }
495            }
496            None => {
497                self.atomic_ops = Some(Box::new(AtomicMemoryCellClocks::new(size)));
498                Ok(self.atomic_ops.as_mut().unwrap())
499            }
500        }
501    }
502
503    /// Update memory cell data-race tracking for atomic
504    /// load acquire semantics, is a no-op if this memory was
505    /// not used previously as atomic memory.
506    fn load_acquire(
507        &mut self,
508        thread_clocks: &mut ThreadClockSet,
509        index: VectorIdx,
510        access_size: Size,
511        sync_clock: Option<&VClock>,
512    ) -> Result<(), DataRace> {
513        self.atomic_read_detect(thread_clocks, index, access_size)?;
514        if let Some(sync_clock) = sync_clock.or_else(|| self.atomic().map(|a| &a.sync_vector)) {
515            thread_clocks.clock.join(sync_clock);
516        }
517        Ok(())
518    }
519
520    /// Update memory cell data-race tracking for atomic
521    /// load relaxed semantics, is a no-op if this memory was
522    /// not used previously as atomic memory.
523    fn load_relaxed(
524        &mut self,
525        thread_clocks: &mut ThreadClockSet,
526        index: VectorIdx,
527        access_size: Size,
528        sync_clock: Option<&VClock>,
529    ) -> Result<(), DataRace> {
530        self.atomic_read_detect(thread_clocks, index, access_size)?;
531        if let Some(sync_clock) = sync_clock.or_else(|| self.atomic().map(|a| &a.sync_vector)) {
532            thread_clocks.fence_acquire.join(sync_clock);
533        }
534        Ok(())
535    }
536
537    /// Update the memory cell data-race tracking for atomic
538    /// store release semantics.
539    fn store_release(
540        &mut self,
541        thread_clocks: &ThreadClockSet,
542        index: VectorIdx,
543        access_size: Size,
544    ) -> Result<(), DataRace> {
545        self.atomic_write_detect(thread_clocks, index, access_size)?;
546        let atomic = self.atomic_mut_unwrap(); // initialized by `atomic_write_detect`
547        atomic.sync_vector.clone_from(&thread_clocks.clock);
548        Ok(())
549    }
550
551    /// Update the memory cell data-race tracking for atomic
552    /// store relaxed semantics.
553    fn store_relaxed(
554        &mut self,
555        thread_clocks: &ThreadClockSet,
556        index: VectorIdx,
557        access_size: Size,
558    ) -> Result<(), DataRace> {
559        self.atomic_write_detect(thread_clocks, index, access_size)?;
560
561        // The handling of release sequences was changed in C++20 and so
562        // the code here is different to the paper since now all relaxed
563        // stores block release sequences. The exception for same-thread
564        // relaxed stores has been removed. We always overwrite the `sync_vector`,
565        // meaning the previous release sequence is broken.
566        let atomic = self.atomic_mut_unwrap();
567        atomic.sync_vector.clone_from(&thread_clocks.fence_release);
568        Ok(())
569    }
570
571    /// Update the memory cell data-race tracking for atomic
572    /// store release semantics for RMW operations.
573    fn rmw_release(
574        &mut self,
575        thread_clocks: &ThreadClockSet,
576        index: VectorIdx,
577        access_size: Size,
578    ) -> Result<(), DataRace> {
579        self.atomic_write_detect(thread_clocks, index, access_size)?;
580        let atomic = self.atomic_mut_unwrap();
581        // This *joining* of `sync_vector` implements release sequences: future
582        // reads of this location will acquire our clock *and* what was here before.
583        atomic.sync_vector.join(&thread_clocks.clock);
584        Ok(())
585    }
586
587    /// Update the memory cell data-race tracking for atomic
588    /// store relaxed semantics for RMW operations.
589    fn rmw_relaxed(
590        &mut self,
591        thread_clocks: &ThreadClockSet,
592        index: VectorIdx,
593        access_size: Size,
594    ) -> Result<(), DataRace> {
595        self.atomic_write_detect(thread_clocks, index, access_size)?;
596        let atomic = self.atomic_mut_unwrap();
597        // This *joining* of `sync_vector` implements release sequences: future
598        // reads of this location will acquire our fence clock *and* what was here before.
599        atomic.sync_vector.join(&thread_clocks.fence_release);
600        Ok(())
601    }
602
603    /// Detect data-races with an atomic read, caused by a non-atomic write that does
604    /// not happen-before the atomic-read.
605    fn atomic_read_detect(
606        &mut self,
607        thread_clocks: &ThreadClockSet,
608        index: VectorIdx,
609        access_size: Size,
610    ) -> Result<(), DataRace> {
611        trace!("Atomic read with vectors: {:#?} :: {:#?}", self, thread_clocks);
612        let atomic = self.atomic_access(thread_clocks, access_size, /*write*/ false)?;
613        atomic.read_vector.set_at_index(&thread_clocks.clock, index);
614        // Make sure the last non-atomic write was before this access.
615        if self.write_was_before(&thread_clocks.clock) { Ok(()) } else { Err(DataRace) }
616    }
617
618    /// Detect data-races with an atomic write, either with a non-atomic read or with
619    /// a non-atomic write.
620    fn atomic_write_detect(
621        &mut self,
622        thread_clocks: &ThreadClockSet,
623        index: VectorIdx,
624        access_size: Size,
625    ) -> Result<(), DataRace> {
626        trace!("Atomic write with vectors: {:#?} :: {:#?}", self, thread_clocks);
627        let atomic = self.atomic_access(thread_clocks, access_size, /*write*/ true)?;
628        atomic.write_vector.set_at_index(&thread_clocks.clock, index);
629        // Make sure the last non-atomic write and all non-atomic reads were before this access.
630        if self.write_was_before(&thread_clocks.clock) && self.read <= thread_clocks.clock {
631            Ok(())
632        } else {
633            Err(DataRace)
634        }
635    }
636
637    /// Detect races for non-atomic read operations at the current memory cell
638    /// returns true if a data-race is detected.
639    fn read_race_detect(
640        &mut self,
641        thread_clocks: &mut ThreadClockSet,
642        index: VectorIdx,
643        read_type: NaReadType,
644        current_span: Span,
645    ) -> Result<(), DataRace> {
646        trace!("Unsynchronized read with vectors: {:#?} :: {:#?}", self, thread_clocks);
647        if !current_span.is_dummy() {
648            thread_clocks.clock.index_mut(index).span = current_span;
649        }
650        thread_clocks.clock.index_mut(index).set_read_type(read_type);
651        if self.write_was_before(&thread_clocks.clock) {
652            // We must be ordered-after all atomic writes.
653            let race_free = if let Some(atomic) = self.atomic() {
654                atomic.write_vector <= thread_clocks.clock
655            } else {
656                true
657            };
658            self.read.set_at_index(&thread_clocks.clock, index);
659            if race_free { Ok(()) } else { Err(DataRace) }
660        } else {
661            Err(DataRace)
662        }
663    }
664
665    /// Detect races for non-atomic write operations at the current memory cell
666    /// returns true if a data-race is detected.
667    fn write_race_detect(
668        &mut self,
669        thread_clocks: &mut ThreadClockSet,
670        index: VectorIdx,
671        write_type: NaWriteType,
672        current_span: Span,
673    ) -> Result<(), DataRace> {
674        trace!("Unsynchronized write with vectors: {:#?} :: {:#?}", self, thread_clocks);
675        if !current_span.is_dummy() {
676            thread_clocks.clock.index_mut(index).span = current_span;
677        }
678        if self.write_was_before(&thread_clocks.clock) && self.read <= thread_clocks.clock {
679            let race_free = if let Some(atomic) = self.atomic() {
680                atomic.write_vector <= thread_clocks.clock
681                    && atomic.read_vector <= thread_clocks.clock
682            } else {
683                true
684            };
685            self.write = (index, thread_clocks.clock[index]);
686            self.write_type = write_type;
687            if race_free {
688                self.read.set_zero_vector();
689                Ok(())
690            } else {
691                Err(DataRace)
692            }
693        } else {
694            Err(DataRace)
695        }
696    }
697}
698
699impl GlobalDataRaceHandler {
700    /// Select whether data race checking is disabled. This is solely an
701    /// implementation detail of `allow_data_races_*` and must not be used anywhere else!
702    fn set_ongoing_action_data_race_free(&self, enable: bool) {
703        match self {
704            GlobalDataRaceHandler::None => {}
705            GlobalDataRaceHandler::Vclocks(data_race) => {
706                let old = data_race.ongoing_action_data_race_free.replace(enable);
707                assert_ne!(old, enable, "cannot nest allow_data_races");
708            }
709            GlobalDataRaceHandler::Genmc(genmc_ctx) => {
710                genmc_ctx.set_ongoing_action_data_race_free(enable);
711            }
712        }
713    }
714}
715
716/// Evaluation context extensions.
717impl<'tcx> EvalContextExt<'tcx> for MiriInterpCx<'tcx> {}
718pub trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
719    /// Perform an atomic read operation at the memory location.
720    fn read_scalar_atomic(
721        &self,
722        place: &MPlaceTy<'tcx>,
723        atomic: AtomicReadOrd,
724    ) -> InterpResult<'tcx, Scalar> {
725        let this = self.eval_context_ref();
726        this.atomic_access_check(place, AtomicAccessType::Load(atomic))?;
727        // This will read from the last store in the modification order of this location. In case
728        // weak memory emulation is enabled, this may not be the store we will pick to actually read from and return.
729        // This is fine with StackedBorrow and race checks because they don't concern metadata on
730        // the *value* (including the associated provenance if this is an AtomicPtr) at this location.
731        // Only metadata on the location itself is used.
732
733        if let Some(genmc_ctx) = this.machine.data_race.as_genmc_ref() {
734            let old_val = this.run_for_validation_ref(|this| this.read_scalar(place)).discard_err();
735            return genmc_ctx.atomic_load(
736                this,
737                place.ptr().addr(),
738                place.layout.size,
739                atomic,
740                old_val,
741            );
742        }
743
744        let scalar = this.allow_data_races_ref(move |this| this.read_scalar(place))?;
745        let buffered_scalar = this.buffered_atomic_read(place, atomic, scalar, |sync_clock| {
746            this.validate_atomic_load(place, atomic, sync_clock)
747        })?;
748        interp_ok(buffered_scalar.ok_or_else(|| err_ub!(InvalidUninitBytes(None)))?)
749    }
750
751    /// Perform an atomic write operation at the memory location.
752    fn write_scalar_atomic(
753        &mut self,
754        val: Scalar,
755        dest: &MPlaceTy<'tcx>,
756        atomic: AtomicWriteOrd,
757    ) -> InterpResult<'tcx> {
758        let this = self.eval_context_mut();
759        this.atomic_access_check(dest, AtomicAccessType::Store)?;
760
761        // Read the previous value so we can put it in the store buffer later.
762        // The program didn't actually do a read, so suppress the memory access hooks.
763        // This is also a very special exception where we just ignore an error -- if this read
764        // was UB e.g. because the memory is uninitialized, we don't want to know!
765        let old_val = this.run_for_validation_ref(|this| this.read_scalar(dest)).discard_err();
766
767        // Inform GenMC about the atomic store.
768        if let Some(genmc_ctx) = this.machine.data_race.as_genmc_ref() {
769            if genmc_ctx.atomic_store(
770                this,
771                dest.ptr().addr(),
772                dest.layout.size,
773                val,
774                old_val,
775                atomic,
776            )? {
777                // The store might be the latest store in coherence order (determined by GenMC).
778                // If it is, we need to update the value in Miri's memory:
779                this.allow_data_races_mut(|this| this.write_scalar(val, dest))?;
780            }
781            return interp_ok(());
782        }
783        this.allow_data_races_mut(move |this| this.write_scalar(val, dest))?;
784        this.validate_atomic_store(dest, atomic)?;
785        this.buffered_atomic_write(val, dest, atomic, old_val)
786    }
787
788    /// Perform an atomic RMW operation on a memory location.
789    fn atomic_rmw_op_immediate(
790        &mut self,
791        place: &MPlaceTy<'tcx>,
792        rhs: &ImmTy<'tcx>,
793        atomic_op: AtomicRmwOp,
794        ord: AtomicRwOrd,
795    ) -> InterpResult<'tcx, ImmTy<'tcx>> {
796        let this = self.eval_context_mut();
797        this.atomic_access_check(place, AtomicAccessType::Rmw)?;
798
799        let old = this.allow_data_races_mut(|this| this.read_immediate(place))?;
800
801        // Inform GenMC about the atomic rmw operation.
802        if let Some(genmc_ctx) = this.machine.data_race.as_genmc_ref() {
803            let (old_val, new_val) = genmc_ctx.atomic_rmw_op(
804                this,
805                place.ptr().addr(),
806                place.layout.size,
807                atomic_op,
808                place.layout.backend_repr.is_signed(),
809                ord,
810                rhs.to_scalar(),
811                old.to_scalar(),
812            )?;
813            if let Some(new_val) = new_val {
814                this.allow_data_races_mut(|this| this.write_scalar(new_val, place))?;
815            }
816            return interp_ok(ImmTy::from_scalar(old_val, old.layout));
817        }
818
819        let val = match atomic_op {
820            AtomicRmwOp::MirOp { op, neg } => {
821                let val = this.binary_op(op, &old, rhs)?;
822                if neg { this.unary_op(mir::UnOp::Not, &val)? } else { val }
823            }
824            AtomicRmwOp::Max => {
825                let lt = this.binary_op(mir::BinOp::Lt, &old, rhs)?.to_scalar().to_bool()?;
826                if lt { rhs } else { &old }.clone()
827            }
828            AtomicRmwOp::Min => {
829                let lt = this.binary_op(mir::BinOp::Lt, &old, rhs)?.to_scalar().to_bool()?;
830                if lt { &old } else { rhs }.clone()
831            }
832        };
833
834        this.allow_data_races_mut(|this| this.write_immediate(*val, place))?;
835
836        this.validate_atomic_rmw(place, ord)?;
837
838        this.buffered_atomic_rmw(val.to_scalar(), place, ord, old.to_scalar())?;
839        interp_ok(old)
840    }
841
842    /// Perform an atomic exchange with a memory place and a new
843    /// scalar value, the old value is returned.
844    fn atomic_exchange_scalar(
845        &mut self,
846        place: &MPlaceTy<'tcx>,
847        new: Scalar,
848        atomic: AtomicRwOrd,
849    ) -> InterpResult<'tcx, Scalar> {
850        let this = self.eval_context_mut();
851        this.atomic_access_check(place, AtomicAccessType::Rmw)?;
852
853        let old = this.allow_data_races_mut(|this| this.read_scalar(place))?;
854        this.allow_data_races_mut(|this| this.write_scalar(new, place))?;
855
856        // Inform GenMC about the atomic atomic exchange.
857        if let Some(genmc_ctx) = this.machine.data_race.as_genmc_ref() {
858            let (old_val, new_val) = genmc_ctx.atomic_exchange(
859                this,
860                place.ptr().addr(),
861                place.layout.size,
862                new,
863                atomic,
864                old,
865            )?;
866            // The store might be the latest store in coherence order (determined by GenMC).
867            // If it is, we need to update the value in Miri's memory:
868            if let Some(new_val) = new_val {
869                this.allow_data_races_mut(|this| this.write_scalar(new_val, place))?;
870            }
871            return interp_ok(old_val);
872        }
873
874        this.validate_atomic_rmw(place, atomic)?;
875
876        this.buffered_atomic_rmw(new, place, atomic, old)?;
877        interp_ok(old)
878    }
879
880    /// Perform an atomic compare and exchange at a given memory location.
881    /// On success an atomic RMW operation is performed and on failure
882    /// only an atomic read occurs. If `can_fail_spuriously` is true,
883    /// then we treat it as a "compare_exchange_weak" operation, and
884    /// some portion of the time fail even when the values are actually
885    /// identical.
886    fn atomic_compare_exchange_scalar(
887        &mut self,
888        place: &MPlaceTy<'tcx>,
889        expect_old: &ImmTy<'tcx>,
890        new: Scalar,
891        success: AtomicRwOrd,
892        fail: AtomicReadOrd,
893        can_fail_spuriously: bool,
894    ) -> InterpResult<'tcx, Immediate<Provenance>> {
895        use rand::Rng as _;
896        let this = self.eval_context_mut();
897        this.atomic_access_check(place, AtomicAccessType::Rmw)?;
898
899        // Read as immediate for the sake of `binary_op()`
900        let old = this.allow_data_races_mut(|this| this.read_immediate(place))?;
901
902        // Inform GenMC about the atomic atomic compare exchange.
903        if let Some(genmc_ctx) = this.machine.data_race.as_genmc_ref() {
904            let (old_value, new_value, cmpxchg_success) = genmc_ctx.atomic_compare_exchange(
905                this,
906                place.ptr().addr(),
907                place.layout.size,
908                this.read_scalar(expect_old)?,
909                new,
910                success,
911                fail,
912                can_fail_spuriously,
913                old.to_scalar(),
914            )?;
915            // The store might be the latest store in coherence order (determined by GenMC).
916            // If it is, we need to update the value in Miri's memory:
917            if let Some(new_value) = new_value {
918                this.allow_data_races_mut(|this| this.write_scalar(new_value, place))?;
919            }
920            return interp_ok(Immediate::ScalarPair(old_value, Scalar::from_bool(cmpxchg_success)));
921        }
922
923        // `binary_op` will bail if either of them is not a scalar.
924        let eq = this.binary_op(mir::BinOp::Eq, &old, expect_old)?;
925        // If the operation would succeed, but is "weak", fail some portion
926        // of the time, based on `success_rate`.
927        let success_rate = 1.0 - this.machine.cmpxchg_weak_failure_rate;
928        let cmpxchg_success = eq.to_scalar().to_bool()?
929            && if can_fail_spuriously {
930                this.machine.rng.get_mut().random_bool(success_rate)
931            } else {
932                true
933            };
934        let res = Immediate::ScalarPair(old.to_scalar(), Scalar::from_bool(cmpxchg_success));
935
936        // Update ptr depending on comparison.
937        // if successful, perform a full rw-atomic validation
938        // otherwise treat this as an atomic load with the fail ordering.
939        if cmpxchg_success {
940            this.allow_data_races_mut(|this| this.write_scalar(new, place))?;
941            this.validate_atomic_rmw(place, success)?;
942            this.buffered_atomic_rmw(new, place, success, old.to_scalar())?;
943        } else {
944            this.validate_atomic_load(place, fail, /* can use latest sync clock */ None)?;
945            // A failed compare exchange is equivalent to a load, reading from the latest store
946            // in the modification order.
947            // Since `old` is only a value and not the store element, we need to separately
948            // find it in our store buffer and perform load_impl on it.
949            this.perform_read_on_buffered_latest(place, fail)?;
950        }
951
952        // Return the old value.
953        interp_ok(res)
954    }
955
956    /// Update the data-race detector for an atomic fence on the current thread.
957    fn atomic_fence(&mut self, atomic: AtomicFenceOrd) -> InterpResult<'tcx> {
958        let this = self.eval_context_mut();
959        let machine = &this.machine;
960        match &this.machine.data_race {
961            GlobalDataRaceHandler::None => interp_ok(()),
962            GlobalDataRaceHandler::Vclocks(data_race) => data_race.atomic_fence(machine, atomic),
963            GlobalDataRaceHandler::Genmc(genmc_ctx) => genmc_ctx.atomic_fence(machine, atomic),
964        }
965    }
966
967    /// Calls the callback with the "release" clock of the current thread.
968    /// Other threads can acquire this clock in the future to establish synchronization
969    /// with this program point.
970    ///
971    /// The closure will only be invoked if data race handling is on.
972    fn release_clock<R>(
973        &self,
974        callback: impl FnOnce(&VClock) -> R,
975    ) -> InterpResult<'tcx, Option<R>> {
976        let this = self.eval_context_ref();
977        interp_ok(match &this.machine.data_race {
978            GlobalDataRaceHandler::None => None,
979            GlobalDataRaceHandler::Genmc(_genmc_ctx) =>
980                throw_unsup_format!(
981                    "this operation performs synchronization that is not supported in GenMC mode"
982                ),
983            GlobalDataRaceHandler::Vclocks(data_race) =>
984                Some(data_race.release_clock(&this.machine.threads, callback)),
985        })
986    }
987
988    /// Acquire the given clock into the current thread, establishing synchronization with
989    /// the moment when that clock snapshot was taken via `release_clock`.
990    fn acquire_clock(&self, clock: &VClock) -> InterpResult<'tcx> {
991        let this = self.eval_context_ref();
992        match &this.machine.data_race {
993            GlobalDataRaceHandler::None => {}
994            GlobalDataRaceHandler::Genmc(_genmc_ctx) =>
995                throw_unsup_format!(
996                    "this operation performs synchronization that is not supported in GenMC mode"
997                ),
998            GlobalDataRaceHandler::Vclocks(data_race) =>
999                data_race.acquire_clock(clock, &this.machine.threads),
1000        }
1001        interp_ok(())
1002    }
1003}
1004
1005/// Vector clock metadata for a logical memory allocation.
1006#[derive(Debug, Clone)]
1007pub struct VClockAlloc {
1008    /// Assigning each byte a MemoryCellClocks.
1009    alloc_ranges: RefCell<DedupRangeMap<MemoryCellClocks>>,
1010}
1011
1012impl VisitProvenance for VClockAlloc {
1013    fn visit_provenance(&self, _visit: &mut VisitWith<'_>) {
1014        // No tags or allocIds here.
1015    }
1016}
1017
1018impl VClockAlloc {
1019    /// Create a new data-race detector for newly allocated memory.
1020    pub fn new_allocation(
1021        global: &GlobalState,
1022        thread_mgr: &ThreadManager<'_>,
1023        len: Size,
1024        kind: MemoryKind,
1025        current_span: Span,
1026    ) -> VClockAlloc {
1027        // Determine the thread that did the allocation, and when it did it.
1028        let (alloc_timestamp, alloc_index) = match kind {
1029            // User allocated and stack memory should track allocation.
1030            MemoryKind::Machine(
1031                MiriMemoryKind::Rust
1032                | MiriMemoryKind::Miri
1033                | MiriMemoryKind::C
1034                | MiriMemoryKind::WinHeap
1035                | MiriMemoryKind::WinLocal
1036                | MiriMemoryKind::Mmap,
1037            )
1038            | MemoryKind::Stack => {
1039                let (alloc_index, clocks) = global.active_thread_state(thread_mgr);
1040                let mut alloc_timestamp = clocks.clock[alloc_index];
1041                alloc_timestamp.span = current_span;
1042                (alloc_timestamp, alloc_index)
1043            }
1044            // Other global memory should trace races but be allocated at the 0 timestamp
1045            // (conceptually they are allocated on the main thread before everything).
1046            MemoryKind::Machine(
1047                MiriMemoryKind::Global
1048                | MiriMemoryKind::Machine
1049                | MiriMemoryKind::Runtime
1050                | MiriMemoryKind::ExternStatic
1051                | MiriMemoryKind::Tls,
1052            )
1053            | MemoryKind::CallerLocation =>
1054                (VTimestamp::ZERO, global.thread_index(ThreadId::MAIN_THREAD)),
1055        };
1056        VClockAlloc {
1057            alloc_ranges: RefCell::new(DedupRangeMap::new(
1058                len,
1059                MemoryCellClocks::new(alloc_timestamp, alloc_index),
1060            )),
1061        }
1062    }
1063
1064    // Find an index, if one exists where the value
1065    // in `l` is greater than the value in `r`.
1066    fn find_gt_index(l: &VClock, r: &VClock) -> Option<VectorIdx> {
1067        trace!("Find index where not {:?} <= {:?}", l, r);
1068        let l_slice = l.as_slice();
1069        let r_slice = r.as_slice();
1070        l_slice
1071            .iter()
1072            .zip(r_slice.iter())
1073            .enumerate()
1074            .find_map(|(idx, (&l, &r))| if l > r { Some(idx) } else { None })
1075            .or_else(|| {
1076                if l_slice.len() > r_slice.len() {
1077                    // By invariant, if l_slice is longer
1078                    // then one element must be larger.
1079                    // This just validates that this is true
1080                    // and reports earlier elements first.
1081                    let l_remainder_slice = &l_slice[r_slice.len()..];
1082                    let idx = l_remainder_slice
1083                        .iter()
1084                        .enumerate()
1085                        .find_map(|(idx, &r)| if r == VTimestamp::ZERO { None } else { Some(idx) })
1086                        .expect("Invalid VClock Invariant");
1087                    Some(idx + r_slice.len())
1088                } else {
1089                    None
1090                }
1091            })
1092            .map(VectorIdx::new)
1093    }
1094
1095    /// Report a data-race found in the program.
1096    /// This finds the two racing threads and the type
1097    /// of data-race that occurred. This will also
1098    /// return info about the memory location the data-race
1099    /// occurred in. The `ty` parameter is used for diagnostics, letting
1100    /// the user know which type was involved in the access.
1101    #[cold]
1102    #[inline(never)]
1103    fn report_data_race<'tcx>(
1104        global: &GlobalState,
1105        thread_mgr: &ThreadManager<'_>,
1106        mem_clocks: &MemoryCellClocks,
1107        access: AccessType,
1108        access_size: Size,
1109        ptr_dbg: interpret::Pointer<AllocId>,
1110        ty: Option<Ty<'_>>,
1111    ) -> InterpResult<'tcx> {
1112        let (active_index, active_clocks) = global.active_thread_state(thread_mgr);
1113        let mut other_size = None; // if `Some`, this was a size-mismatch race
1114        let write_clock;
1115        let (other_access, other_thread, other_clock) =
1116            // First check the atomic-nonatomic cases.
1117            if !access.is_atomic() &&
1118                let Some(atomic) = mem_clocks.atomic() &&
1119                let Some(idx) = Self::find_gt_index(&atomic.write_vector, &active_clocks.clock)
1120            {
1121                (AccessType::AtomicStore, idx, &atomic.write_vector)
1122            } else if !access.is_atomic() &&
1123                let Some(atomic) = mem_clocks.atomic() &&
1124                let Some(idx) = Self::find_gt_index(&atomic.read_vector, &active_clocks.clock)
1125            {
1126                (AccessType::AtomicLoad, idx, &atomic.read_vector)
1127            // Then check races with non-atomic writes/reads.
1128            } else if mem_clocks.write.1 > active_clocks.clock[mem_clocks.write.0] {
1129                write_clock = mem_clocks.write();
1130                (AccessType::NaWrite(mem_clocks.write_type), mem_clocks.write.0, &write_clock)
1131            } else if let Some(idx) = Self::find_gt_index(&mem_clocks.read, &active_clocks.clock) {
1132                (AccessType::NaRead(mem_clocks.read[idx].read_type()), idx, &mem_clocks.read)
1133            // Finally, mixed-size races.
1134            } else if access.is_atomic() && let Some(atomic) = mem_clocks.atomic() && atomic.size != Some(access_size) {
1135                // This is only a race if we are not synchronized with all atomic accesses, so find
1136                // the one we are not synchronized with.
1137                other_size = Some(atomic.size.unwrap_or(Size::ZERO));
1138                if let Some(idx) = Self::find_gt_index(&atomic.write_vector, &active_clocks.clock)
1139                    {
1140                        (AccessType::AtomicStore, idx, &atomic.write_vector)
1141                    } else if let Some(idx) =
1142                        Self::find_gt_index(&atomic.read_vector, &active_clocks.clock)
1143                    {
1144                        (AccessType::AtomicLoad, idx, &atomic.read_vector)
1145                    } else {
1146                        unreachable!(
1147                            "Failed to report data-race for mixed-size access: no race found"
1148                        )
1149                    }
1150            } else {
1151                unreachable!("Failed to report data-race")
1152            };
1153
1154        // Load elaborated thread information about the racing thread actions.
1155        let active_thread_info = global.print_thread_metadata(thread_mgr, active_index);
1156        let other_thread_info = global.print_thread_metadata(thread_mgr, other_thread);
1157        let involves_non_atomic = !access.is_atomic() || !other_access.is_atomic();
1158
1159        // Throw the data-race detection.
1160        let extra = if other_size.is_some() {
1161            assert!(!involves_non_atomic);
1162            Some("overlapping unsynchronized atomic accesses must use the same access size")
1163        } else if access.is_read() && other_access.is_read() {
1164            panic!("there should be no same-size read-read races")
1165        } else {
1166            None
1167        };
1168        Err(err_machine_stop!(TerminationInfo::DataRace {
1169            involves_non_atomic,
1170            extra,
1171            retag_explain: access.is_retag() || other_access.is_retag(),
1172            ptr: ptr_dbg,
1173            op1: RacingOp {
1174                action: other_access.description(None, other_size),
1175                thread_info: other_thread_info,
1176                span: other_clock.as_slice()[other_thread.index()].span_data(),
1177            },
1178            op2: RacingOp {
1179                action: access.description(ty, other_size.map(|_| access_size)),
1180                thread_info: active_thread_info,
1181                span: active_clocks.clock.as_slice()[active_index.index()].span_data(),
1182            },
1183        }))?
1184    }
1185
1186    /// Return the release/acquire synchronization clock for the given memory range.
1187    pub(super) fn sync_clock(&self, access_range: AllocRange) -> VClock {
1188        let alloc_ranges = self.alloc_ranges.borrow();
1189        let mut clock = VClock::default();
1190        for (_, mem_clocks) in alloc_ranges.iter(access_range.start, access_range.size) {
1191            if let Some(atomic) = mem_clocks.atomic() {
1192                clock.join(&atomic.sync_vector);
1193            }
1194        }
1195        clock
1196    }
1197
1198    /// Detect data-races for an unsynchronized read operation. It will not perform
1199    /// data-race detection if `race_detecting()` is false, either due to no threads
1200    /// being created or if it is temporarily disabled during a racy read or write
1201    /// operation for which data-race detection is handled separately, for example
1202    /// atomic read operations. The `ty` parameter is used for diagnostics, letting
1203    /// the user know which type was read.
1204    pub fn read<'tcx>(
1205        &self,
1206        alloc_id: AllocId,
1207        access_range: AllocRange,
1208        read_type: NaReadType,
1209        ty: Option<Ty<'_>>,
1210        machine: &MiriMachine<'_>,
1211    ) -> InterpResult<'tcx> {
1212        let current_span = machine.current_user_relevant_span();
1213        let global = machine.data_race.as_vclocks_ref().unwrap();
1214        if !global.race_detecting() {
1215            return interp_ok(());
1216        }
1217        let (index, mut thread_clocks) = global.active_thread_state_mut(&machine.threads);
1218        let mut alloc_ranges = self.alloc_ranges.borrow_mut();
1219        for (mem_clocks_range, mem_clocks) in
1220            alloc_ranges.iter_mut(access_range.start, access_range.size)
1221        {
1222            if let Err(DataRace) =
1223                mem_clocks.read_race_detect(&mut thread_clocks, index, read_type, current_span)
1224            {
1225                drop(thread_clocks);
1226                // Report data-race.
1227                return Self::report_data_race(
1228                    global,
1229                    &machine.threads,
1230                    mem_clocks,
1231                    AccessType::NaRead(read_type),
1232                    access_range.size,
1233                    interpret::Pointer::new(alloc_id, Size::from_bytes(mem_clocks_range.start)),
1234                    ty,
1235                );
1236            }
1237        }
1238        interp_ok(())
1239    }
1240
1241    /// Detect data-races for an unsynchronized write operation. It will not perform
1242    /// data-race detection if `race_detecting()` is false, either due to no threads
1243    /// being created or if it is temporarily disabled during a racy read or write
1244    /// operation. The `ty` parameter is used for diagnostics, letting
1245    /// the user know which type was written.
1246    pub fn write<'tcx>(
1247        &mut self,
1248        alloc_id: AllocId,
1249        access_range: AllocRange,
1250        write_type: NaWriteType,
1251        ty: Option<Ty<'_>>,
1252        machine: &mut MiriMachine<'_>,
1253    ) -> InterpResult<'tcx> {
1254        let current_span = machine.current_user_relevant_span();
1255        let global = machine.data_race.as_vclocks_mut().unwrap();
1256        if !global.race_detecting() {
1257            return interp_ok(());
1258        }
1259        let (index, mut thread_clocks) = global.active_thread_state_mut(&machine.threads);
1260        for (mem_clocks_range, mem_clocks) in
1261            self.alloc_ranges.get_mut().iter_mut(access_range.start, access_range.size)
1262        {
1263            if let Err(DataRace) =
1264                mem_clocks.write_race_detect(&mut thread_clocks, index, write_type, current_span)
1265            {
1266                drop(thread_clocks);
1267                // Report data-race
1268                return Self::report_data_race(
1269                    global,
1270                    &machine.threads,
1271                    mem_clocks,
1272                    AccessType::NaWrite(write_type),
1273                    access_range.size,
1274                    interpret::Pointer::new(alloc_id, Size::from_bytes(mem_clocks_range.start)),
1275                    ty,
1276                );
1277            }
1278        }
1279        interp_ok(())
1280    }
1281}
1282
1283/// Vector clock state for a stack frame (tracking the local variables
1284/// that do not have an allocation yet).
1285#[derive(Debug, Default)]
1286pub struct FrameState {
1287    local_clocks: RefCell<FxHashMap<mir::Local, LocalClocks>>,
1288}
1289
1290/// Stripped-down version of [`MemoryCellClocks`] for the clocks we need to keep track
1291/// of in a local that does not yet have addressable memory -- and hence can only
1292/// be accessed from the thread its stack frame belongs to, and cannot be access atomically.
1293#[derive(Debug)]
1294struct LocalClocks {
1295    write: VTimestamp,
1296    write_type: NaWriteType,
1297    read: VTimestamp,
1298}
1299
1300impl Default for LocalClocks {
1301    fn default() -> Self {
1302        Self { write: VTimestamp::ZERO, write_type: NaWriteType::Allocate, read: VTimestamp::ZERO }
1303    }
1304}
1305
1306impl FrameState {
1307    pub fn local_write(&self, local: mir::Local, storage_live: bool, machine: &MiriMachine<'_>) {
1308        let current_span = machine.current_user_relevant_span();
1309        let global = machine.data_race.as_vclocks_ref().unwrap();
1310        if !global.race_detecting() {
1311            return;
1312        }
1313        let (index, mut thread_clocks) = global.active_thread_state_mut(&machine.threads);
1314        // This should do the same things as `MemoryCellClocks::write_race_detect`.
1315        if !current_span.is_dummy() {
1316            thread_clocks.clock.index_mut(index).span = current_span;
1317        }
1318        let mut clocks = self.local_clocks.borrow_mut();
1319        if storage_live {
1320            let new_clocks = LocalClocks {
1321                write: thread_clocks.clock[index],
1322                write_type: NaWriteType::Allocate,
1323                read: VTimestamp::ZERO,
1324            };
1325            // There might already be an entry in the map for this, if the local was previously
1326            // live already.
1327            clocks.insert(local, new_clocks);
1328        } else {
1329            // This can fail to exist if `race_detecting` was false when the allocation
1330            // occurred, in which case we can backdate this to the beginning of time.
1331            let clocks = clocks.entry(local).or_default();
1332            clocks.write = thread_clocks.clock[index];
1333            clocks.write_type = NaWriteType::Write;
1334        }
1335    }
1336
1337    pub fn local_read(&self, local: mir::Local, machine: &MiriMachine<'_>) {
1338        let current_span = machine.current_user_relevant_span();
1339        let global = machine.data_race.as_vclocks_ref().unwrap();
1340        if !global.race_detecting() {
1341            return;
1342        }
1343        let (index, mut thread_clocks) = global.active_thread_state_mut(&machine.threads);
1344        // This should do the same things as `MemoryCellClocks::read_race_detect`.
1345        if !current_span.is_dummy() {
1346            thread_clocks.clock.index_mut(index).span = current_span;
1347        }
1348        thread_clocks.clock.index_mut(index).set_read_type(NaReadType::Read);
1349        // This can fail to exist if `race_detecting` was false when the allocation
1350        // occurred, in which case we can backdate this to the beginning of time.
1351        let mut clocks = self.local_clocks.borrow_mut();
1352        let clocks = clocks.entry(local).or_default();
1353        clocks.read = thread_clocks.clock[index];
1354    }
1355
1356    pub fn local_moved_to_memory(
1357        &self,
1358        local: mir::Local,
1359        alloc: &mut VClockAlloc,
1360        machine: &MiriMachine<'_>,
1361    ) {
1362        let global = machine.data_race.as_vclocks_ref().unwrap();
1363        if !global.race_detecting() {
1364            return;
1365        }
1366        let (index, _thread_clocks) = global.active_thread_state_mut(&machine.threads);
1367        // Get the time the last write actually happened. This can fail to exist if
1368        // `race_detecting` was false when the write occurred, in that case we can backdate this
1369        // to the beginning of time.
1370        let local_clocks = self.local_clocks.borrow_mut().remove(&local).unwrap_or_default();
1371        for (_mem_clocks_range, mem_clocks) in alloc.alloc_ranges.get_mut().iter_mut_all() {
1372            // The initialization write for this already happened, just at the wrong timestamp.
1373            // Check that the thread index matches what we expect.
1374            assert_eq!(mem_clocks.write.0, index);
1375            // Convert the local's clocks into memory clocks.
1376            mem_clocks.write = (index, local_clocks.write);
1377            mem_clocks.write_type = local_clocks.write_type;
1378            mem_clocks.read = VClock::new_with_index(index, local_clocks.read);
1379        }
1380    }
1381}
1382
1383impl<'tcx> EvalContextPrivExt<'tcx> for MiriInterpCx<'tcx> {}
1384trait EvalContextPrivExt<'tcx>: MiriInterpCxExt<'tcx> {
1385    /// Temporarily allow data-races to occur. This should only be used in
1386    /// one of these cases:
1387    /// - One of the appropriate `validate_atomic` functions will be called to
1388    ///   treat a memory access as atomic.
1389    /// - The memory being accessed should be treated as internal state, that
1390    ///   cannot be accessed by the interpreted program.
1391    /// - Execution of the interpreted program execution has halted.
1392    #[inline]
1393    fn allow_data_races_ref<R>(&self, op: impl FnOnce(&MiriInterpCx<'tcx>) -> R) -> R {
1394        let this = self.eval_context_ref();
1395        this.machine.data_race.set_ongoing_action_data_race_free(true);
1396        let result = op(this);
1397        this.machine.data_race.set_ongoing_action_data_race_free(false);
1398        result
1399    }
1400
1401    /// Same as `allow_data_races_ref`, this temporarily disables any data-race detection and
1402    /// so should only be used for atomic operations or internal state that the program cannot
1403    /// access.
1404    #[inline]
1405    fn allow_data_races_mut<R>(&mut self, op: impl FnOnce(&mut MiriInterpCx<'tcx>) -> R) -> R {
1406        let this = self.eval_context_mut();
1407        this.machine.data_race.set_ongoing_action_data_race_free(true);
1408        let result = op(this);
1409        this.machine.data_race.set_ongoing_action_data_race_free(false);
1410        result
1411    }
1412
1413    /// Checks that an atomic access is legal at the given place.
1414    fn atomic_access_check(
1415        &self,
1416        place: &MPlaceTy<'tcx>,
1417        access_type: AtomicAccessType,
1418    ) -> InterpResult<'tcx> {
1419        let this = self.eval_context_ref();
1420        // Check alignment requirements. Atomics must always be aligned to their size,
1421        // even if the type they wrap would be less aligned (e.g. AtomicU64 on 32bit must
1422        // be 8-aligned).
1423        let align = Align::from_bytes(place.layout.size.bytes()).unwrap();
1424        this.check_ptr_align(place.ptr(), align)?;
1425        // Ensure the allocation is mutable. Even failing (read-only) compare_exchange need mutable
1426        // memory on many targets (i.e., they segfault if that memory is mapped read-only), and
1427        // atomic loads can be implemented via compare_exchange on some targets. There could
1428        // possibly be some very specific exceptions to this, see
1429        // <https://github.com/rust-lang/miri/pull/2464#discussion_r939636130> for details.
1430        // We avoid `get_ptr_alloc` since we do *not* want to run the access hooks -- the actual
1431        // access will happen later.
1432        let (alloc_id, _offset, _prov) = this
1433            .ptr_try_get_alloc_id(place.ptr(), 0)
1434            .expect("there are no zero-sized atomic accesses");
1435        if this.get_alloc_mutability(alloc_id)? == Mutability::Not {
1436            // See if this is fine.
1437            match access_type {
1438                AtomicAccessType::Rmw | AtomicAccessType::Store => {
1439                    throw_ub_format!(
1440                        "atomic store and read-modify-write operations cannot be performed on read-only memory\n\
1441                        see <https://doc.rust-lang.org/nightly/std/sync/atomic/index.html#atomic-accesses-to-read-only-memory> for more information"
1442                    );
1443                }
1444                AtomicAccessType::Load(_)
1445                    if place.layout.size > this.tcx.data_layout().pointer_size() =>
1446                {
1447                    throw_ub_format!(
1448                        "large atomic load operations cannot be performed on read-only memory\n\
1449                        these operations often have to be implemented using read-modify-write operations, which require writeable memory\n\
1450                        see <https://doc.rust-lang.org/nightly/std/sync/atomic/index.html#atomic-accesses-to-read-only-memory> for more information"
1451                    );
1452                }
1453                AtomicAccessType::Load(o) if o != AtomicReadOrd::Relaxed => {
1454                    throw_ub_format!(
1455                        "non-relaxed atomic load operations cannot be performed on read-only memory\n\
1456                        these operations sometimes have to be implemented using read-modify-write operations, which require writeable memory\n\
1457                        see <https://doc.rust-lang.org/nightly/std/sync/atomic/index.html#atomic-accesses-to-read-only-memory> for more information"
1458                    );
1459                }
1460                _ => {
1461                    // Large relaxed loads are fine!
1462                }
1463            }
1464        }
1465        interp_ok(())
1466    }
1467
1468    /// Update the data-race detector for an atomic read occurring at the
1469    /// associated memory-place and on the current thread.
1470    fn validate_atomic_load(
1471        &self,
1472        place: &MPlaceTy<'tcx>,
1473        atomic: AtomicReadOrd,
1474        sync_clock: Option<&VClock>,
1475    ) -> InterpResult<'tcx> {
1476        let this = self.eval_context_ref();
1477        this.validate_atomic_op(
1478            place,
1479            atomic,
1480            AccessType::AtomicLoad,
1481            move |memory, clocks, index, atomic| {
1482                if atomic == AtomicReadOrd::Relaxed {
1483                    memory.load_relaxed(&mut *clocks, index, place.layout.size, sync_clock)
1484                } else {
1485                    memory.load_acquire(&mut *clocks, index, place.layout.size, sync_clock)
1486                }
1487            },
1488        )
1489    }
1490
1491    /// Update the data-race detector for an atomic write occurring at the
1492    /// associated memory-place and on the current thread.
1493    fn validate_atomic_store(
1494        &mut self,
1495        place: &MPlaceTy<'tcx>,
1496        atomic: AtomicWriteOrd,
1497    ) -> InterpResult<'tcx> {
1498        let this = self.eval_context_mut();
1499        this.validate_atomic_op(
1500            place,
1501            atomic,
1502            AccessType::AtomicStore,
1503            move |memory, clocks, index, atomic| {
1504                if atomic == AtomicWriteOrd::Relaxed {
1505                    memory.store_relaxed(clocks, index, place.layout.size)
1506                } else {
1507                    memory.store_release(clocks, index, place.layout.size)
1508                }
1509            },
1510        )
1511    }
1512
1513    /// Update the data-race detector for an atomic read-modify-write occurring
1514    /// at the associated memory place and on the current thread.
1515    fn validate_atomic_rmw(
1516        &mut self,
1517        place: &MPlaceTy<'tcx>,
1518        atomic: AtomicRwOrd,
1519    ) -> InterpResult<'tcx> {
1520        use AtomicRwOrd::*;
1521        let acquire = matches!(atomic, Acquire | AcqRel | SeqCst);
1522        let release = matches!(atomic, Release | AcqRel | SeqCst);
1523        let this = self.eval_context_mut();
1524        this.validate_atomic_op(
1525            place,
1526            atomic,
1527            AccessType::AtomicRmw,
1528            move |memory, clocks, index, _| {
1529                if acquire {
1530                    memory.load_acquire(clocks, index, place.layout.size, None)?;
1531                } else {
1532                    memory.load_relaxed(clocks, index, place.layout.size, None)?;
1533                }
1534                if release {
1535                    memory.rmw_release(clocks, index, place.layout.size)
1536                } else {
1537                    memory.rmw_relaxed(clocks, index, place.layout.size)
1538                }
1539            },
1540        )
1541    }
1542
1543    /// Generic atomic operation implementation
1544    fn validate_atomic_op<A: Debug + Copy>(
1545        &self,
1546        place: &MPlaceTy<'tcx>,
1547        atomic: A,
1548        access: AccessType,
1549        mut op: impl FnMut(
1550            &mut MemoryCellClocks,
1551            &mut ThreadClockSet,
1552            VectorIdx,
1553            A,
1554        ) -> Result<(), DataRace>,
1555    ) -> InterpResult<'tcx> {
1556        let this = self.eval_context_ref();
1557        assert!(access.is_atomic());
1558        let Some(data_race) = this.machine.data_race.as_vclocks_ref() else {
1559            return interp_ok(());
1560        };
1561        if !data_race.race_detecting() {
1562            return interp_ok(());
1563        }
1564        let size = place.layout.size;
1565        let (alloc_id, base_offset, _prov) = this.ptr_get_alloc_id(place.ptr(), 0)?;
1566        // Load and log the atomic operation.
1567        // Note that atomic loads are possible even from read-only allocations, so `get_alloc_extra_mut` is not an option.
1568        let alloc_meta = this.get_alloc_extra(alloc_id)?.data_race.as_vclocks_ref().unwrap();
1569        trace!(
1570            "Atomic op({}) with ordering {:?} on {:?} (size={})",
1571            access.description(None, None),
1572            &atomic,
1573            place.ptr(),
1574            size.bytes()
1575        );
1576
1577        let current_span = this.machine.current_user_relevant_span();
1578        // Perform the atomic operation.
1579        data_race.maybe_perform_sync_operation(
1580            &this.machine.threads,
1581            current_span,
1582            |index, mut thread_clocks| {
1583                for (mem_clocks_range, mem_clocks) in
1584                    alloc_meta.alloc_ranges.borrow_mut().iter_mut(base_offset, size)
1585                {
1586                    if let Err(DataRace) = op(mem_clocks, &mut thread_clocks, index, atomic) {
1587                        mem::drop(thread_clocks);
1588                        return VClockAlloc::report_data_race(
1589                            data_race,
1590                            &this.machine.threads,
1591                            mem_clocks,
1592                            access,
1593                            place.layout.size,
1594                            interpret::Pointer::new(
1595                                alloc_id,
1596                                Size::from_bytes(mem_clocks_range.start),
1597                            ),
1598                            None,
1599                        )
1600                        .map(|_| true);
1601                    }
1602                }
1603
1604                // This conservatively assumes all operations have release semantics
1605                interp_ok(true)
1606            },
1607        )?;
1608
1609        // Log changes to atomic memory.
1610        if tracing::enabled!(tracing::Level::TRACE) {
1611            for (_offset, mem_clocks) in alloc_meta.alloc_ranges.borrow().iter(base_offset, size) {
1612                trace!(
1613                    "Updated atomic memory({:?}, size={}) to {:#?}",
1614                    place.ptr(),
1615                    size.bytes(),
1616                    mem_clocks.atomic_ops
1617                );
1618            }
1619        }
1620
1621        interp_ok(())
1622    }
1623}
1624
1625impl GlobalState {
1626    /// Create a new global state, setup with just thread-id=0
1627    /// advanced to timestamp = 1.
1628    pub fn new(config: &MiriConfig) -> Self {
1629        let mut global_state = GlobalState {
1630            multi_threaded: Cell::new(false),
1631            ongoing_action_data_race_free: Cell::new(false),
1632            vector_clocks: RefCell::new(IndexVec::new()),
1633            vector_info: RefCell::new(IndexVec::new()),
1634            thread_info: RefCell::new(IndexVec::new()),
1635            reuse_candidates: RefCell::new(FxHashSet::default()),
1636            last_sc_fence: RefCell::new(VClock::default()),
1637            last_sc_write_per_thread: RefCell::new(VClock::default()),
1638            track_outdated_loads: config.track_outdated_loads,
1639            weak_memory: config.weak_memory_emulation,
1640        };
1641
1642        // Setup the main-thread since it is not explicitly created:
1643        // uses vector index and thread-id 0.
1644        let index = global_state.vector_clocks.get_mut().push(ThreadClockSet::default());
1645        global_state.vector_info.get_mut().push(ThreadId::MAIN_THREAD);
1646        global_state
1647            .thread_info
1648            .get_mut()
1649            .push(ThreadExtraState { vector_index: Some(index), termination_vector_clock: None });
1650
1651        global_state
1652    }
1653
1654    // We perform data race detection when there are more than 1 active thread
1655    // and we have not temporarily disabled race detection to perform something
1656    // data race free
1657    fn race_detecting(&self) -> bool {
1658        self.multi_threaded.get() && !self.ongoing_action_data_race_free.get()
1659    }
1660
1661    pub fn ongoing_action_data_race_free(&self) -> bool {
1662        self.ongoing_action_data_race_free.get()
1663    }
1664
1665    // Try to find vector index values that can potentially be re-used
1666    // by a new thread instead of a new vector index being created.
1667    fn find_vector_index_reuse_candidate(&self) -> Option<VectorIdx> {
1668        let mut reuse = self.reuse_candidates.borrow_mut();
1669        let vector_clocks = self.vector_clocks.borrow();
1670        for &candidate in reuse.iter() {
1671            let target_timestamp = vector_clocks[candidate].clock[candidate];
1672            if vector_clocks.iter_enumerated().all(|(clock_idx, clock)| {
1673                // The thread happens before the clock, and hence cannot report
1674                // a data-race with this the candidate index.
1675                let no_data_race = clock.clock[candidate] >= target_timestamp;
1676
1677                // The vector represents a thread that has terminated and hence cannot
1678                // report a data-race with the candidate index.
1679                let vector_terminated = reuse.contains(&clock_idx);
1680
1681                // The vector index cannot report a race with the candidate index
1682                // and hence allows the candidate index to be re-used.
1683                no_data_race || vector_terminated
1684            }) {
1685                // All vector clocks for each vector index are equal to
1686                // the target timestamp, and the thread is known to have
1687                // terminated, therefore this vector clock index cannot
1688                // report any more data-races.
1689                assert!(reuse.remove(&candidate));
1690                return Some(candidate);
1691            }
1692        }
1693        None
1694    }
1695
1696    // Hook for thread creation, enabled multi-threaded execution and marks
1697    // the current thread timestamp as happening-before the current thread.
1698    #[inline]
1699    pub fn thread_created(
1700        &mut self,
1701        thread_mgr: &ThreadManager<'_>,
1702        thread: ThreadId,
1703        current_span: Span,
1704    ) {
1705        let current_index = self.active_thread_index(thread_mgr);
1706
1707        // Enable multi-threaded execution, there are now at least two threads
1708        // so data-races are now possible.
1709        self.multi_threaded.set(true);
1710
1711        // Load and setup the associated thread metadata
1712        let mut thread_info = self.thread_info.borrow_mut();
1713        thread_info.ensure_contains_elem(thread, Default::default);
1714
1715        // Assign a vector index for the thread, attempting to re-use an old
1716        // vector index that can no longer report any data-races if possible.
1717        let created_index = if let Some(reuse_index) = self.find_vector_index_reuse_candidate() {
1718            // Now re-configure the re-use candidate, increment the clock
1719            // for the new sync use of the vector.
1720            let vector_clocks = self.vector_clocks.get_mut();
1721            vector_clocks[reuse_index].increment_clock(reuse_index, current_span);
1722
1723            // Locate the old thread the vector was associated with and update
1724            // it to represent the new thread instead.
1725            let vector_info = self.vector_info.get_mut();
1726            let old_thread = vector_info[reuse_index];
1727            vector_info[reuse_index] = thread;
1728
1729            // Mark the thread the vector index was associated with as no longer
1730            // representing a thread index.
1731            thread_info[old_thread].vector_index = None;
1732
1733            reuse_index
1734        } else {
1735            // No vector re-use candidates available, instead create
1736            // a new vector index.
1737            let vector_info = self.vector_info.get_mut();
1738            vector_info.push(thread)
1739        };
1740
1741        trace!("Creating thread = {:?} with vector index = {:?}", thread, created_index);
1742
1743        // Mark the chosen vector index as in use by the thread.
1744        thread_info[thread].vector_index = Some(created_index);
1745
1746        // Create a thread clock set if applicable.
1747        let vector_clocks = self.vector_clocks.get_mut();
1748        if created_index == vector_clocks.next_index() {
1749            vector_clocks.push(ThreadClockSet::default());
1750        }
1751
1752        // Now load the two clocks and configure the initial state.
1753        let (current, created) = vector_clocks.pick2_mut(current_index, created_index);
1754
1755        // Join the created with current, since the current threads
1756        // previous actions happen-before the created thread.
1757        created.join_with(current);
1758
1759        // Advance both threads after the synchronized operation.
1760        // Both operations are considered to have release semantics.
1761        current.increment_clock(current_index, current_span);
1762        created.increment_clock(created_index, current_span);
1763    }
1764
1765    /// Hook on a thread join to update the implicit happens-before relation between the joined
1766    /// thread (the joinee, the thread that someone waited on) and the current thread (the joiner,
1767    /// the thread who was waiting).
1768    #[inline]
1769    pub fn thread_joined(&mut self, threads: &ThreadManager<'_>, joinee: ThreadId) {
1770        let thread_info = self.thread_info.borrow();
1771        let thread_info = &thread_info[joinee];
1772
1773        // Load the associated vector clock for the terminated thread.
1774        let join_clock = thread_info
1775            .termination_vector_clock
1776            .as_ref()
1777            .expect("joined with thread but thread has not terminated");
1778        // Acquire that into the current thread.
1779        self.acquire_clock(join_clock, threads);
1780
1781        // Check the number of live threads, if the value is 1
1782        // then test for potentially disabling multi-threaded execution.
1783        // This has to happen after `acquire_clock`, otherwise there'll always
1784        // be some thread that has not synchronized yet.
1785        if let Some(current_index) = thread_info.vector_index {
1786            if threads.get_live_thread_count() == 1 {
1787                let vector_clocks = self.vector_clocks.get_mut();
1788                // May potentially be able to disable multi-threaded execution.
1789                let current_clock = &vector_clocks[current_index];
1790                if vector_clocks
1791                    .iter_enumerated()
1792                    .all(|(idx, clocks)| clocks.clock[idx] <= current_clock.clock[idx])
1793                {
1794                    // All thread terminations happen-before the current clock
1795                    // therefore no data-races can be reported until a new thread
1796                    // is created, so disable multi-threaded execution.
1797                    self.multi_threaded.set(false);
1798                }
1799            }
1800        }
1801    }
1802
1803    /// On thread termination, the vector clock may be re-used
1804    /// in the future once all remaining thread-clocks catch
1805    /// up with the time index of the terminated thread.
1806    /// This assigns thread termination with a unique index
1807    /// which will be used to join the thread
1808    /// This should be called strictly before any calls to
1809    /// `thread_joined`.
1810    #[inline]
1811    pub fn thread_terminated(&mut self, thread_mgr: &ThreadManager<'_>) {
1812        let current_thread = thread_mgr.active_thread();
1813        let current_index = self.active_thread_index(thread_mgr);
1814
1815        // Store the terminaion clock.
1816        let terminaion_clock = self.release_clock(thread_mgr, |clock| clock.clone());
1817        self.thread_info.get_mut()[current_thread].termination_vector_clock =
1818            Some(terminaion_clock);
1819
1820        // Add this thread's clock index as a candidate for re-use.
1821        let reuse = self.reuse_candidates.get_mut();
1822        reuse.insert(current_index);
1823    }
1824
1825    /// Update the data-race detector for an atomic fence on the current thread.
1826    fn atomic_fence<'tcx>(
1827        &self,
1828        machine: &MiriMachine<'tcx>,
1829        atomic: AtomicFenceOrd,
1830    ) -> InterpResult<'tcx> {
1831        let current_span = machine.current_user_relevant_span();
1832        self.maybe_perform_sync_operation(&machine.threads, current_span, |index, mut clocks| {
1833            trace!("Atomic fence on {:?} with ordering {:?}", index, atomic);
1834
1835            // Apply data-race detection for the current fences
1836            // this treats AcqRel and SeqCst as the same as an acquire
1837            // and release fence applied in the same timestamp.
1838            if atomic != AtomicFenceOrd::Release {
1839                // Either Acquire | AcqRel | SeqCst
1840                clocks.apply_acquire_fence();
1841            }
1842            if atomic == AtomicFenceOrd::SeqCst {
1843                // Behave like an RMW on the global fence location. This takes full care of
1844                // all the SC fence requirements, including C++17 ยง32.4 [atomics.order]
1845                // paragraph 6 (which would limit what future reads can see). It also rules
1846                // out many legal behaviors, but we don't currently have a model that would
1847                // be more precise.
1848                // Also see the second bullet on page 10 of
1849                // <https://www.cs.tau.ac.il/~orilahav/papers/popl21_robustness.pdf>.
1850                let mut sc_fence_clock = self.last_sc_fence.borrow_mut();
1851                sc_fence_clock.join(&clocks.clock);
1852                clocks.clock.join(&sc_fence_clock);
1853                // Also establish some sort of order with the last SC write that happened, globally
1854                // (but this is only respected by future reads).
1855                clocks.write_seqcst.join(&self.last_sc_write_per_thread.borrow());
1856            }
1857            // The release fence is last, since both of the above could alter our clock,
1858            // which should be part of what is being released.
1859            if atomic != AtomicFenceOrd::Acquire {
1860                // Either Release | AcqRel | SeqCst
1861                clocks.apply_release_fence();
1862            }
1863
1864            // Increment timestamp in case of release semantics.
1865            interp_ok(atomic != AtomicFenceOrd::Acquire)
1866        })
1867    }
1868
1869    /// Attempt to perform a synchronized operation, this
1870    /// will perform no operation if multi-threading is
1871    /// not currently enabled.
1872    /// Otherwise it will increment the clock for the current
1873    /// vector before and after the operation for data-race
1874    /// detection between any happens-before edges the
1875    /// operation may create.
1876    fn maybe_perform_sync_operation<'tcx>(
1877        &self,
1878        thread_mgr: &ThreadManager<'_>,
1879        current_span: Span,
1880        op: impl FnOnce(VectorIdx, RefMut<'_, ThreadClockSet>) -> InterpResult<'tcx, bool>,
1881    ) -> InterpResult<'tcx> {
1882        if self.multi_threaded.get() {
1883            let (index, clocks) = self.active_thread_state_mut(thread_mgr);
1884            if op(index, clocks)? {
1885                let (_, mut clocks) = self.active_thread_state_mut(thread_mgr);
1886                clocks.increment_clock(index, current_span);
1887            }
1888        }
1889        interp_ok(())
1890    }
1891
1892    /// Internal utility to identify a thread stored internally
1893    /// returns the id and the name for better diagnostics.
1894    fn print_thread_metadata(&self, thread_mgr: &ThreadManager<'_>, vector: VectorIdx) -> String {
1895        let thread = self.vector_info.borrow()[vector];
1896        let thread_name = thread_mgr.get_thread_display_name(thread);
1897        format!("thread `{thread_name}`")
1898    }
1899
1900    /// Acquire the given clock into the current thread, establishing synchronization with
1901    /// the moment when that clock snapshot was taken via `release_clock`.
1902    /// As this is an acquire operation, the thread timestamp is not
1903    /// incremented.
1904    pub fn acquire_clock<'tcx>(&self, clock: &VClock, threads: &ThreadManager<'tcx>) {
1905        let thread = threads.active_thread();
1906        let (_, mut clocks) = self.thread_state_mut(thread);
1907        clocks.clock.join(clock);
1908    }
1909
1910    /// Calls the given closure with the "release" clock of the current thread.
1911    /// Other threads can acquire this clock in the future to establish synchronization
1912    /// with this program point.
1913    pub fn release_clock<'tcx, R>(
1914        &self,
1915        threads: &ThreadManager<'tcx>,
1916        callback: impl FnOnce(&VClock) -> R,
1917    ) -> R {
1918        let thread = threads.active_thread();
1919        let span = threads.active_thread_ref().current_user_relevant_span();
1920        let (index, mut clocks) = self.thread_state_mut(thread);
1921        let r = callback(&clocks.clock);
1922        // Increment the clock, so that all following events cannot be confused with anything that
1923        // occurred before the release. Crucially, the callback is invoked on the *old* clock!
1924        clocks.increment_clock(index, span);
1925
1926        r
1927    }
1928
1929    fn thread_index(&self, thread: ThreadId) -> VectorIdx {
1930        self.thread_info.borrow()[thread].vector_index.expect("thread has no assigned vector")
1931    }
1932
1933    /// Load the vector index used by the given thread as well as the set of vector clocks
1934    /// used by the thread.
1935    #[inline]
1936    fn thread_state_mut(&self, thread: ThreadId) -> (VectorIdx, RefMut<'_, ThreadClockSet>) {
1937        let index = self.thread_index(thread);
1938        let ref_vector = self.vector_clocks.borrow_mut();
1939        let clocks = RefMut::map(ref_vector, |vec| &mut vec[index]);
1940        (index, clocks)
1941    }
1942
1943    /// Load the vector index used by the given thread as well as the set of vector clocks
1944    /// used by the thread.
1945    #[inline]
1946    fn thread_state(&self, thread: ThreadId) -> (VectorIdx, Ref<'_, ThreadClockSet>) {
1947        let index = self.thread_index(thread);
1948        let ref_vector = self.vector_clocks.borrow();
1949        let clocks = Ref::map(ref_vector, |vec| &vec[index]);
1950        (index, clocks)
1951    }
1952
1953    /// Load the current vector clock in use and the current set of thread clocks
1954    /// in use for the vector.
1955    #[inline]
1956    pub(super) fn active_thread_state(
1957        &self,
1958        thread_mgr: &ThreadManager<'_>,
1959    ) -> (VectorIdx, Ref<'_, ThreadClockSet>) {
1960        self.thread_state(thread_mgr.active_thread())
1961    }
1962
1963    /// Load the current vector clock in use and the current set of thread clocks
1964    /// in use for the vector mutably for modification.
1965    #[inline]
1966    pub(super) fn active_thread_state_mut(
1967        &self,
1968        thread_mgr: &ThreadManager<'_>,
1969    ) -> (VectorIdx, RefMut<'_, ThreadClockSet>) {
1970        self.thread_state_mut(thread_mgr.active_thread())
1971    }
1972
1973    /// Return the current thread, should be the same
1974    /// as the data-race active thread.
1975    #[inline]
1976    fn active_thread_index(&self, thread_mgr: &ThreadManager<'_>) -> VectorIdx {
1977        let active_thread_id = thread_mgr.active_thread();
1978        self.thread_index(active_thread_id)
1979    }
1980
1981    // SC ATOMIC STORE rule in the paper.
1982    pub(super) fn sc_write(&self, thread_mgr: &ThreadManager<'_>) {
1983        let (index, clocks) = self.active_thread_state(thread_mgr);
1984        self.last_sc_write_per_thread.borrow_mut().set_at_index(&clocks.clock, index);
1985    }
1986
1987    // SC ATOMIC READ rule in the paper.
1988    pub(super) fn sc_read(&self, thread_mgr: &ThreadManager<'_>) {
1989        let (.., mut clocks) = self.active_thread_state_mut(thread_mgr);
1990        clocks.read_seqcst.join(&self.last_sc_fence.borrow());
1991    }
1992}