Skip to content

Commit

Permalink
add more tests for SC access/fence consistency
Browse files Browse the repository at this point in the history
  • Loading branch information
@RalfJung
RalfJung committed Dec 12, 2024
1 parent d7822b3 commit f2e12cd
Show file tree
Hide file tree
Showing 2 changed files with 305 additions and 204 deletions.
205 changes: 1 addition & 204 deletions tests/pass/0weak_memory_consistency.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ fn static_atomic_bool(val: bool) -> &'static AtomicBool {
Box::leak(Box::new(AtomicBool::new(val)))
}

// Spins until it acquires a pre-determined value.
/// Spins until it acquires a pre-determined value.
fn loads_value(loc: &AtomicI32, ord: Ordering, val: i32) -> i32 {
while loc.load(ord) != val {
std::hint::spin_loop();
Expand Down Expand Up @@ -186,31 +186,6 @@ fn test_mixed_access() {
assert_eq!(r2, 2);
}

// The following two tests are taken from Repairing Sequential Consistency in C/C++11
// by Lahav et al.
// https://plv.mpi-sws.org/scfix/paper.pdf

// Test case SB
fn test_sc_store_buffering() {
let x = static_atomic(0);
let y = static_atomic(0);

let j1 = spawn(move || {
x.store(1, SeqCst);
y.load(SeqCst)
});

let j2 = spawn(move || {
y.store(1, SeqCst);
x.load(SeqCst)
});

let a = j1.join().unwrap();
let b = j2.join().unwrap();

assert_ne!((a, b), (0, 0));
}

fn test_single_thread() {
let x = AtomicI32::new(42);

Expand Down Expand Up @@ -257,178 +232,6 @@ fn test_sync_through_rmw_and_fences() {
assert_ne!((a, b), (0, 0));
}

// Test case by @SabrinaJewson
// https://github.com/rust-lang/miri/issues/2301#issuecomment-1221502757
// Demonstrating C++20 SC access changes
fn test_iriw_sc_rlx() {
let x = static_atomic_bool(false);
let y = static_atomic_bool(false);

let a = spawn(move || x.store(true, Relaxed));
let b = spawn(move || y.store(true, Relaxed));
let c = spawn(move || {
while !x.load(SeqCst) {}
y.load(SeqCst)
});
let d = spawn(move || {
while !y.load(SeqCst) {}
x.load(SeqCst)
});

a.join().unwrap();
b.join().unwrap();
let c = c.join().unwrap();
let d = d.join().unwrap();

assert!(c || d);
}

// Similar to `test_iriw_sc_rlx` but with fences instead of SC accesses.
fn test_cpp20_sc_fence_fix() {
let x = static_atomic_bool(false);
let y = static_atomic_bool(false);

let thread1 = spawn(|| {
let a = x.load(Relaxed);
fence(SeqCst);
let b = y.load(Relaxed);
(a, b)
});

let thread2 = spawn(|| {
x.store(true, Relaxed);
});
let thread3 = spawn(|| {
y.store(true, Relaxed);
});

let thread4 = spawn(|| {
let c = y.load(Relaxed);
fence(SeqCst);
let d = x.load(Relaxed);
(c, d)
});

let (a, b) = thread1.join().unwrap();
thread2.join().unwrap();
thread3.join().unwrap();
let (c, d) = thread4.join().unwrap();
let bad = a == true && b == false && c == true && d == false;
assert!(!bad);
}

// https://plv.mpi-sws.org/scfix/paper.pdf
// 2.2 Second Problem: SC Fences are Too Weak
fn test_cpp20_rwc_syncs() {
/*
int main() {
atomic_int x = 0;
atomic_int y = 0;
{{{ x.store(1,mo_relaxed);
||| { r1=x.load(mo_relaxed).readsvalue(1);
fence(mo_seq_cst);
r2=y.load(mo_relaxed); }
||| { y.store(1,mo_relaxed);
fence(mo_seq_cst);
r3=x.load(mo_relaxed); }
}}}
return 0;
}
*/
let x = static_atomic(0);
let y = static_atomic(0);

let j1 = spawn(move || {
x.store(1, Relaxed);
});

let j2 = spawn(move || {
loads_value(&x, Relaxed, 1);
fence(SeqCst);
y.load(Relaxed)
});

let j3 = spawn(move || {
y.store(1, Relaxed);
fence(SeqCst);
x.load(Relaxed)
});

j1.join().unwrap();
let b = j2.join().unwrap();
let c = j3.join().unwrap();

assert!((b, c) != (0, 0));
}

/// This checks that the *last* thing the SC fence does is act like a release fence.
/// See <https://github.com/rust-lang/miri/pull/4057#issuecomment-2522296601>.
fn test_sc_fence_release() {
let x = static_atomic(0);
let y = static_atomic(0);
let z = static_atomic(0);
let k = static_atomic(0);

let j1 = spawn(move || {
x.store(1, Relaxed);
fence(SeqCst);
k.store(1, Relaxed);
});
let j2 = spawn(move || {
y.store(1, Relaxed);
fence(SeqCst);
z.store(1, Relaxed);
});

let j3 = spawn(move || {
let kval = k.load(Acquire);
let yval = y.load(Relaxed);
(kval, yval)
});
let j4 = spawn(move || {
let zval = z.load(Acquire);
let xval = x.load(Relaxed);
(zval, xval)
});

j1.join().unwrap();
j2.join().unwrap();
let (kval, yval) = j3.join().unwrap();
let (zval, xval) = j4.join().unwrap();

let bad = kval == 1 && yval == 0 && zval == 1 && xval == 0;
assert!(!bad);
}

/// Test that SC fences and accesses sync correctly with each other.
fn test_sc_fence_access() {
/*
Wx1 sc
Ry0 sc
||
Wy1 rlx
SC-fence
Rx0 rlx
*/
let x = static_atomic(0);
let y = static_atomic(0);

let j1 = spawn(move || {
x.store(1, SeqCst);
y.load(SeqCst)
});
let j2 = spawn(move || {
y.store(1, Relaxed);
fence(SeqCst);
x.load(Relaxed)
});

let v1 = j1.join().unwrap();
let v2 = j2.join().unwrap();
let bad = v1 == 0 && v2 == 0;
assert!(!bad);
}

pub fn main() {
for _ in 0..50 {
test_single_thread();
Expand All @@ -437,12 +240,6 @@ pub fn main() {
test_message_passing();
test_wrc();
test_corr();
test_sc_store_buffering();
test_sync_through_rmw_and_fences();
test_iriw_sc_rlx();
test_cpp20_sc_fence_fix();
test_cpp20_rwc_syncs();
test_sc_fence_release();
test_sc_fence_access();
}
}
Loading

0 comments on commit f2e12cd

Please sign in to comment.