Move type definitions together and clarify fetch_store on empty buffer

Author: cbeuw

src/weak_memory.rs

@@ -40,13 +40,40 @@ 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
     // Behind a RefCell because we need to allocate/remove on read access
     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