Skip to content

Miri subtree update #134784

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
bors merged 19 commits into from
Dec 26, 2024
Merged

Miri subtree update #134784

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
f9e9856
add more tests for SC access/fence consistency
RalfJung Dec 12, 2024
7b29daf
Merge pull request #4090 from RalfJung/sc-test
RalfJung Dec 21, 2024
9c87ec8
remove an unused helper method
RalfJung Dec 21, 2024
58ad698
Merge pull request #4103 from RalfJung/remove-unused
RalfJung Dec 21, 2024
38e3ebc
miri-script: support saving bench results in a baseline JSON file
RalfJung Dec 22, 2024
40b3310
miri-script: add option to compare with baseline results
RalfJung Dec 22, 2024
41f3edc
CONTRIBUTING: explain how to do benchmarking with a baseline
RalfJung Dec 22, 2024
bba6f0a
Merge pull request #4104 from RalfJung/bench
RalfJung Dec 22, 2024
d80f319
add -Zmiri-many-seeds flag to the driver itself
RalfJung Dec 23, 2024
0bd76e1
remove many-seeds mode from cargo-miri
RalfJung Dec 23, 2024
d04b972
remove --many-seeds from ./miri run
RalfJung Dec 23, 2024
0f49f0f
stop using process-wide state, now that we are running multiple inter…
RalfJung Dec 23, 2024
4116585
many-seeds: add flag to keep going even after we found a failing seed
RalfJung Dec 23, 2024
fdfd064
use std::sync::Once instead of hand-rolling a bad version of it
RalfJung Dec 23, 2024
cb73bb6
Merge pull request #4105 from RalfJung/many-seeds
oli-obk Dec 23, 2024
2de4561
show an error on some invalid flag combinations: TB + permissive prov…
RalfJung Dec 24, 2024
b109091
remove some flags that have been hard errors for a while
RalfJung Dec 24, 2024
35f10b1
we generally make later flags overwrite earlier flags, so remove some…
RalfJung Dec 24, 2024
60e3bf4
Merge pull request #4109 from RalfJung/flags
RalfJung Dec 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
add more tests for SC access/fence consistency
  • Loading branch information
@RalfJung
RalfJung committed Dec 18, 2024
commit f9e98561ec7af22271e24390777f957c3fabdf71
205 changes: 1 addition & 204 deletions src/tools/miri/tests/pass/0weak_memory_consistency.rs
View file
Open in desktop
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