Skip to content

Commit

Permalink
Comments addressing deviations from paper's operational semantics
Browse files Browse the repository at this point in the history
  • Loading branch information
cbeuw committed Feb 2, 2022
1 parent dbde843 commit 1b73d67
Showing 1 changed file with 13 additions and 9 deletions.
22 changes: 13 additions & 9 deletions src/weak_memory.rs
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,16 @@ impl Default for StoreBuffer {
}
}

// Operational semantics in the paper has several problems:
// 1. Store elements keep a copy of the atomic object's vector clock (AtomicCellClocks::sync_vector in miri),
// but this is not used anywhere so it's omitted
// 2. §4.5 of the paper wants an SC store to mark all existing stores in the buffer that happens before it
// as SC. This is not done in the operational semantics but implemented correctly in tsan11
// (https://github.com/ChrisLidbury/tsan11/blob/ecbd6b81e9b9454e01cba78eb9d88684168132c7/lib/tsan/rtl/tsan_relaxed.cc#L160-L167)
// 3. W_SC ; R_SC case requires the SC load to ignore all but last store maked SC (stores not marked SC are not
// affected). But this rule is applied to all loads in ReadsFromSet (last two lines of code), not just SC load.
// This is implemented correctly in tsan11
// (https://github.com/ChrisLidbury/tsan11/blob/ecbd6b81e9b9454e01cba78eb9d88684168132c7/lib/tsan/rtl/tsan_relaxed.cc#L295)
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
Expand All @@ -134,7 +144,7 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
if !keep_searching {
return false;
}
// CoWR: if a store in modification order happens-before the current load,
// CoWR: if a store happens-before the current load,
// then we can't read-from anything earlier in modification order.
if store_elem.timestamp <= clocks.clock[store_elem.store_index] {
log::info!("Stopped due to coherent write-read");
Expand Down Expand Up @@ -196,9 +206,7 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
candidates.choose(rng)
}

/// ATOMIC STORE IMPL in the paper
/// The paper also wants the variable's clock (AtomicMemoryCellClocks::sync_vector in our code)
/// to be in the store element, but it's not used anywhere so we don't actually need it
/// ATOMIC STORE IMPL in the paper (except we don't need the location's vector clock)
fn store_impl(
&mut self,
val: ScalarMaybeUninit<Tag>,
Expand All @@ -223,12 +231,8 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
}
if is_seqcst {
// Every store that happens before this needs to be marked as SC
// so that in fetch_store, only the last SC store (i.e. this one) or stores that
// so that in a later SC load, only the last SC store (i.e. this one) or stores that
// aren't ordered by hb with the last SC is picked.
//
// This is described in the paper (§4.5) and implemented in tsan11
// (https://github.com/ChrisLidbury/tsan11/blob/ecbd6b81e9b9454e01cba78eb9d88684168132c7/lib/tsan/rtl/tsan_relaxed.cc#L160-L167)
// but absent in the operational semantics.
self.buffer.iter_mut().rev().for_each(|elem| {
if elem.timestamp <= thread_clock[elem.store_index] {
elem.is_seqcst = true;
Expand Down

0 comments on commit 1b73d67

Please sign in to comment.