Move type definitions together and clarify fetch_store on empty buffer

diff --git a/src/weak_memory.rs b/src/weak_memory.rs
index 34c669239d5b8e3ec162e1fc358591e0ddcaf61b..0d892a5b38db528ff6a9ae485877c104e8a722d7 100644 (file)
--- a/src/weak_memory.rs
+++ b/src/weak_memory.rs
@@ -40,6 +40,8 @@
 
 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 @@ pub fn get_store_buffer_mut(&mut self, range: AllocRange) -> &mut StoreBuffer {
     }
 }
 
-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 @@ pub fn buffered_write(
 
     /// 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 @@ fn store_impl(
     }
 }
 
-#[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