Add std::hint::spin_loop()

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

@@ -48,6 +48,14 @@ fn loads_value(loc: &AtomicI32, ord: Ordering, val: i32) -> i32 {
     val
 }
 
+/// Spins until it acquires a pre-determined boolean.
+fn loads_bool(loc: &AtomicBool, ord: Ordering, val: bool) -> bool {
+    while loc.load(ord) != val {
+        std::hint::spin_loop();
+    }
+    val
+}
+
 fn test_corr() {
     let x = static_atomic(0);
     let y = static_atomic(0);
@@ -216,12 +224,12 @@ fn test_sync_through_rmw_and_fences() {
     let go = static_atomic_bool(false);
 
     let t1 = spawn(move || {
-        while !go.load(Relaxed) {}
+        loads_bool(go, Relaxed, true);
         rdmw(y, x, z)
     });
 
     let t2 = spawn(move || {
-        while !go.load(Relaxed) {}
+        loads_bool(go, Relaxed, true);
         rdmw(z, x, y)
     });
 

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

@@ -27,6 +27,14 @@ fn loads_value(loc: &AtomicI32, ord: Ordering, val: i32) -> i32 {
     val
 }
 
+/// Spins until it acquires a pre-determined boolean.
+fn loads_bool(loc: &AtomicBool, ord: Ordering, val: bool) -> bool {
+    while loc.load(ord) != val {
+        std::hint::spin_loop();
+    }
+    val
+}
+
 // Test case SB taken from Repairing Sequential Consistency in C/C++11
 // by Lahav et al.
 // https://plv.mpi-sws.org/scfix/paper.pdf
@@ -60,11 +68,11 @@ fn test_iriw_sc_rlx() {
     let a = spawn(move || x.store(true, Relaxed));
     let b = spawn(move || y.store(true, Relaxed));
     let c = spawn(move || {
-        while !x.load(SeqCst) {}
+        loads_bool(x, SeqCst, true);
         y.load(SeqCst)
     });
     let d = spawn(move || {
-        while !y.load(SeqCst) {}
+        loads_bool(y, SeqCst, true);
         x.load(SeqCst)
     });
 

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

@@ -119,12 +119,12 @@ fn faa_replaced_by_load() -> bool {
     let go = static_atomic(0);
 
     let t1 = spawn(move || {
-        while go.load(Relaxed) == 0 {}
+        reads_value(go, 1);
         rdmw(y, x, z)
     });
 
     let t2 = spawn(move || {
-        while go.load(Relaxed) == 0 {}
+        reads_value(go, 1);
         rdmw(z, x, y)
     });