Skip to content

Commit 60fa558

Browse files
committed
Clearer boundries between alloc metadata with multiple buffers and an individual store buffer
1 parent 69c15a1 commit 60fa558

File tree

2 files changed

+36
-40
lines changed

2 files changed

+36
-40
lines changed

src/data_race.rs

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -489,8 +489,8 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
489489
global.sc_read();
490490
}
491491
let mut rng = this.machine.rng.borrow_mut();
492-
let loaded = alloc_buffers.buffered_read(
493-
alloc_range(base_offset, place.layout.size),
492+
let buffer = alloc_buffers.get_store_buffer(alloc_range(base_offset, place.layout.size));
493+
let loaded = buffer.buffered_read(
494494
global,
495495
atomic == AtomicReadOp::SeqCst,
496496
&mut *rng,
@@ -525,10 +525,9 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
525525
if atomic == AtomicWriteOp::SeqCst {
526526
global.sc_write();
527527
}
528-
let size = dest.layout.size;
529-
alloc_buffers.buffered_write(
528+
let mut buffer = alloc_buffers.get_store_buffer_mut(alloc_range(base_offset, dest.layout.size));
529+
buffer.buffered_write(
530530
val,
531-
alloc_range(base_offset, size),
532531
global,
533532
atomic == AtomicWriteOp::SeqCst,
534533
)?;
@@ -674,7 +673,8 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
674673
let (alloc_id, base_offset, ..) = this.ptr_get_alloc_id(place.ptr)?;
675674
if let Some(alloc_buffers) = this.get_alloc_extra(alloc_id)?.weak_memory.as_ref() {
676675
if global.multi_threaded.get() {
677-
alloc_buffers.read_from_last_store(alloc_range(base_offset, size), global);
676+
let buffer = alloc_buffers.get_store_buffer(alloc_range(base_offset, size));
677+
buffer.read_from_last_store(global);
678678
}
679679
}
680680
}
@@ -701,10 +701,10 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
701701
global.sc_read();
702702
global.sc_write();
703703
}
704-
let size = place.layout.size;
705-
let range = alloc_range(base_offset, size);
706-
alloc_buffers.read_from_last_store(range, global);
707-
alloc_buffers.buffered_write(new_val, range, global, atomic == AtomicRwOp::SeqCst)?;
704+
let range = alloc_range(base_offset, place.layout.size);
705+
let mut buffer = alloc_buffers.get_store_buffer_mut(range);
706+
buffer.read_from_last_store(global);
707+
buffer.buffered_write(new_val, global, atomic == AtomicRwOp::SeqCst)?;
708708
}
709709
Ok(())
710710
}

src/weak_memory.rs

Lines changed: 26 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -53,48 +53,63 @@ impl StoreBufferAlloc {
5353
}
5454

5555
/// Gets a store buffer associated with an atomic object in this allocation
56-
fn get_store_buffer(&self, range: AllocRange) -> Ref<'_, StoreBuffer> {
56+
pub fn get_store_buffer(&self, range: AllocRange) -> Ref<'_, StoreBuffer> {
5757
Ref::map(self.store_buffer.borrow(), |range_map| {
5858
let (.., store_buffer) = range_map.iter(range.start, range.size).next().unwrap();
5959
store_buffer
6060
})
6161
}
6262

63-
fn get_store_buffer_mut(&self, range: AllocRange) -> RefMut<'_, StoreBuffer> {
63+
pub fn get_store_buffer_mut(&self, range: AllocRange) -> RefMut<'_, StoreBuffer> {
6464
RefMut::map(self.store_buffer.borrow_mut(), |range_map| {
6565
let (.., store_buffer) = range_map.iter_mut(range.start, range.size).next().unwrap();
6666
store_buffer
6767
})
6868
}
6969

