//@compile-flags: -Zmiri-ignore-leaks -Zmiri-fixed-schedule
// This test's runtime explodes if the GC interval is set to 1 (which we do in CI), so we
// override it internally back to the default frequency.
//@compile-flags: -Zmiri-provenance-gc=10000

// Tests showing weak memory behaviours are exhibited, even with a fixed scheule.
// We run all tests a number of times and then check that we see the desired list of outcomes.

// Spurious failure is possible, if you are really unlucky with
// the RNG and always read the latest value from the store buffer.

use std::sync::atomic::Ordering::*;
use std::sync::atomic::{AtomicUsize, fence};
use std::thread::spawn;

#[path = "../../utils/mod.rs"]
mod utils;
use utils::check_all_outcomes;

#[allow(dead_code)]
#[derive(Copy, Clone)]
struct EvilSend<T>(pub T);

unsafe impl<T> Send for EvilSend<T> {}
unsafe impl<T> Sync for EvilSend<T> {}

// We can't create static items because we need to run each test multiple times.
fn static_atomic(val: usize) -> &'static AtomicUsize {
    Box::leak(Box::new(AtomicUsize::new(val)))
}

// Spins until it reads the given value
fn spin_until(loc: &AtomicUsize, val: usize) -> usize {
    while loc.load(Relaxed) != val {
        std::hint::spin_loop();
    }
    val
}

fn relaxed() {
    check_all_outcomes([0, 1, 2], || {
        let x = static_atomic(0);
        let j1 = spawn(move || {
            x.store(1, Relaxed);
            // Preemption is disabled, so the store above will never be the
            // latest store visible to another thread.
            x.store(2, Relaxed);
        });

        let j2 = spawn(move || x.load(Relaxed));

        j1.join().unwrap();
        let r2 = j2.join().unwrap();

        // There are three possible values here: 0 (from the initial read), 1 (from the first relaxed
        // read), and 2 (the last read).
        r2
    });
}

// https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf Figure 8
fn seq_cst() {
    check_all_outcomes([1, 3], || {
        let x = static_atomic(0);

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

        let j2 = spawn(move || {
            x.store(2, SeqCst);
            x.store(3, SeqCst);
        });

        let j3 = spawn(move || x.load(SeqCst));

        j1.join().unwrap();
        j2.join().unwrap();
        let r3 = j3.join().unwrap();

        // Even though we force t3 to run last, it can still see the value 1.
        // And it can *never* see the value 2!
        r3
    });
}

fn initialization_write(add_fence: bool) {
    check_all_outcomes([11, 22], || {
        let x = static_atomic(11);

        let wait = static_atomic(0);

        let j1 = spawn(move || {
            x.store(22, Relaxed);
            // Relaxed is intentional. We want to test if the thread 2 reads the initialisation write
            // after a relaxed write
            wait.store(1, Relaxed);
        });

        let j2 = spawn(move || {
            spin_until(wait, 1);
            if add_fence {
                fence(AcqRel);
            }
            x.load(Relaxed)
        });

        j1.join().unwrap();
        let r2 = j2.join().unwrap();

        r2
    });
}

fn faa_replaced_by_load() {
    check_all_outcomes([true, false], || {
        // Example from https://github.com/llvm/llvm-project/issues/56450#issuecomment-1183695905
        pub fn rdmw(storing: &AtomicUsize, sync: &AtomicUsize, loading: &AtomicUsize) -> usize {
            storing.store(1, Relaxed);
            fence(Release);
            // sync.fetch_add(0, Relaxed);
            sync.load(Relaxed);
            fence(Acquire);
            loading.load(Relaxed)
        }

        let x = static_atomic(0);
        let y = static_atomic(0);
        let z = static_atomic(0);

        let t1 = spawn(move || rdmw(y, x, z));

        let t2 = spawn(move || rdmw(z, x, y));

        let a = t1.join().unwrap();
        let b = t2.join().unwrap();
        (a, b) == (0, 0)
    });
}

/// Checking that the weaker release sequence example from
/// <https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0982r0.html> can actually produce the
/// new behavior (`Some(0)` in our version).
fn weaker_release_sequences() {
    check_all_outcomes([None, Some(0), Some(1)], || {
        let x = static_atomic(0);
        let y = static_atomic(0);

        let t1 = spawn(move || {
            x.store(2, Relaxed);
        });
        let t2 = spawn(move || {
            y.store(1, Relaxed);
            x.store(1, Release);
            x.store(3, Relaxed);
        });
        let t3 = spawn(move || {
            if x.load(Acquire) == 3 {
                // In C++11, if we read the 3 here, and if the store of 1 was just before the store
                // of 3 in mo order (which it is because we fix the schedule), this forms a release
                // sequence, meaning we acquire the release store of 1, and we can thus never see
                // the value 0.
                // In C++20, this is no longer a release sequence, so 0 can now be observed.
                Some(y.load(Relaxed))
            } else {
                None
            }
        });

        t1.join().unwrap();
        t2.join().unwrap();
        t3.join().unwrap()
    });
}

/// Ensuring normal release sequences (with RMWs) still work correctly.
fn release_sequence() {
    check_all_outcomes([None, Some(1)], || {
        let x = static_atomic(0);
        let y = static_atomic(0);

        let t1 = spawn(move || {
            y.store(1, Relaxed);
            x.store(1, Release);
            x.swap(3, Relaxed);
        });
        let t2 = spawn(move || {
            if x.load(Acquire) == 3 {
                // If we read 3 here, we are seeing the result of the `x.swap` above, which was
                // relaxed but forms a release sequence with the `x.store`. This means there is a
                // release sequence, so we acquire the `y.store` and cannot see the original value
                // `0` any more.
                Some(y.load(Relaxed))
            } else {
                None
            }
        });

        t1.join().unwrap();
        t2.join().unwrap()
    });
}

/// Ensure that when we read from an outdated release store, we acquire its clock.
fn old_release_store() {
    check_all_outcomes([None, Some(1)], || {
        let x = static_atomic(0);
        let y = static_atomic(0);

        let t1 = spawn(move || {
            y.store(1, Relaxed);
            x.store(1, Release); // this is what we want to read from
            x.store(3, Relaxed);
        });
        let t2 = spawn(move || {
            if x.load(Acquire) == 1 {
                // We must have acquired the `y.store` so we cannot see the initial value any more.
                Some(y.load(Relaxed))
            } else {
                None
            }
        });

        t1.join().unwrap();
        t2.join().unwrap()
    });
}

pub fn main() {
    relaxed();
    seq_cst();
    initialization_write(false);
    initialization_write(true);
    faa_replaced_by_load();
    release_sequence();
    weaker_release_sequences();
    old_release_store();
}