Miri now produces relaxed memory effects

270 points cbeuw

Did you know that you can read outdated values? The C++ Standard says you can, and so does Miri!

The latest Miri can produce a wide range of relaxed atomics behaviours allowed under the C++11 memory model, on which Rust piggybacks. You do not need to do anything to see them, it's enabled by default.

Edit: I just realised the latest Miri isn't available through the nightly channel yet 😅. You could either checkout Miri's source and compile yourself or wait a couple days for the release to catch up

If you cargo miri run this program

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

pub fn main() {
    static X: AtomicUsize = AtomicUsize::new(0);
    static T1_DONE: AtomicBool = AtomicBool::new(false);

    let t1 = spawn(move || {
        X.store(1, Relaxed);
        X.store(2, Relaxed);
        X.store(3, Relaxed);
        println!("written {}", X.load(Relaxed));

        T1_DONE.store(true, Relaxed);
    });

    while !T1_DONE.load(Relaxed) {
        std::hint::spin_loop();
    }

    let r = X.load(Relaxed);

    t1.join().unwrap();

    println!("read {r}");
}

You'll see the output

written 3
read 1

How come we read 1 after 2 and 3 has already been written? The read clearly executed after both stores since we waited for T1_DONE

It is in fact impossible to explain this behaviour as concurrent interleaving of threads ("interleaving semantics"):

     T1        main thread
   x <- 1
                 x == 1  // Clearly we can only read x between the two writes
   x <- 2
   x <- 3
done <- true   
              done == true // ??? but this must come before x == 1 !

​

     T1        main thread
   x <- 1
   x <- 2
   x <- 3
done <- true   
              done == true // Clearly done is only true after T1 is finished
                 x == 1 // ??? but 3 was last written to x !

These sort of behaviours is called weak or relaxed memory effects. In this particular case, using Relaxed ordering to access T1_DONE produces no synchronisation. The fact that the main thread sees T1_DONE being true has no implication on what values it may observe at other memory locations. The compiler and CPU are therefore free to reorder instructions, or keep values in local caches unobservable to threads running on other cores. Some CPU architectures are stricter than others: if you compile the program to run natively on x86(\_64), you'll always see 3 being read, but you may see 1 or 2 on ARM or Power ISA.

If you want to know more about the details, read the fine print atop https://github.com/rust-lang/miri/blob/master/src/concurrency/weak\_memory.rs

Or if you are boring and don't like chaos :(, you can disable this with -Zmiri-disable-weak-memory-emulation