miri/concurrency/
weak_memory.rs

1//! Implementation of C++11-consistent weak memory emulation using store buffers
2//! based on Dynamic Race Detection for C++ ("the paper"):
3//! <https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf>
4//!
5//! This implementation will never generate weak memory behaviours forbidden by the C++11 model,
6//! but it is incapable of producing all possible weak behaviours allowed by the model. There are
7//! certain weak behaviours observable on real hardware but not while using this.
8//!
9//! Note that this implementation does not fully take into account of C++20's memory model revision to SC accesses
10//! and fences introduced by P0668 (<https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0668r5.html>).
11//! This implementation is not fully correct under the revised C++20 model and may generate behaviours C++20
12//! disallows (<https://github.com/rust-lang/miri/issues/2301>).
13//!
14//! Modifications are made to the paper's model to address C++20 changes:
15//! - If an SC load reads from an atomic store of any ordering, then a later SC load cannot read
16//!   from an earlier store in the location's modification order. This is to prevent creating a
17//!   backwards S edge from the second load to the first, as a result of C++20's coherence-ordered
18//!   before rules. (This seems to rule out behaviors that were actually permitted by the RC11 model
19//!   that C++20 intended to copy (<https://plv.mpi-sws.org/scfix/paper.pdf>); a change was
20//!   introduced when translating the math to English. According to Viktor Vafeiadis, this
21//!   difference is harmless. So we stick to what the standard says, and allow fewer behaviors.)
22//! - SC fences are treated like AcqRel RMWs to a global clock, to ensure they induce enough
23//!   synchronization with the surrounding accesses. This rules out legal behavior, but it is really
24//!   hard to be more precise here.
25//!
26//! Rust follows the C++20 memory model (except for the Consume ordering and some operations not performable through C++'s
27//! `std::atomic<T>` API). It is therefore possible for this implementation to generate behaviours never observable when the
28//! same program is compiled and run natively. Unfortunately, no literature exists at the time of writing which proposes
29//! an implementable and C++20-compatible relaxed memory model that supports all atomic operation existing in Rust. The closest one is
30//! A Promising Semantics for Relaxed-Memory Concurrency by Jeehoon Kang et al. (<https://www.cs.tau.ac.il/~orilahav/papers/popl17.pdf>)
31//! However, this model lacks SC accesses and is therefore unusable by Miri (SC accesses are everywhere in library code).
32//!
33//! If you find anything that proposes a relaxed memory model that is C++20-consistent, supports all orderings Rust's atomic accesses
34//! and fences accept, and is implementable (with operational semantics), please open a GitHub issue!
35//!
36//! One characteristic of this implementation, in contrast to some other notable operational models such as ones proposed in
37//! Taming Release-Acquire Consistency by Ori Lahav et al. (<https://plv.mpi-sws.org/sra/paper.pdf>) or Promising Semantics noted above,
38//! is that this implementation does not require each thread to hold an isolated view of the entire memory. Here, store buffers are per-location
39//! and shared across all threads. This is more memory efficient but does require store elements (representing writes to a location) to record
40//! information about reads, whereas in the other two models it is the other way round: reads points to the write it got its value from.
41//! Additionally, writes in our implementation do not have globally unique timestamps attached. In the other two models this timestamp is
42//! used to make sure a value in a thread's view is not overwritten by a write that occurred earlier than the one in the existing view.
43//! In our implementation, this is detected using read information attached to store elements, as there is no data structure representing reads.
44//!
45//! The C++ memory model is built around the notion of an 'atomic object', so it would be natural
46//! to attach store buffers to atomic objects. However, Rust follows LLVM in that it only has
47//! 'atomic accesses'. Therefore Miri cannot know when and where atomic 'objects' are being
48//! created or destroyed, to manage its store buffers. Instead, we hence lazily create an
49//! atomic object on the first atomic write to a given region, and we destroy that object
50//! on the next non-atomic or imperfectly overlapping atomic write to that region.
51//! These lazy (de)allocations happen in memory_accessed() on non-atomic accesses, and
52//! get_or_create_store_buffer_mut() on atomic writes.
53//!
54//! One consequence of this difference is that safe/sound Rust allows for more operations on atomic locations
55//! than the C++20 atomic API was intended to allow, such as non-atomically accessing
56//! a previously atomically accessed location, or accessing previously atomically accessed locations with a differently sized operation
57//! (such as accessing the top 16 bits of an AtomicU32). These scenarios are generally undiscussed in formalizations of C++ memory model.
58//! In Rust, these operations can only be done through a `&mut AtomicFoo` reference or one derived from it, therefore these operations
59//! can only happen after all previous accesses on the same locations. This implementation is adapted to allow these operations.
60//! A mixed atomicity read that races with writes, or a write that races with reads or writes will still cause UBs to be thrown.
61//! Mixed size atomic accesses must not race with any other atomic access, whether read or write, or a UB will be thrown.
62//! You can refer to test cases in weak_memory/extra_cpp.rs and weak_memory/extra_cpp_unsafe.rs for examples of these operations.
63
64// Our and the author's own implementation (tsan11) of the paper have some deviations from the provided operational semantics in §5.3:
65// 1. In the operational semantics, loads acquire the vector clock of the atomic location
66// irrespective of which store buffer element is loaded. That's incorrect; the synchronization clock
67// needs to be tracked per-store-buffer-element. (The paper has a field "clocks" for that purpose,
68// but it is not actuallt used.) tsan11 does this correctly
69// (https://github.com/ChrisLidbury/tsan11/blob/ecbd6b81e9b9454e01cba78eb9d88684168132c7/lib/tsan/rtl/tsan_relaxed.cc#L305).
70//
71// 2. In the operational semantics, each store element keeps the timestamp of a thread when it loads from the store.
72// If the same thread loads from the same store element multiple times, then the timestamps at all loads are saved in a list of load elements.
73// This is not necessary as later loads by the same thread will always have greater timestamp values, so we only need to record the timestamp of the first
74// load by each thread. This optimisation is done in tsan11
75// (https://github.com/ChrisLidbury/tsan11/blob/ecbd6b81e9b9454e01cba78eb9d88684168132c7/lib/tsan/rtl/tsan_relaxed.h#L35-L37)
76// and here.
77//
78// 3. §4.5 of the paper wants an SC store to mark all existing stores in the buffer that happens before it
79// as SC. This is not done in the operational semantics but implemented correctly in tsan11
80// (https://github.com/ChrisLidbury/tsan11/blob/ecbd6b81e9b9454e01cba78eb9d88684168132c7/lib/tsan/rtl/tsan_relaxed.cc#L160-L167)
81// and here.
82//
83// 4. W_SC ; R_SC case requires the SC load to ignore all but last store marked SC (stores not marked SC are not
84// affected). But this rule is applied to all loads in ReadsFromSet from the paper (last two lines of code), not just SC load.
85// This is implemented correctly in tsan11
86// (https://github.com/ChrisLidbury/tsan11/blob/ecbd6b81e9b9454e01cba78eb9d88684168132c7/lib/tsan/rtl/tsan_relaxed.cc#L295)
87// and here.
88
89use std::cell::{Ref, RefCell};
90use std::collections::VecDeque;
91
92use rustc_data_structures::fx::FxHashMap;
93
94use super::AllocDataRaceHandler;
95use super::data_race::{GlobalState as DataRaceState, ThreadClockSet};
96use super::vector_clock::{VClock, VTimestamp, VectorIdx};
97use crate::concurrency::GlobalDataRaceHandler;
98use crate::data_structures::range_object_map::{AccessType, RangeObjectMap};
99use crate::*;
100
101pub type AllocState = StoreBufferAlloc;
102
103// Each store buffer must be bounded otherwise it will grow indefinitely.
104// However, bounding the store buffer means restricting the amount of weak
105// behaviours observable. The author picked 128 as a good tradeoff
106// so we follow them here.
107const STORE_BUFFER_LIMIT: usize = 128;
108
109#[derive(Debug, Clone)]
110pub struct StoreBufferAlloc {
111    /// Store buffer of each atomic object in this allocation
112    // Behind a RefCell because we need to allocate/remove on read access
113    store_buffers: RefCell<RangeObjectMap<StoreBuffer>>,
114}
115
116impl VisitProvenance for StoreBufferAlloc {
117    fn visit_provenance(&self, visit: &mut VisitWith<'_>) {
118        let Self { store_buffers } = self;
119        for val in store_buffers
120            .borrow()
121            .iter()
122            .flat_map(|buf| buf.buffer.iter().map(|element| &element.val))
123        {
124            val.visit_provenance(visit);
125        }
126    }
127}
128
129#[derive(Debug, Clone, PartialEq, Eq)]
130pub(super) struct StoreBuffer {
131    // Stores to this location in modification order
132    buffer: VecDeque<StoreElement>,
133}
134
135/// Whether a load returned the latest value or not.
136#[derive(PartialEq, Eq)]
137enum LoadRecency {
138    Latest,
139    Outdated,
140}
141
142#[derive(Debug, Clone, PartialEq, Eq)]
143struct StoreElement {
144    /// The thread that performed the store.
145    store_thread: VectorIdx,
146    /// The timestamp of the storing thread when it performed the store
147    store_timestamp: VTimestamp,
148
149    /// The vector clock that can be acquired by loading this store.
150    sync_clock: VClock,
151
152    /// Whether this store is SC.
153    is_seqcst: bool,
154
155    /// The value of this store. `None` means uninitialized.
156    // FIXME: Currently, we cannot represent partial initialization.
157    val: Option<Scalar>,
158
159    /// Metadata about loads from this store element,
160    /// behind a RefCell to keep load op take &self
161    load_info: RefCell<LoadInfo>,
162}
163
164#[derive(Debug, Clone, PartialEq, Eq, Default)]
165struct LoadInfo {
166    /// Timestamp of first loads from this store element by each thread.
167    timestamps: FxHashMap<VectorIdx, VTimestamp>,
168    /// Whether this store element has been read by an SC load.
169    /// This is crucial to ensure we respect coherence-ordered-before. Concretely we use
170    /// this to ensure that if a store element is seen by an SC load, then all later SC loads
171    /// cannot see `mo`-earlier store elements.
172    sc_loaded: bool,
173}
174
175impl StoreBufferAlloc {
176    pub fn new_allocation() -> Self {
177        Self { store_buffers: RefCell::new(RangeObjectMap::new()) }
178    }
179
180    /// When a non-atomic access happens on a location that has been atomically accessed
181    /// before without data race, we can determine that the non-atomic access fully happens
182    /// after all the prior atomic writes so the location no longer needs to exhibit
183    /// any weak memory behaviours until further atomic accesses.
184    pub fn memory_accessed(&self, range: AllocRange, global: &DataRaceState) {
185        if !global.ongoing_action_data_race_free() {
186            let mut buffers = self.store_buffers.borrow_mut();
187            let access_type = buffers.access_type(range);
188            match access_type {
189                AccessType::PerfectlyOverlapping(pos) => {
190                    buffers.remove_from_pos(pos);
191                }
192                AccessType::ImperfectlyOverlapping(pos_range) => {
193                    // We rely on the data-race check making sure this is synchronized.
194                    // Therefore we can forget about the old data here.
195                    buffers.remove_pos_range(pos_range);
196                }
197                AccessType::Empty(_) => {
198                    // The range had no weak behaviours attached, do nothing
199                }
200            }
201        }
202    }
203
204    /// Gets a store buffer associated with an atomic object in this allocation.
205    /// Returns `None` if there is no store buffer.
206    fn get_store_buffer<'tcx>(
207        &self,
208        range: AllocRange,
209    ) -> InterpResult<'tcx, Option<Ref<'_, StoreBuffer>>> {
210        let access_type = self.store_buffers.borrow().access_type(range);
211        let pos = match access_type {
212            AccessType::PerfectlyOverlapping(pos) => pos,
213            // If there is nothing here yet, that means there wasn't an atomic write yet so
214            // we can't return anything outdated.
215            _ => return interp_ok(None),
216        };
217        let store_buffer = Ref::map(self.store_buffers.borrow(), |buffer| &buffer[pos]);
218        interp_ok(Some(store_buffer))
219    }
220
221    /// Gets a mutable store buffer associated with an atomic object in this allocation,
222    /// or creates one with the specified initial value if no atomic object exists yet.
223    fn get_or_create_store_buffer_mut<'tcx>(
224        &mut self,
225        range: AllocRange,
226        init: Option<Scalar>,
227    ) -> InterpResult<'tcx, &mut StoreBuffer> {
228        let buffers = self.store_buffers.get_mut();
229        let access_type = buffers.access_type(range);
230        let pos = match access_type {
231            AccessType::PerfectlyOverlapping(pos) => pos,
232            AccessType::Empty(pos) => {
233                buffers.insert_at_pos(pos, range, StoreBuffer::new(init));
234                pos
235            }
236            AccessType::ImperfectlyOverlapping(pos_range) => {
237                // Once we reach here we would've already checked that this access is not racy.
238                buffers.remove_pos_range(pos_range.clone());
239                buffers.insert_at_pos(pos_range.start, range, StoreBuffer::new(init));
240                pos_range.start
241            }
242        };
243        interp_ok(&mut buffers[pos])
244    }
245}
246
247impl<'tcx> StoreBuffer {
248    fn new(init: Option<Scalar>) -> Self {
249        let mut buffer = VecDeque::new();
250        let store_elem = StoreElement {
251            // The thread index and timestamp of the initialisation write
252            // are never meaningfully used, so it's fine to leave them as 0
253            store_thread: VectorIdx::from(0),
254            store_timestamp: VTimestamp::ZERO,
255            // The initialization write is non-atomic so nothing can be acquired.
256            sync_clock: VClock::default(),
257            val: init,
258            is_seqcst: false,
259            load_info: RefCell::new(LoadInfo::default()),
260        };
261        buffer.push_back(store_elem);
262        Self { buffer }
263    }
264
265    /// Reads from the last store in modification order, if any.
266    fn read_from_last_store(
267        &self,
268        global: &DataRaceState,
269        thread_mgr: &ThreadManager<'_>,
270        is_seqcst: bool,
271    ) {
272        let store_elem = self.buffer.back();
273        if let Some(store_elem) = store_elem {
274            let (index, clocks) = global.active_thread_state(thread_mgr);
275            store_elem.load_impl(index, &clocks, is_seqcst);
276        }
277    }
278
279    fn buffered_read(
280        &self,
281        global: &DataRaceState,
282        thread_mgr: &ThreadManager<'_>,
283        is_seqcst: bool,
284        rng: &mut (impl rand::Rng + ?Sized),
285        validate: impl FnOnce(Option<&VClock>) -> InterpResult<'tcx>,
286    ) -> InterpResult<'tcx, (Option<Scalar>, LoadRecency)> {
287        // Having a live borrow to store_buffer while calling validate_atomic_load is fine
288        // because the race detector doesn't touch store_buffer
289
290        let (store_elem, recency) = {
291            // The `clocks` we got here must be dropped before calling validate_atomic_load
292            // as the race detector will update it
293            let (.., clocks) = global.active_thread_state(thread_mgr);
294            // Load from a valid entry in the store buffer
295            self.fetch_store(is_seqcst, &clocks, &mut *rng)
296        };
297
298        // Unlike in buffered_atomic_write, thread clock updates have to be done
299        // after we've picked a store element from the store buffer, as presented
300        // in ATOMIC LOAD rule of the paper. This is because fetch_store
301        // requires access to ThreadClockSet.clock, which is updated by the race detector
302        validate(Some(&store_elem.sync_clock))?;
303
304        let (index, clocks) = global.active_thread_state(thread_mgr);
305        let loaded = store_elem.load_impl(index, &clocks, is_seqcst);
306        interp_ok((loaded, recency))
307    }
308
309    fn buffered_write(
310        &mut self,
311        val: Scalar,
312        global: &DataRaceState,
313        thread_mgr: &ThreadManager<'_>,
314        is_seqcst: bool,
315        sync_clock: VClock,
316    ) -> InterpResult<'tcx> {
317        let (index, clocks) = global.active_thread_state(thread_mgr);
318
319        self.store_impl(val, index, &clocks.clock, is_seqcst, sync_clock);
320        interp_ok(())
321    }
322
323    /// Selects a valid store element in the buffer.
324    fn fetch_store<R: rand::Rng + ?Sized>(
325        &self,
326        is_seqcst: bool,
327        clocks: &ThreadClockSet,
328        rng: &mut R,
329    ) -> (&StoreElement, LoadRecency) {
330        use rand::seq::IteratorRandom;
331        let mut found_sc = false;
332        // FIXME: we want an inclusive take_while (stops after a false predicate, but
333        // includes the element that gave the false), but such function doesn't yet
334        // exist in the standard library https://github.com/rust-lang/rust/issues/62208
335        // so we have to hack around it with keep_searching
336        let mut keep_searching = true;
337        let candidates = self
338            .buffer
339            .iter()
340            .rev()
341            .take_while(move |&store_elem| {
342                if !keep_searching {
343                    return false;
344                }
345
346                keep_searching = if store_elem.store_timestamp
347                    <= clocks.clock[store_elem.store_thread]
348                {
349                    // CoWR: if a store happens-before the current load,
350                    // then we can't read-from anything earlier in modification order.
351                    // C++20 §6.9.2.2 [intro.races] paragraph 18
352                    false
353                } else if store_elem.load_info.borrow().timestamps.iter().any(
354                    |(&load_index, &load_timestamp)| load_timestamp <= clocks.clock[load_index],
355                ) {
356                    // CoRR: if there was a load from this store which happened-before the current load,
357                    // then we cannot read-from anything earlier in modification order.
358                    // C++20 §6.9.2.2 [intro.races] paragraph 16
359                    false
360                } else if store_elem.store_timestamp <= clocks.write_seqcst[store_elem.store_thread]
361                    && store_elem.is_seqcst
362                {
363                    // The current non-SC load, which may be sequenced-after an SC fence,
364                    // cannot read-before the last SC store executed before the fence.
365                    // C++17 §32.4 [atomics.order] paragraph 4
366                    false
367                } else if is_seqcst
368                    && store_elem.store_timestamp <= clocks.read_seqcst[store_elem.store_thread]
369                {
370                    // The current SC load cannot read-before the last store sequenced-before
371                    // the last SC fence.
372                    // C++17 §32.4 [atomics.order] paragraph 5
373                    false
374                } else if is_seqcst && store_elem.load_info.borrow().sc_loaded {
375                    // The current SC load cannot read-before a store that an earlier SC load has observed.
376                    // See https://github.com/rust-lang/miri/issues/2301#issuecomment-1222720427.
377                    // Consequences of C++20 §31.4 [atomics.order] paragraph 3.1, 3.3 (coherence-ordered before)
378                    // and 4.1 (coherence-ordered before between SC makes global total order S).
379                    false
380                } else {
381                    true
382                };
383
384                true
385            })
386            .filter(|&store_elem| {
387                if is_seqcst && store_elem.is_seqcst {
388                    // An SC load needs to ignore all but last store maked SC (stores not marked SC are not
389                    // affected)
390                    let include = !found_sc;
391                    found_sc = true;
392                    include
393                } else {
394                    true
395                }
396            });
397
398        let chosen = candidates.choose(rng).expect("store buffer cannot be empty");
399        if std::ptr::eq(chosen, self.buffer.back().expect("store buffer cannot be empty")) {
400            (chosen, LoadRecency::Latest)
401        } else {
402            (chosen, LoadRecency::Outdated)
403        }
404    }
405
406    /// ATOMIC STORE IMPL in the paper
407    fn store_impl(
408        &mut self,
409        val: Scalar,
410        index: VectorIdx,
411        thread_clock: &VClock,
412        is_seqcst: bool,
413        sync_clock: VClock,
414    ) {
415        let store_elem = StoreElement {
416            store_thread: index,
417            store_timestamp: thread_clock[index],
418            sync_clock,
419            // In the language provided in the paper, an atomic store takes the value from a
420            // non-atomic memory location.
421            // But we already have the immediate value here so we don't need to do the memory
422            // access.
423            val: Some(val),
424            is_seqcst,
425            load_info: RefCell::new(LoadInfo::default()),
426        };
427        if self.buffer.len() >= STORE_BUFFER_LIMIT {
428            self.buffer.pop_front();
429        }
430        self.buffer.push_back(store_elem);
431        if is_seqcst {
432            // Every store that happens before this needs to be marked as SC
433            // so that in a later SC load, only the last SC store (i.e. this one) or stores that
434            // aren't ordered by hb with the last SC is picked.
435            self.buffer.iter_mut().rev().for_each(|elem| {
436                if elem.store_timestamp <= thread_clock[elem.store_thread] {
437                    elem.is_seqcst = true;
438                }
439            })
440        }
441    }
442}
443
444impl StoreElement {
445    /// ATOMIC LOAD IMPL in the paper
446    /// Unlike the operational semantics in the paper, we don't need to keep track
447    /// of the thread timestamp for every single load. Keeping track of the first (smallest)
448    /// timestamp of each thread that has loaded from a store is sufficient: if the earliest
449    /// load of another thread happens before the current one, then we must stop searching the store
450    /// buffer regardless of subsequent loads by the same thread; if the earliest load of another
451    /// thread doesn't happen before the current one, then no subsequent load by the other thread
452    /// can happen before the current one.
453    fn load_impl(
454        &self,
455        index: VectorIdx,
456        clocks: &ThreadClockSet,
457        is_seqcst: bool,
458    ) -> Option<Scalar> {
459        let mut load_info = self.load_info.borrow_mut();
460        load_info.sc_loaded |= is_seqcst;
461        let _ = load_info.timestamps.try_insert(index, clocks.clock[index]);
462        self.val
463    }
464}
465
466impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
467pub(super) trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
468    fn buffered_atomic_rmw(
469        &mut self,
470        new_val: Scalar,
471        place: &MPlaceTy<'tcx>,
472        atomic: AtomicRwOrd,
473        init: Scalar,
474    ) -> InterpResult<'tcx> {
475        let this = self.eval_context_mut();
476        let (alloc_id, base_offset, ..) = this.ptr_get_alloc_id(place.ptr(), 0)?;
477        if let (
478            crate::AllocExtra {
479                data_race: AllocDataRaceHandler::Vclocks(data_race_clocks, Some(alloc_buffers)),
480                ..
481            },
482            crate::MiriMachine {
483                data_race: GlobalDataRaceHandler::Vclocks(global), threads, ..
484            },
485        ) = this.get_alloc_extra_mut(alloc_id)?
486        {
487            if atomic == AtomicRwOrd::SeqCst {
488                global.sc_read(threads);
489                global.sc_write(threads);
490            }
491            let range = alloc_range(base_offset, place.layout.size);
492            let sync_clock = data_race_clocks.sync_clock(range);
493            let buffer = alloc_buffers.get_or_create_store_buffer_mut(range, Some(init))?;
494            // The RMW always reads from the most recent store.
495            buffer.read_from_last_store(global, threads, atomic == AtomicRwOrd::SeqCst);
496            buffer.buffered_write(
497                new_val,
498                global,
499                threads,
500                atomic == AtomicRwOrd::SeqCst,
501                sync_clock,
502            )?;
503        }
504        interp_ok(())
505    }
506
507    /// The argument to `validate` is the synchronization clock of the memory that is being read,
508    /// if we are reading from a store buffer element.
509    fn buffered_atomic_read(
510        &self,
511        place: &MPlaceTy<'tcx>,
512        atomic: AtomicReadOrd,
513        latest_in_mo: Scalar,
514        validate: impl FnOnce(Option<&VClock>) -> InterpResult<'tcx>,
515    ) -> InterpResult<'tcx, Option<Scalar>> {
516        let this = self.eval_context_ref();
517        'fallback: {
518            if let Some(global) = this.machine.data_race.as_vclocks_ref() {
519                let (alloc_id, base_offset, ..) = this.ptr_get_alloc_id(place.ptr(), 0)?;
520                if let Some(alloc_buffers) =
521                    this.get_alloc_extra(alloc_id)?.data_race.as_weak_memory_ref()
522                {
523                    if atomic == AtomicReadOrd::SeqCst {
524                        global.sc_read(&this.machine.threads);
525                    }
526                    let mut rng = this.machine.rng.borrow_mut();
527                    let Some(buffer) = alloc_buffers
528                        .get_store_buffer(alloc_range(base_offset, place.layout.size))?
529                    else {
530                        // No old writes available, fall back to base case.
531                        break 'fallback;
532                    };
533                    let (loaded, recency) = buffer.buffered_read(
534                        global,
535                        &this.machine.threads,
536                        atomic == AtomicReadOrd::SeqCst,
537                        &mut *rng,
538                        validate,
539                    )?;
540                    if global.track_outdated_loads && recency == LoadRecency::Outdated {
541                        this.emit_diagnostic(NonHaltingDiagnostic::WeakMemoryOutdatedLoad {
542                            ptr: place.ptr(),
543                        });
544                    }
545
546                    return interp_ok(loaded);
547                }
548            }
549        }
550
551        // Race detector or weak memory disabled, simply read the latest value
552        validate(None)?;
553        interp_ok(Some(latest_in_mo))
554    }
555
556    /// Add the given write to the store buffer. (Does not change machine memory.)
557    ///
558    /// `init` says with which value to initialize the store buffer in case there wasn't a store
559    /// buffer for this memory range before.
560    ///
561    /// Must be called *after* `validate_atomic_store` to ensure that `sync_clock` is up-to-date.
562    fn buffered_atomic_write(
563        &mut self,
564        val: Scalar,
565        dest: &MPlaceTy<'tcx>,
566        atomic: AtomicWriteOrd,
567        init: Option<Scalar>,
568    ) -> InterpResult<'tcx> {
569        let this = self.eval_context_mut();
570        let (alloc_id, base_offset, ..) = this.ptr_get_alloc_id(dest.ptr(), 0)?;
571        if let (
572            crate::AllocExtra {
573                data_race: AllocDataRaceHandler::Vclocks(data_race_clocks, Some(alloc_buffers)),
574                ..
575            },
576            crate::MiriMachine {
577                data_race: GlobalDataRaceHandler::Vclocks(global), threads, ..
578            },
579        ) = this.get_alloc_extra_mut(alloc_id)?
580        {
581            if atomic == AtomicWriteOrd::SeqCst {
582                global.sc_write(threads);
583            }
584
585            let range = alloc_range(base_offset, dest.layout.size);
586            // It's a bit annoying that we have to go back to the data race part to get the clock...
587            // but it does make things a lot simpler.
588            let sync_clock = data_race_clocks.sync_clock(range);
589            let buffer = alloc_buffers.get_or_create_store_buffer_mut(range, init)?;
590            buffer.buffered_write(
591                val,
592                global,
593                threads,
594                atomic == AtomicWriteOrd::SeqCst,
595                sync_clock,
596            )?;
597        }
598
599        // Caller should've written to dest with the vanilla scalar write, we do nothing here
600        interp_ok(())
601    }
602
603    /// Caller should never need to consult the store buffer for the latest value.
604    /// This function is used exclusively for failed atomic_compare_exchange_scalar
605    /// to perform load_impl on the latest store element
606    fn perform_read_on_buffered_latest(
607        &self,
608        place: &MPlaceTy<'tcx>,
609        atomic: AtomicReadOrd,
610    ) -> InterpResult<'tcx> {
611        let this = self.eval_context_ref();
612
613        if let Some(global) = this.machine.data_race.as_vclocks_ref() {
614            if atomic == AtomicReadOrd::SeqCst {
615                global.sc_read(&this.machine.threads);
616            }
617            let size = place.layout.size;
618            let (alloc_id, base_offset, ..) = this.ptr_get_alloc_id(place.ptr(), 0)?;
619            if let Some(alloc_buffers) =
620                this.get_alloc_extra(alloc_id)?.data_race.as_weak_memory_ref()
621            {
622                let Some(buffer) =
623                    alloc_buffers.get_store_buffer(alloc_range(base_offset, size))?
624                else {
625                    // No store buffer, nothing to do.
626                    return interp_ok(());
627                };
628                buffer.read_from_last_store(
629                    global,
630                    &this.machine.threads,
631                    atomic == AtomicReadOrd::SeqCst,
632                );
633            }
634        }
635        interp_ok(())
636    }
637}