Update README

README.md

@@ -20,7 +20,8 @@ for example:
   or an invalid enum discriminant)
 * **Experimental**: Violations of the [Stacked Borrows] rules governing aliasing
   for reference types
-* **Experimental**: Data races (but no weak memory effects)
+* **Experimental**: Data races
+* **Experimental**: Weak memory emulation
 
 On top of that, Miri will also tell you about memory leaks: when there is memory
 still allocated at the end of the execution, and that memory is not reachable
@@ -62,9 +63,11 @@ in your program, and cannot run all programs:
   not support networking. System API support varies between targets; if you run
   on Windows it is a good idea to use `--target x86_64-unknown-linux-gnu` to get
   better support.
-* Threading support is not finished yet. E.g., weak memory effects are not
-  emulated and spin loops (without syscalls) just loop forever. There is no
-  threading support on Windows.
+* Threading support is not finished yet. E.g. spin loops (without syscalls) just
+  loop forever. There is no threading support on Windows.
+* Weak memory emulation may produce weak behaivours unobservable by compiled
+  programs running on real hardware when `SeqCst` fences are used, and it cannot
+  produce all behaviors possibly observable on real hardware.
 
 [rust]: https://www.rust-lang.org/
 [mir]: https://github.com/rust-lang/rfcs/blob/master/text/1211-mir.md
@@ -253,20 +256,20 @@ environment variable:
   Using this flag is **unsound**.
 * `-Zmiri-disable-data-race-detector` disables checking for data races.  Using
   this flag is **unsound**. This implies `-Zmiri-disable-weak-memory-emulation`.
+* `-Zmiri-disable-isolation` disables host isolation.  As a consequence,
+  the program has access to host resources such as environment variables, file
+  systems, and randomness.
 * `-Zmiri-disable-stacked-borrows` disables checking the experimental
   [Stacked Borrows] aliasing rules.  This can make Miri run faster, but it also
   means no aliasing violations will be detected.  Using this flag is **unsound**
   (but the affected soundness rules are experimental).
-* `-Zmiri-disable-weak-memory-emulation` disables the emulation of some C++11 weak
-  memory effects.
 * `-Zmiri-disable-validation` disables enforcing validity invariants, which are
   enforced by default.  This is mostly useful to focus on other failures (such
   as out-of-bounds accesses) first.  Setting this flag means Miri can miss bugs
   in your program.  However, this can also help to make Miri run faster.  Using
   this flag is **unsound**.
-* `-Zmiri-disable-isolation` disables host isolation.  As a consequence,
-  the program has access to host resources such as environment variables, file
-  systems, and randomness.
+* `-Zmiri-disable-weak-memory-emulation` disables the emulation of some C++11 weak
+  memory effects.
 * `-Zmiri-isolation-error=<action>` configures Miri's response to operations
   requiring host access while isolation is enabled. `abort`, `hide`, `warn`,
   and `warn-nobacktrace` are the supported actions. The default is to `abort`,

src/weak_memory.rs

@@ -1,26 +1,26 @@
 //! Implementation of C++11-consistent weak memory emulation using store buffers
 //! based on Dynamic Race Detection for C++ ("the paper"):
 //! https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf
-//! 
+//!
 //! This implementation will never generate weak memory behaviours forbidden by the C++11 model,
 //! but it is incapable of producing all possible weak behaviours allowed by the model. There are
 //! certain weak behaviours observable on real hardware but not while using this.
-//! 
+//!
 //! Note that this implementation does not take into account of C++20's memory model revision to SC accesses
 //! and fences introduced by P0668 (https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0668r5.html).
 //! This implementation is not fully correct under the revised C++20 model and may generate behaviours C++20
 //! disallows.
-//! 
+//!
 //! Rust follows the full C++20 memory model (except for the Consume ordering). It is therefore
 //! possible for this implementation to generate behaviours never observable when the same program is compiled and
 //! run natively. Unfortunately, no literature exists at the time of writing which proposes an implementable and C++20-compatible
 //! relaxed memory model that supports all atomic operation existing in Rust. The closest one is
 //! A Promising Semantics for Relaxed-Memory Concurrency by Jeehoon Kang et al. (https://www.cs.tau.ac.il/~orilahav/papers/popl17.pdf)
 //! However, this model lacks SC accesses and is therefore unusable by Miri (SC accesses are everywhere in library code).
-//! 
+//!
 //! If you find anything that proposes a relaxed memory model that is C++20-consistent, supports all orderings Rust's atomic accesses
 //! and fences accept, and is implementable (with operational semanitcs), please open a GitHub issue!
-//! 
+//!
 //! One characteristic of this implementation, in contrast to some other notable operational models such as ones proposed in
 //! Taming Release-Acquire Consistency by Ori Lahav et al. (https://plv.mpi-sws.org/sra/paper.pdf) or Promising Semantics noted above,
 //! is that this implementation does not require each thread to hold an isolated view of the entire memory. Here, store buffers are per-location