From e1d35c551fde82668d7e8be8f759bd02e9b5345b Mon Sep 17 00:00:00 2001 From: Patrick-6 Date: Tue, 15 Jul 2025 10:32:19 +0200 Subject: [PATCH] Add std::hint::spin_loop() --- .../miri/tests/pass/0weak_memory_consistency.rs | 12 ++++++++++-- .../miri/tests/pass/0weak_memory_consistency_sc.rs | 12 ++++++++++-- src/tools/miri/tests/pass/weak_memory/weak.rs | 4 ++-- 3 files changed, 22 insertions(+), 6 deletions(-) diff --git a/src/tools/miri/tests/pass/0weak_memory_consistency.rs b/src/tools/miri/tests/pass/0weak_memory_consistency.rs index b33aefaf1d59..5fba54934421 100644 --- a/src/tools/miri/tests/pass/0weak_memory_consistency.rs +++ b/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) }); diff --git a/src/tools/miri/tests/pass/0weak_memory_consistency_sc.rs b/src/tools/miri/tests/pass/0weak_memory_consistency_sc.rs index 45cc5e6e7221..2c9d742a8b11 100644 --- a/src/tools/miri/tests/pass/0weak_memory_consistency_sc.rs +++ b/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) }); diff --git a/src/tools/miri/tests/pass/weak_memory/weak.rs b/src/tools/miri/tests/pass/weak_memory/weak.rs index eeab4ebf129e..569a307ab064 100644 --- a/src/tools/miri/tests/pass/weak_memory/weak.rs +++ b/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) });