39
39
//! to attach store buffers to atomic objects. However, Rust follows LLVM in that it only has
40
40
//! 'atomic accesses'. Therefore Miri cannot know when and where atomic 'objects' are being
41
41
//! 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.
44
44
//! 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.
47
46
//!
48
47
//! One consequence of this difference is that safe/sound Rust allows for more operations on atomic locations
49
48
//! than the C++20 atomic API was intended to allow, such as non-atomically accessing
@@ -144,11 +143,9 @@ struct StoreElement {
144
143
145
144
/// The timestamp of the storing thread when it performed the store
146
145
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 > ,
152
149
153
150
/// Metadata about loads from this store element,
154
151
/// behind a RefCell to keep load op take &self
@@ -170,7 +167,7 @@ impl StoreBufferAlloc {
170
167
171
168
/// When a non-atomic access happens on a location that has been atomically accessed
172
169
/// 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
174
171
/// any weak memory behaviours until further atomic accesses.
175
172
pub fn memory_accessed ( & self , range : AllocRange , global : & DataRaceState ) {
176
173
if !global. ongoing_action_data_race_free ( ) {
@@ -192,37 +189,29 @@ impl StoreBufferAlloc {
192
189
}
193
190
}
194
191
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 > (
198
195
& self ,
199
196
range : AllocRange ,
200
- init : Scalar ,
201
- ) -> InterpResult < ' tcx , Ref < ' _ , StoreBuffer > > {
197
+ ) -> InterpResult < ' tcx , Option < Ref < ' _ , StoreBuffer > > > {
202
198
let access_type = self . store_buffers . borrow ( ) . access_type ( range) ;
203
199
let pos = match access_type {
204
200
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 ) ,
217
204
} ;
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) )
219
207
}
220
208
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.
222
211
fn get_or_create_store_buffer_mut < ' tcx > (
223
212
& mut self ,
224
213
range : AllocRange ,
225
- init : Scalar ,
214
+ init : Option < Scalar > ,
226
215
) -> InterpResult < ' tcx , & mut StoreBuffer > {
227
216
let buffers = self . store_buffers . get_mut ( ) ;
228
217
let access_type = buffers. access_type ( range) ;
@@ -244,10 +233,8 @@ impl StoreBufferAlloc {
244
233
}
245
234
246
235
impl < ' tcx > StoreBuffer {
247
- fn new ( init : Scalar ) -> Self {
236
+ fn new ( init : Option < Scalar > ) -> Self {
248
237
let mut buffer = VecDeque :: new ( ) ;
249
- buffer. reserve ( STORE_BUFFER_LIMIT ) ;
250
- let mut ret = Self { buffer } ;
251
238
let store_elem = StoreElement {
252
239
// The thread index and timestamp of the initialisation write
253
240
// are never meaningfully used, so it's fine to leave them as 0
@@ -257,11 +244,11 @@ impl<'tcx> StoreBuffer {
257
244
is_seqcst : false ,
258
245
load_info : RefCell :: new ( LoadInfo :: default ( ) ) ,
259
246
} ;
260
- ret . buffer . push_back ( store_elem) ;
261
- ret
247
+ buffer. push_back ( store_elem) ;
248
+ Self { buffer }
262
249
}
263
250
264
- /// Reads from the last store in modification order
251
+ /// Reads from the last store in modification order, if any.
265
252
fn read_from_last_store (
266
253
& self ,
267
254
global : & DataRaceState ,
@@ -282,7 +269,7 @@ impl<'tcx> StoreBuffer {
282
269
is_seqcst : bool ,
283
270
rng : & mut ( impl rand:: Rng + ?Sized ) ,
284
271
validate : impl FnOnce ( ) -> InterpResult < ' tcx > ,
285
- ) -> InterpResult < ' tcx , ( Scalar , LoadRecency ) > {
272
+ ) -> InterpResult < ' tcx , ( Option < Scalar > , LoadRecency ) > {
286
273
// Having a live borrow to store_buffer while calling validate_atomic_load is fine
287
274
// because the race detector doesn't touch store_buffer
288
275
@@ -419,15 +406,15 @@ impl<'tcx> StoreBuffer {
419
406
// In the language provided in the paper, an atomic store takes the value from a
420
407
// non-atomic memory location.
421
408
// 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 ) ,
424
411
is_seqcst,
425
412
load_info : RefCell :: new ( LoadInfo :: default ( ) ) ,
426
413
} ;
427
- self . buffer . push_back ( store_elem) ;
428
- if self . buffer . len ( ) > STORE_BUFFER_LIMIT {
414
+ if self . buffer . len ( ) >= STORE_BUFFER_LIMIT {
429
415
self . buffer . pop_front ( ) ;
430
416
}
417
+ self . buffer . push_back ( store_elem) ;
431
418
if is_seqcst {
432
419
// Every store that happens before this needs to be marked as SC
433
420
// 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 {
450
437
/// buffer regardless of subsequent loads by the same thread; if the earliest load of another
451
438
/// thread doesn't happen before the current one, then no subsequent load by the other thread
452
439
/// 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 > {
454
446
let mut load_info = self . load_info . borrow_mut ( ) ;
455
447
load_info. sc_loaded |= is_seqcst;
456
448
let _ = load_info. timestamps . try_insert ( index, clocks. clock [ index] ) ;
@@ -479,7 +471,7 @@ pub(super) trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
479
471
global. sc_write ( threads) ;
480
472
}
481
473
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) ) ?;
483
475
buffer. read_from_last_store ( global, threads, atomic == AtomicRwOrd :: SeqCst ) ;
484
476
buffer. buffered_write ( new_val, global, threads, atomic == AtomicRwOrd :: SeqCst ) ?;
485
477
}
@@ -492,47 +484,55 @@ pub(super) trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
492
484
atomic : AtomicReadOrd ,
493
485
latest_in_mo : Scalar ,
494
486
validate : impl FnOnce ( ) -> InterpResult < ' tcx > ,
495
- ) -> InterpResult < ' tcx , Scalar > {
487
+ ) -> InterpResult < ' tcx , Option < Scalar > > {
496
488
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) ;
519
517
}
520
-
521
- return Ok ( loaded) ;
522
518
}
523
519
}
524
520
525
521
// Race detector or weak memory disabled, simply read the latest value
526
522
validate ( ) ?;
527
- Ok ( latest_in_mo)
523
+ Ok ( Some ( latest_in_mo) )
528
524
}
529
525
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.
530
530
fn buffered_atomic_write (
531
531
& mut self ,
532
532
val : Scalar ,
533
533
dest : & MPlaceTy < ' tcx > ,
534
534
atomic : AtomicWriteOrd ,
535
- init : Scalar ,
535
+ init : Option < Scalar > ,
536
536
) -> InterpResult < ' tcx > {
537
537
let this = self . eval_context_mut ( ) ;
538
538
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> {
545
545
global. sc_write ( threads) ;
546
546
}
547
547
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
- ) ;
559
548
let buffer = alloc_buffers
560
549
. 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
-
565
550
buffer. buffered_write ( val, global, threads, atomic == AtomicWriteOrd :: SeqCst ) ?;
566
551
}
567
552
@@ -576,7 +561,6 @@ pub(super) trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
576
561
& self ,
577
562
place : & MPlaceTy < ' tcx > ,
578
563
atomic : AtomicReadOrd ,
579
- init : Scalar ,
580
564
) -> InterpResult < ' tcx > {
581
565
let this = self . eval_context_ref ( ) ;
582
566
@@ -587,8 +571,12 @@ pub(super) trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
587
571
let size = place. layout . size ;
588
572
let ( alloc_id, base_offset, ..) = this. ptr_get_alloc_id ( place. ptr ( ) , 0 ) ?;
589
573
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
+ } ;
592
580
buffer. read_from_last_store (
593
581
global,
594
582
& this. machine . threads ,
0 commit comments