3939//! to attach store buffers to atomic objects. However, Rust follows LLVM in that it only has
4040//! 'atomic accesses'. Therefore Miri cannot know when and where atomic 'objects' are being
4141//! created or destroyed, to manage its store buffers. Instead, we hence lazily create an
42- //! atomic object on the first atomic access to a given region, and we destroy that object
43- //! on the next non-atomic or imperfectly overlapping atomic access to that region.
42+ //! atomic object on the first atomic write to a given region, and we destroy that object
43+ //! on the next non-atomic or imperfectly overlapping atomic write to that region.
4444//! These lazy (de)allocations happen in memory_accessed() on non-atomic accesses, and
45- //! get_or_create_store_buffer() on atomic accesses. This mostly works well, but it does
46- //! lead to some issues (<https://github.com/rust-lang/miri/issues/2164>).
45+ //! get_or_create_store_buffer_mut() on atomic writes.
4746//!
4847//! One consequence of this difference is that safe/sound Rust allows for more operations on atomic locations
4948//! than the C++20 atomic API was intended to allow, such as non-atomically accessing
@@ -144,11 +143,9 @@ struct StoreElement {
144143
145144 /// The timestamp of the storing thread when it performed the store
146145 timestamp : VTimestamp ,
147- /// The value of this store
148- // FIXME: this means the store must be fully initialized;
149- // we will have to change this if we want to support atomics on
150- // (partially) uninitialized data.
151- val : Scalar ,
146+ /// The value of this store. `None` means uninitialized.
147+ // FIXME: Currently, we cannot represent partial initialization.
148+ val : Option < Scalar > ,
152149
153150 /// Metadata about loads from this store element,
154151 /// behind a RefCell to keep load op take &self
@@ -170,7 +167,7 @@ impl StoreBufferAlloc {
170167
171168 /// When a non-atomic access happens on a location that has been atomically accessed
172169 /// before without data race, we can determine that the non-atomic access fully happens
173- /// after all the prior atomic accesses so the location no longer needs to exhibit
170+ /// after all the prior atomic writes so the location no longer needs to exhibit
174171 /// any weak memory behaviours until further atomic accesses.
175172 pub fn memory_accessed ( & self , range : AllocRange , global : & DataRaceState ) {
176173 if !global. ongoing_action_data_race_free ( ) {
@@ -192,37 +189,29 @@ impl StoreBufferAlloc {
192189 }
193190 }
194191
195- /// Gets a store buffer associated with an atomic object in this allocation,
196- /// or creates one with the specified initial value if no atomic object exists yet .
197- fn get_or_create_store_buffer < ' tcx > (
192+ /// Gets a store buffer associated with an atomic object in this allocation.
193+ /// Returns `None` if there is no store buffer .
194+ fn get_store_buffer < ' tcx > (
198195 & self ,
199196 range : AllocRange ,
200- init : Scalar ,
201- ) -> InterpResult < ' tcx , Ref < ' _ , StoreBuffer > > {
197+ ) -> InterpResult < ' tcx , Option < Ref < ' _ , StoreBuffer > > > {
202198 let access_type = self . store_buffers . borrow ( ) . access_type ( range) ;
203199 let pos = match access_type {
204200 AccessType :: PerfectlyOverlapping ( pos) => pos,
205- AccessType :: Empty ( pos) => {
206- let mut buffers = self . store_buffers . borrow_mut ( ) ;
207- buffers. insert_at_pos ( pos, range, StoreBuffer :: new ( init) ) ;
208- pos
209- }
210- AccessType :: ImperfectlyOverlapping ( pos_range) => {
211- // Once we reach here we would've already checked that this access is not racy.
212- let mut buffers = self . store_buffers . borrow_mut ( ) ;
213- buffers. remove_pos_range ( pos_range. clone ( ) ) ;
214- buffers. insert_at_pos ( pos_range. start , range, StoreBuffer :: new ( init) ) ;
215- pos_range. start
216- }
201+ // If there is nothing here yet, that means there wasn't an atomic write yet so
202+ // we can't return anything outdated.
203+ _ => return Ok ( None ) ,
217204 } ;
218- Ok ( Ref :: map ( self . store_buffers . borrow ( ) , |buffer| & buffer[ pos] ) )
205+ let store_buffer = Ref :: map ( self . store_buffers . borrow ( ) , |buffer| & buffer[ pos] ) ;
206+ Ok ( Some ( store_buffer) )
219207 }
220208
221- /// Gets a mutable store buffer associated with an atomic object in this allocation
209+ /// Gets a mutable store buffer associated with an atomic object in this allocation,
210+ /// or creates one with the specified initial value if no atomic object exists yet.
222211 fn get_or_create_store_buffer_mut < ' tcx > (
223212 & mut self ,
224213 range : AllocRange ,
225- init : Scalar ,
214+ init : Option < Scalar > ,
226215 ) -> InterpResult < ' tcx , & mut StoreBuffer > {
227216 let buffers = self . store_buffers . get_mut ( ) ;
228217 let access_type = buffers. access_type ( range) ;
@@ -244,10 +233,8 @@ impl StoreBufferAlloc {
244233}
245234
246235impl < ' tcx > StoreBuffer {
247- fn new ( init : Scalar ) -> Self {
236+ fn new ( init : Option < Scalar > ) -> Self {
248237 let mut buffer = VecDeque :: new ( ) ;
249- buffer. reserve ( STORE_BUFFER_LIMIT ) ;
250- let mut ret = Self { buffer } ;
251238 let store_elem = StoreElement {
252239 // The thread index and timestamp of the initialisation write
253240 // are never meaningfully used, so it's fine to leave them as 0
@@ -257,11 +244,11 @@ impl<'tcx> StoreBuffer {
257244 is_seqcst : false ,
258245 load_info : RefCell :: new ( LoadInfo :: default ( ) ) ,
259246 } ;
260- ret . buffer . push_back ( store_elem) ;
261- ret
247+ buffer. push_back ( store_elem) ;
248+ Self { buffer }
262249 }
263250
264- /// Reads from the last store in modification order
251+ /// Reads from the last store in modification order, if any.
265252 fn read_from_last_store (
266253 & self ,
267254 global : & DataRaceState ,
@@ -282,7 +269,7 @@ impl<'tcx> StoreBuffer {
282269 is_seqcst : bool ,
283270 rng : & mut ( impl rand:: Rng + ?Sized ) ,
284271 validate : impl FnOnce ( ) -> InterpResult < ' tcx > ,
285- ) -> InterpResult < ' tcx , ( Scalar , LoadRecency ) > {
272+ ) -> InterpResult < ' tcx , ( Option < Scalar > , LoadRecency ) > {
286273 // Having a live borrow to store_buffer while calling validate_atomic_load is fine
287274 // because the race detector doesn't touch store_buffer
288275
@@ -419,15 +406,15 @@ impl<'tcx> StoreBuffer {
419406 // In the language provided in the paper, an atomic store takes the value from a
420407 // non-atomic memory location.
421408 // But we already have the immediate value here so we don't need to do the memory
422- // access
423- val,
409+ // access.
410+ val : Some ( val ) ,
424411 is_seqcst,
425412 load_info : RefCell :: new ( LoadInfo :: default ( ) ) ,
426413 } ;
427- self . buffer . push_back ( store_elem) ;
428- if self . buffer . len ( ) > STORE_BUFFER_LIMIT {
414+ if self . buffer . len ( ) >= STORE_BUFFER_LIMIT {
429415 self . buffer . pop_front ( ) ;
430416 }
417+ self . buffer . push_back ( store_elem) ;
431418 if is_seqcst {
432419 // Every store that happens before this needs to be marked as SC
433420 // so that in a later SC load, only the last SC store (i.e. this one) or stores that
@@ -450,7 +437,12 @@ impl StoreElement {
450437 /// buffer regardless of subsequent loads by the same thread; if the earliest load of another
451438 /// thread doesn't happen before the current one, then no subsequent load by the other thread
452439 /// can happen before the current one.
453- fn load_impl ( & self , index : VectorIdx , clocks : & ThreadClockSet , is_seqcst : bool ) -> Scalar {
440+ fn load_impl (
441+ & self ,
442+ index : VectorIdx ,
443+ clocks : & ThreadClockSet ,
444+ is_seqcst : bool ,
445+ ) -> Option < Scalar > {
454446 let mut load_info = self . load_info . borrow_mut ( ) ;
455447 load_info. sc_loaded |= is_seqcst;
456448 let _ = load_info. timestamps . try_insert ( index, clocks. clock [ index] ) ;
@@ -479,7 +471,7 @@ pub(super) trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
479471 global. sc_write ( threads) ;
480472 }
481473 let range = alloc_range ( base_offset, place. layout . size ) ;
482- let buffer = alloc_buffers. get_or_create_store_buffer_mut ( range, init) ?;
474+ let buffer = alloc_buffers. get_or_create_store_buffer_mut ( range, Some ( init) ) ?;
483475 buffer. read_from_last_store ( global, threads, atomic == AtomicRwOrd :: SeqCst ) ;
484476 buffer. buffered_write ( new_val, global, threads, atomic == AtomicRwOrd :: SeqCst ) ?;
485477 }
@@ -492,47 +484,55 @@ pub(super) trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
492484 atomic : AtomicReadOrd ,
493485 latest_in_mo : Scalar ,
494486 validate : impl FnOnce ( ) -> InterpResult < ' tcx > ,
495- ) -> InterpResult < ' tcx , Scalar > {
487+ ) -> InterpResult < ' tcx , Option < Scalar > > {
496488 let this = self . eval_context_ref ( ) ;
497- if let Some ( global) = & this. machine . data_race {
498- let ( alloc_id, base_offset, ..) = this. ptr_get_alloc_id ( place. ptr ( ) , 0 ) ?;
499- if let Some ( alloc_buffers) = this. get_alloc_extra ( alloc_id) ?. weak_memory . as_ref ( ) {
500- if atomic == AtomicReadOrd :: SeqCst {
501- global. sc_read ( & this. machine . threads ) ;
502- }
503- let mut rng = this. machine . rng . borrow_mut ( ) ;
504- let buffer = alloc_buffers. get_or_create_store_buffer (
505- alloc_range ( base_offset, place. layout . size ) ,
506- latest_in_mo,
507- ) ?;
508- let ( loaded, recency) = buffer. buffered_read (
509- global,
510- & this. machine . threads ,
511- atomic == AtomicReadOrd :: SeqCst ,
512- & mut * rng,
513- validate,
514- ) ?;
515- if global. track_outdated_loads && recency == LoadRecency :: Outdated {
516- this. emit_diagnostic ( NonHaltingDiagnostic :: WeakMemoryOutdatedLoad {
517- ptr : place. ptr ( ) ,
518- } ) ;
489+ ' fallback: {
490+ if let Some ( global) = & this. machine . data_race {
491+ let ( alloc_id, base_offset, ..) = this. ptr_get_alloc_id ( place. ptr ( ) , 0 ) ?;
492+ if let Some ( alloc_buffers) = this. get_alloc_extra ( alloc_id) ?. weak_memory . as_ref ( ) {
493+ if atomic == AtomicReadOrd :: SeqCst {
494+ global. sc_read ( & this. machine . threads ) ;
495+ }
496+ let mut rng = this. machine . rng . borrow_mut ( ) ;
497+ let Some ( buffer) = alloc_buffers
498+ . get_store_buffer ( alloc_range ( base_offset, place. layout . size ) ) ?
499+ else {
500+ // No old writes available, fall back to base case.
501+ break ' fallback;
502+ } ;
503+ let ( loaded, recency) = buffer. buffered_read (
504+ global,
505+ & this. machine . threads ,
506+ atomic == AtomicReadOrd :: SeqCst ,
507+ & mut * rng,
508+ validate,
509+ ) ?;
510+ if global. track_outdated_loads && recency == LoadRecency :: Outdated {
511+ this. emit_diagnostic ( NonHaltingDiagnostic :: WeakMemoryOutdatedLoad {
512+ ptr : place. ptr ( ) ,
513+ } ) ;
514+ }
515+
516+ return Ok ( loaded) ;
519517 }
520-
521- return Ok ( loaded) ;
522518 }
523519 }
524520
525521 // Race detector or weak memory disabled, simply read the latest value
526522 validate ( ) ?;
527- Ok ( latest_in_mo)
523+ Ok ( Some ( latest_in_mo) )
528524 }
529525
526+ /// Add the given write to the store buffer. (Does not change machine memory.)
527+ ///
528+ /// `init` says with which value to initialize the store buffer in case there wasn't a store
529+ /// buffer for this memory range before.
530530 fn buffered_atomic_write (
531531 & mut self ,
532532 val : Scalar ,
533533 dest : & MPlaceTy < ' tcx > ,
534534 atomic : AtomicWriteOrd ,
535- init : Scalar ,
535+ init : Option < Scalar > ,
536536 ) -> InterpResult < ' tcx > {
537537 let this = self . eval_context_mut ( ) ;
538538 let ( alloc_id, base_offset, ..) = this. ptr_get_alloc_id ( dest. ptr ( ) , 0 ) ?;
@@ -545,23 +545,8 @@ pub(super) trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
545545 global. sc_write ( threads) ;
546546 }
547547
548- // UGLY HACK: in write_scalar_atomic() we don't know the value before our write,
549- // so init == val always. If the buffer is fresh then we would've duplicated an entry,
550- // so we need to remove it.
551- // See https://github.com/rust-lang/miri/issues/2164
552- let was_empty = matches ! (
553- alloc_buffers
554- . store_buffers
555- . borrow( )
556- . access_type( alloc_range( base_offset, dest. layout. size) ) ,
557- AccessType :: Empty ( _)
558- ) ;
559548 let buffer = alloc_buffers
560549 . get_or_create_store_buffer_mut ( alloc_range ( base_offset, dest. layout . size ) , init) ?;
561- if was_empty {
562- buffer. buffer . pop_front ( ) ;
563- }
564-
565550 buffer. buffered_write ( val, global, threads, atomic == AtomicWriteOrd :: SeqCst ) ?;
566551 }
567552
@@ -576,7 +561,6 @@ pub(super) trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
576561 & self ,
577562 place : & MPlaceTy < ' tcx > ,
578563 atomic : AtomicReadOrd ,
579- init : Scalar ,
580564 ) -> InterpResult < ' tcx > {
581565 let this = self . eval_context_ref ( ) ;
582566
@@ -587,8 +571,12 @@ pub(super) trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
587571 let size = place. layout . size ;
588572 let ( alloc_id, base_offset, ..) = this. ptr_get_alloc_id ( place. ptr ( ) , 0 ) ?;
589573 if let Some ( alloc_buffers) = this. get_alloc_extra ( alloc_id) ?. weak_memory . as_ref ( ) {
590- let buffer = alloc_buffers
591- . get_or_create_store_buffer ( alloc_range ( base_offset, size) , init) ?;
574+ let Some ( buffer) =
575+ alloc_buffers. get_store_buffer ( alloc_range ( base_offset, size) ) ?
576+ else {
577+ // No store buffer, nothing to do.
578+ return Ok ( ( ) ) ;
579+ } ;
592580 buffer. read_from_last_store (
593581 global,
594582 & this. machine . threads ,
0 commit comments