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}