From e1d35c551fde82668d7e8be8f759bd02e9b5345b Mon Sep 17 00:00:00 2001 From: Patrick-6 Date: Tue, 15 Jul 2025 10:32:19 +0200 Subject: [PATCH 1/2] 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) }); From 9a76dde4d23371d2deef39c56ff9f22051c884f7 Mon Sep 17 00:00:00 2001 From: Patrick-6 Date: Tue, 15 Jul 2025 15:50:02 +0200 Subject: [PATCH 2/2] Make spin function naming more consistent --- .../miri/tests/pass/0weak_memory_consistency.rs | 16 ++++++++-------- .../tests/pass/0weak_memory_consistency_sc.rs | 10 +++++----- src/tools/miri/tests/pass/weak_memory/weak.rs | 8 ++++---- 3 files changed, 17 insertions(+), 17 deletions(-) diff --git a/src/tools/miri/tests/pass/0weak_memory_consistency.rs b/src/tools/miri/tests/pass/0weak_memory_consistency.rs index 5fba54934421..e4ed9675de82 100644 --- a/src/tools/miri/tests/pass/0weak_memory_consistency.rs +++ b/src/tools/miri/tests/pass/0weak_memory_consistency.rs @@ -41,7 +41,7 @@ fn static_atomic_bool(val: bool) -> &'static AtomicBool { } /// Spins until it acquires a pre-determined value. -fn loads_value(loc: &AtomicI32, ord: Ordering, val: i32) -> i32 { +fn spin_until_i32(loc: &AtomicI32, ord: Ordering, val: i32) -> i32 { while loc.load(ord) != val { std::hint::spin_loop(); } @@ -49,7 +49,7 @@ fn loads_value(loc: &AtomicI32, ord: Ordering, val: i32) -> i32 { } /// Spins until it acquires a pre-determined boolean. -fn loads_bool(loc: &AtomicBool, ord: Ordering, val: bool) -> bool { +fn spin_until_bool(loc: &AtomicBool, ord: Ordering, val: bool) -> bool { while loc.load(ord) != val { std::hint::spin_loop(); } @@ -73,7 +73,7 @@ fn test_corr() { }); // | | #[rustfmt::skip] // |synchronizes-with |happens-before let j3 = spawn(move || { // | | - loads_value(&y, Acquire, 1); // <------------+ | + spin_until_i32(&y, Acquire, 1); // <---------+ | x.load(Relaxed) // <----------------------------------------------+ // The two reads on x are ordered by hb, so they cannot observe values // differently from the modification order. If the first read observed @@ -98,12 +98,12 @@ fn test_wrc() { }); // | | #[rustfmt::skip] // |synchronizes-with | let j2 = spawn(move || { // | | - loads_value(&x, Acquire, 1); // <------------+ | + spin_until_i32(&x, Acquire, 1); // <---------+ | y.store(1, Release); // ---------------------+ |happens-before }); // | | #[rustfmt::skip] // |synchronizes-with | let j3 = spawn(move || { // | | - loads_value(&y, Acquire, 1); // <------------+ | + spin_until_i32(&y, Acquire, 1); // <---------+ | x.load(Relaxed) // <-----------------------------------------------+ }); @@ -129,7 +129,7 @@ fn test_message_passing() { #[rustfmt::skip] // |synchronizes-with | happens-before let j2 = spawn(move || { // | | let x = x; // avoid field capturing | | - loads_value(&y, Acquire, 1); // <------------+ | + spin_until_i32(&y, Acquire, 1); // <---------+ | unsafe { *x.0 } // <---------------------------------------------+ }); @@ -224,12 +224,12 @@ fn test_sync_through_rmw_and_fences() { let go = static_atomic_bool(false); let t1 = spawn(move || { - loads_bool(go, Relaxed, true); + spin_until_bool(go, Relaxed, true); rdmw(y, x, z) }); let t2 = spawn(move || { - loads_bool(go, Relaxed, true); + spin_until_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 2c9d742a8b11..937c2a8cf282 100644 --- a/src/tools/miri/tests/pass/0weak_memory_consistency_sc.rs +++ b/src/tools/miri/tests/pass/0weak_memory_consistency_sc.rs @@ -20,7 +20,7 @@ fn static_atomic_bool(val: bool) -> &'static AtomicBool { } /// Spins until it acquires a pre-determined value. -fn loads_value(loc: &AtomicI32, ord: Ordering, val: i32) -> i32 { +fn spin_until_i32(loc: &AtomicI32, ord: Ordering, val: i32) -> i32 { while loc.load(ord) != val { std::hint::spin_loop(); } @@ -28,7 +28,7 @@ fn loads_value(loc: &AtomicI32, ord: Ordering, val: i32) -> i32 { } /// Spins until it acquires a pre-determined boolean. -fn loads_bool(loc: &AtomicBool, ord: Ordering, val: bool) -> bool { +fn spin_until_bool(loc: &AtomicBool, ord: Ordering, val: bool) -> bool { while loc.load(ord) != val { std::hint::spin_loop(); } @@ -68,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 || { - loads_bool(x, SeqCst, true); + spin_until_bool(x, SeqCst, true); y.load(SeqCst) }); let d = spawn(move || { - loads_bool(y, SeqCst, true); + spin_until_bool(y, SeqCst, true); x.load(SeqCst) }); @@ -144,7 +144,7 @@ fn test_cpp20_rwc_syncs() { }); let j2 = spawn(move || { - loads_value(&x, Relaxed, 1); + spin_until_i32(&x, Relaxed, 1); fence(SeqCst); y.load(Relaxed) }); diff --git a/src/tools/miri/tests/pass/weak_memory/weak.rs b/src/tools/miri/tests/pass/weak_memory/weak.rs index 569a307ab064..199f83f05286 100644 --- a/src/tools/miri/tests/pass/weak_memory/weak.rs +++ b/src/tools/miri/tests/pass/weak_memory/weak.rs @@ -24,7 +24,7 @@ fn static_atomic(val: usize) -> &'static AtomicUsize { } // Spins until it reads the given value -fn reads_value(loc: &AtomicUsize, val: usize) -> usize { +fn spin_until(loc: &AtomicUsize, val: usize) -> usize { while loc.load(Relaxed) != val { std::hint::spin_loop(); } @@ -85,7 +85,7 @@ fn initialization_write(add_fence: bool) -> bool { }); let j2 = spawn(move || { - reads_value(wait, 1); + spin_until(wait, 1); if add_fence { fence(AcqRel); } @@ -119,12 +119,12 @@ fn faa_replaced_by_load() -> bool { let go = static_atomic(0); let t1 = spawn(move || { - reads_value(go, 1); + spin_until(go, 1); rdmw(y, x, z) }); let t2 = spawn(move || { - reads_value(go, 1); + spin_until(go, 1); rdmw(z, x, y) });