ensure we do not see the inconsistent execution from Figure 8

Author: RalfJung

src/tools/miri/tests/pass/0weak_memory_consistency.rs

@@ -49,7 +49,8 @@ fn spin_until_bool(loc: &AtomicBool, ord: Ordering, val: bool) -> bool {
     val
 }
 
-/// Test matching https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf, Figure 7
+/// Test matching https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf, Figure 7.
+/// (The Figure 8 test is in `weak_memory/weak.rs`.)
 fn test_corr() {
     let x = static_atomic(0);
     let y = static_atomic(0);

src/tools/miri/tests/pass/weak_memory/weak.rs

@@ -69,6 +69,9 @@ fn seq_cst() -> bool {
     j2.join().unwrap();
     let r3 = j3.join().unwrap();
 
+    // Even though we force t3 to run last, it can still see the value 1.
+    // And it can *never* see the value 2!
+    assert!(r3 == 1 || r3 == 3);
     r3 == 1
 }
 
@@ -148,4 +151,9 @@ pub fn main() {
     assert_once(|| initialization_write(false));
     assert_once(|| initialization_write(true));
     assert_once(faa_replaced_by_load);
+
+    // Run seq_cst a few more times since it has an assertion we want to ensure holds always.
+    for _ in 0..50 {
+        seq_cst();
+    }
 }