mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Move type definitions together and clarify fetch_store on empty buffer

Browse Source
This commit is contained in:
Andy Wang 2022-05-07 01:07:16 +01:00
parent bf7fe68fba
commit 11ca975cd8
No known key found for this signature in database
GPG Key ID: 181B49F9F38F3374
1 changed files with 32 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

59
src/weak_memory.rs
View File

@ -40,6 +40,8 @@ use crate::{
pub type AllocExtra = StoreBufferAlloc;
const STORE_BUFFER_LIMIT: usize = 128;
#[derive(Debug, Clone)]
pub struct StoreBufferAlloc {
/// Store buffer of each atomic object in this allocation
@ -47,6 +49,31 @@ pub struct StoreBufferAlloc {
store_buffer: RefCell<AllocationMap<StoreBuffer>>,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct StoreBuffer {
// Stores to this location in modification order
buffer: VecDeque<StoreElement>,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct StoreElement {
/// The identifier of the vector index, corresponding to a thread
/// that performed the store.
store_index: VectorIdx,
/// Whether this store is SC.
is_seqcst: bool,
/// The timestamp of the storing thread when it performed the store
timestamp: VTimestamp,
/// The value of this store
val: ScalarMaybeUninit<Tag>,
/// Timestamp of first loads from this store element by each thread
/// Behind a RefCell to keep load op take &self
loads: RefCell<FxHashMap<VectorIdx, VTimestamp>>,
}
impl StoreBufferAlloc {
pub fn new_allocation() -> Self {
Self { store_buffer: RefCell::new(AllocationMap::new()) }
@ -105,13 +132,6 @@ impl StoreBufferAlloc {
}
}
const STORE_BUFFER_LIMIT: usize = 128;
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct StoreBuffer {
// Stores to this location in modification order
buffer: VecDeque<StoreElement>,
}
impl Default for StoreBuffer {
fn default() -> Self {
let mut buffer = VecDeque::new();
@ -175,7 +195,11 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
/// Selects a valid store element in the buffer.
/// The buffer does not contain the value used to initialise the atomic object
/// so a fresh atomic object has an empty store buffer until an explicit store.
/// so a fresh atomic object has an empty store buffer and this function
/// will return `None`. In this case, the caller should ensure that the non-buffered
/// value from `MiriEvalContext::read_scalar()` is observed by the program, which is
/// the initial value of the atomic object. `MiriEvalContext::read_scalar()` is always
/// the latest value in modification order so it is always correct to be observed by any thread.
fn fetch_store<R: rand::Rng + ?Sized>(
&self,
is_seqcst: bool,
@ -294,25 +318,6 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
}
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct StoreElement {
/// The identifier of the vector index, corresponding to a thread
/// that performed the store.
store_index: VectorIdx,
/// Whether this store is SC.
is_seqcst: bool,
/// The timestamp of the storing thread when it performed the store
timestamp: VTimestamp,
/// The value of this store
val: ScalarMaybeUninit<Tag>,
/// Timestamp of first loads from this store element by each thread
/// Behind a RefCell to keep load op take &self
loads: RefCell<FxHashMap<VectorIdx, VTimestamp>>,
}
impl StoreElement {
/// ATOMIC LOAD IMPL in the paper
/// Unlike the operational semantics in the paper, we don't need to keep track