diff --git a/src/tools/miri/src/concurrency/data_race.rs b/src/tools/miri/src/concurrency/data_race.rs index f86d1eb1dcbc..e1fc22f68549 100644 --- a/src/tools/miri/src/concurrency/data_race.rs +++ b/src/tools/miri/src/concurrency/data_race.rs @@ -108,19 +108,25 @@ pub(super) struct ThreadClockSet { fence_acquire: VClock, /// The last timestamp of happens-before relations that - /// have been released by this thread by a fence. + /// have been released by this thread by a release fence. fence_release: VClock, /// Timestamps of the last SC fence performed by each - /// thread, updated when this thread performs an SC fence + /// thread, updated when this thread performs an SC fence. + /// This is never acquired into the thread's clock, it + /// just limits which old writes can be seen in weak memory emulation. pub(super) fence_seqcst: VClock, /// Timestamps of the last SC write performed by each - /// thread, updated when this thread performs an SC fence + /// thread, updated when this thread performs an SC fence. + /// This is never acquired into the thread's clock, it + /// just limits which old writes can be seen in weak memory emulation. pub(super) write_seqcst: VClock, /// Timestamps of the last SC fence performed by each - /// thread, updated when this thread performs an SC read + /// thread, updated when this thread performs an SC read. + /// This is never acquired into the thread's clock, it + /// just limits which old writes can be seen in weak memory emulation. pub(super) read_seqcst: VClock, } diff --git a/src/tools/miri/src/concurrency/weak_memory.rs b/src/tools/miri/src/concurrency/weak_memory.rs index c610f1999f7d..7dac171b147d 100644 --- a/src/tools/miri/src/concurrency/weak_memory.rs +++ b/src/tools/miri/src/concurrency/weak_memory.rs @@ -15,6 +15,10 @@ //! Specifically, if an SC load reads from an atomic store of any ordering, then a later SC load cannot read from //! an earlier store in the location's modification order. This is to prevent creating a backwards S edge from the second //! load to the first, as a result of C++20's coherence-ordered before rules. +//! (This seems to rule out behaviors that were actually permitted by the RC11 model that C++20 +//! intended to copy (https://plv.mpi-sws.org/scfix/paper.pdf); a change was introduced when +//! translating the math to English. According to Viktor Vafeiadis, this difference is harmless. So +//! we stick to what the standard says, and allow fewer behaviors.) //! //! Rust follows the C++20 memory model (except for the Consume ordering and some operations not performable through C++'s //! `std::atomic` API). It is therefore possible for this implementation to generate behaviours never observable when the @@ -138,6 +142,7 @@ struct StoreElement { /// The timestamp of the storing thread when it performed the store timestamp: VTimestamp, + /// The value of this store. `None` means uninitialized. // FIXME: Currently, we cannot represent partial initialization. val: Option, @@ -356,9 +361,9 @@ impl<'tcx> StoreBuffer { false } else if is_seqcst && store_elem.load_info.borrow().sc_loaded { // The current SC load cannot read-before a store that an earlier SC load has observed. - // See https://github.com/rust-lang/miri/issues/2301#issuecomment-1222720427 + // See https://github.com/rust-lang/miri/issues/2301#issuecomment-1222720427. // Consequences of C++20 ยง31.4 [atomics.order] paragraph 3.1, 3.3 (coherence-ordered before) - // and 4.1 (coherence-ordered before between SC makes global total order S) + // and 4.1 (coherence-ordered before between SC makes global total order S). false } else { true