1 //@compile-flags: -Zmiri-ignore-leaks -Zmiri-disable-stacked-borrows
3 // The following tests check whether our weak memory emulation produces
4 // any inconsistent execution outcomes
6 // Due to the random nature of choosing valid stores, it is always
7 // possible that our tests spuriously succeeds: even though our weak
8 // memory emulation code has incorrectly identified a store in
9 // modification order as being valid, it may be never chosen by
10 // the RNG and never observed in our tests.
12 // To mitigate this, each test is ran enough times such that the chance
13 // of spurious success is very low. These tests never supriously fail.
15 // Test cases and their consistent outcomes are from
16 // http://svr-pes20-cppmem.cl.cam.ac.uk/cppmem/
18 // M. Batty, S. Owens, S. Sarkar, P. Sewell and T. Weber,
19 // "Mathematizing C++ concurrency", ACM SIGPLAN Notices, vol. 46, no. 1, pp. 55-66, 2011.
20 // Available: https://ss265.host.cs.st-andrews.ac.uk/papers/n3132.pdf.
22 use std::sync::atomic::Ordering::*;
23 use std::sync::atomic::{fence, AtomicBool, AtomicI32};
24 use std::thread::spawn;
26 #[derive(Copy, Clone)]
27 struct EvilSend<T>(pub T);
29 unsafe impl<T> Send for EvilSend<T> {}
30 unsafe impl<T> Sync for EvilSend<T> {}
32 // We can't create static items because we need to run each test
34 fn static_atomic(val: i32) -> &'static AtomicI32 {
35 let ret = Box::leak(Box::new(AtomicI32::new(val)));
36 ret.store(val, Relaxed); // work around https://github.com/rust-lang/miri/issues/2164
39 fn static_atomic_bool(val: bool) -> &'static AtomicBool {
40 let ret = Box::leak(Box::new(AtomicBool::new(val)));
41 ret.store(val, Relaxed); // work around https://github.com/rust-lang/miri/issues/2164
45 // Spins until it acquires a pre-determined value.
46 fn acquires_value(loc: &AtomicI32, val: i32) -> i32 {
47 while loc.load(Acquire) != val {
48 std::hint::spin_loop();
54 let x = static_atomic(0);
55 let y = static_atomic(0);
57 let j1 = spawn(move || {
63 let j2 = spawn(move || {
64 let r2 = x.load(Relaxed); // -------------------------------------+
65 y.store(1, Release); // ---------------------+ |
68 #[rustfmt::skip] // |synchronizes-with |happens-before
69 let j3 = spawn(move || { // | |
70 acquires_value(&y, 1); // <------------------+ |
71 x.load(Relaxed) // <----------------------------------------------+
72 // The two reads on x are ordered by hb, so they cannot observe values
73 // differently from the modification order. If the first read observed
74 // 2, then the second read must observe 2 as well.
78 let r2 = j2.join().unwrap();
79 let r3 = j3.join().unwrap();
86 let x = static_atomic(0);
87 let y = static_atomic(0);
90 let j1 = spawn(move || {
91 x.store(1, Release); // ---------------------+---------------------+
93 #[rustfmt::skip] // |synchronizes-with |
94 let j2 = spawn(move || { // | |
95 acquires_value(&x, 1); // <------------------+ |
96 y.store(1, Release); // ---------------------+ |happens-before
98 #[rustfmt::skip] // |synchronizes-with |
99 let j3 = spawn(move || { // | |
100 acquires_value(&y, 1); // <------------------+ |
101 x.load(Relaxed) // <-----------------------------------------------+
106 let r3 = j3.join().unwrap();
111 fn test_message_passing() {
113 let ptr = &mut var as *mut u32;
114 let x = EvilSend(ptr);
115 let y = static_atomic(0);
118 let j1 = spawn(move || {
119 unsafe { *x.0 = 1 }; // -----------------------------------------+
120 y.store(1, Release); // ---------------------+ |
122 #[rustfmt::skip] // |synchronizes-with | happens-before
123 let j2 = spawn(move || { // | |
124 acquires_value(&y, 1); // <------------------+ |
125 unsafe { *x.0 } // <---------------------------------------------+
129 let r2 = j2.join().unwrap();
134 // LB+acq_rel+acq_rel
135 fn test_load_buffering_acq_rel() {
136 let x = static_atomic(0);
137 let y = static_atomic(0);
138 let j1 = spawn(move || {
139 let r1 = x.load(Acquire);
144 let j2 = spawn(move || {
145 let r2 = y.load(Acquire);
150 let r1 = j1.join().unwrap();
151 let r2 = j2.join().unwrap();
153 // 3 consistent outcomes: (0,0), (0,1), (1,0)
154 assert_ne!((r1, r2), (1, 1));
157 fn test_mixed_access() {
162 x.store(1, mo_relaxed);
165 x.store(2, mo_relaxed);
168 r1 = x.load(mo_relaxed);
174 let x = static_atomic(0);
184 let r2 = spawn(move || x.load(Relaxed)).join().unwrap();
189 // The following two tests are taken from Repairing Sequential Consistency in C/C++11
191 // https://plv.mpi-sws.org/scfix/paper.pdf
194 fn test_sc_store_buffering() {
195 let x = static_atomic(0);
196 let y = static_atomic(0);
198 let j1 = spawn(move || {
203 let j2 = spawn(move || {
208 let a = j1.join().unwrap();
209 let b = j2.join().unwrap();
211 assert_ne!((a, b), (0, 0));
214 fn test_single_thread() {
215 let x = AtomicI32::new(42);
217 assert_eq!(x.load(Relaxed), 42);
219 x.store(43, Relaxed);
221 assert_eq!(x.load(Relaxed), 43);
224 fn test_sync_through_rmw_and_fences() {
225 // Example from https://github.com/llvm/llvm-project/issues/56450#issuecomment-1183695905
227 pub fn rdmw(storing: &AtomicI32, sync: &AtomicI32, loading: &AtomicI32) -> i32 {
228 storing.store(1, Relaxed);
230 sync.fetch_add(0, Relaxed);
232 loading.load(Relaxed)
235 let x = static_atomic(0);
236 let y = static_atomic(0);
237 let z = static_atomic(0);
239 // Since each thread is so short, we need to make sure that they truely run at the same time
240 // Otherwise t1 will finish before t2 even starts
241 let go = static_atomic_bool(false);
243 let t1 = spawn(move || {
244 while !go.load(Relaxed) {}
248 let t2 = spawn(move || {
249 while !go.load(Relaxed) {}
253 go.store(true, Relaxed);
255 let a = t1.join().unwrap();
256 let b = t2.join().unwrap();
257 assert_ne!((a, b), (0, 0));
260 // Test case by @SabrinaJewson
261 // https://github.com/rust-lang/miri/issues/2301#issuecomment-1221502757
262 // Demonstrating C++20 SC access changes
263 fn test_iriw_sc_rlx() {
264 let x = static_atomic_bool(false);
265 let y = static_atomic_bool(false);
267 x.store(false, Relaxed);
268 y.store(false, Relaxed);
270 let a = spawn(move || x.store(true, Relaxed));
271 let b = spawn(move || y.store(true, Relaxed));
272 let c = spawn(move || {
273 while !x.load(SeqCst) {}
276 let d = spawn(move || {
277 while !y.load(SeqCst) {}
283 let c = c.join().unwrap();
284 let d = d.join().unwrap();
291 test_single_thread();
293 test_load_buffering_acq_rel();
294 test_message_passing();
297 test_sc_store_buffering();
298 test_sync_through_rmw_and_fences();