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