70+
}
71+
72+
const STORE_BUFFER_LIMIT: usize = 128;
73+
#[derive(Debug, Clone, PartialEq, Eq)]
74+
pub struct StoreBuffer {
75+
// Stores to this location in modification order
76+
buffer: VecDeque<StoreElement>,
77+
}
78+
79+
impl Default for StoreBuffer {
80+
fn default() -> Self {
81+
let mut buffer = VecDeque::new();
82+
buffer.reserve(STORE_BUFFER_LIMIT);
83+
Self { buffer }
84+
}
85+
}
86+
87+
impl<'mir, 'tcx: 'mir> StoreBuffer {
7088
/// Reads from the last store in modification order
71-
pub fn read_from_last_store<'tcx>(&self, range: AllocRange, global: &GlobalState) {
72-
let store_buffer = self.get_store_buffer(range);
73-
let store_elem = store_buffer.buffer.back();
89+
pub fn read_from_last_store(&self, global: &GlobalState) {
90+
let store_elem = self.buffer.back();
7491
if let Some(store_elem) = store_elem {
7592
let (index, clocks) = global.current_thread_state();
7693
store_elem.load_impl(index, &clocks);
7794
}
7895
}
7996

80-
pub fn buffered_read<'tcx>(
97+
pub fn buffered_read(
8198
&self,
82-
range: AllocRange,
8399
global: &GlobalState,
84100
is_seqcst: bool,
85101
rng: &mut (impl rand::Rng + ?Sized),
86102
validate: impl FnOnce() -> InterpResult<'tcx>,
87103
) -> InterpResult<'tcx, Option<ScalarMaybeUninit<Tag>>> {
88104
// Having a live borrow to store_buffer while calling validate_atomic_load is fine
89105
// because the race detector doesn't touch store_buffer
90-
let store_buffer = self.get_store_buffer(range);
91106

92107
let store_elem = {
93108
// The `clocks` we got here must be dropped before calling validate_atomic_load
94109
// as the race detector will update it
95110
let (.., clocks) = global.current_thread_state();
96111
// Load from a valid entry in the store buffer
97-
store_buffer.fetch_store(is_seqcst, &clocks, &mut *rng)
112+
self.fetch_store(is_seqcst, &clocks, &mut *rng)
98113
};
99114

100115
// Unlike in write_scalar_atomic, thread clock updates have to be done
@@ -110,37 +125,18 @@ impl StoreBufferAlloc {
110125
Ok(loaded)
111126
}
112127

113-
pub fn buffered_write<'tcx>(
128+
pub fn buffered_write(
114129
&mut self,
115130
val: ScalarMaybeUninit<Tag>,
116-
range: AllocRange,
117131
global: &GlobalState,
118132
is_seqcst: bool,
119133
) -> InterpResult<'tcx> {
120134
let (index, clocks) = global.current_thread_state();
121135

122-
let mut store_buffer = self.get_store_buffer_mut(range);
123-
store_buffer.store_impl(val, index, &clocks.clock, is_seqcst);
136+
self.store_impl(val, index, &clocks.clock, is_seqcst);
124137
Ok(())
125138
}
126-
}
127139

128-
const STORE_BUFFER_LIMIT: usize = 128;
129-
#[derive(Debug, Clone, PartialEq, Eq)]
130-
pub struct StoreBuffer {
131-
// Stores to this location in modification order
132-
buffer: VecDeque<StoreElement>,
133-
}
134-
135-
impl Default for StoreBuffer {
136-
fn default() -> Self {
137-
let mut buffer = VecDeque::new();
138-
buffer.reserve(STORE_BUFFER_LIMIT);
139-
Self { buffer }
140-
}
141-
}
142-
143-
impl<'mir, 'tcx: 'mir> StoreBuffer {
144140
/// Selects a valid store element in the buffer.
145141
/// The buffer does not contain the value used to initialise the atomic object
146142
/// so a fresh atomic object has an empty store buffer until an explicit store.

0 commit comments

Comments
 (0)