Data race false positive due to delayed allocation optimization

[RalfJung]

The following code should be fine, but Miri raises an error:

use std::sync::atomic::Ordering::*;
use std::sync::atomic::*;

static P: AtomicPtr<u8> = AtomicPtr::new(core::ptr::null_mut());

fn main() {
    // Create the local variable, and initialize it.
    let mut val: u8 = 0;

    let t1 = std::thread::spawn(|| {
        while P.load(Relaxed).is_null() {
            std::hint::spin_loop();
        }
        unsafe {
            // Initialize `*P`.
            let ptr = P.load(Relaxed);
            *ptr = 127;
        }
    });

    // Actually generate memory for the local variable.
    // This is the time its value is actually written to memory:
    // that's *after* the thread above was spawned!
    P.store(std::ptr::addr_of_mut!(val), Relaxed);
    
    // Wait for the thread to be done.
    t1.join().unwrap();

    // Read initialized value.
    assert_eq!(val, 127);
}

The issue has been described well by CAD97 here:

Without having dived into Miri, it likely is a false positive due to places not being allocated into memory until their reference is taken. It's an optimization for most cases (there's a lot of bookkeeping happening for allocations in Miri) but results in a false positive here. Assuming that's a correct assessment, the fix would be to assign a timestamp corresponding to the local place initialization when reifying into an allocation, instead of the timestamp of the reification itself.

[RalfJung]

the fix would be to assign a timestamp corresponding to the local place initialization

That's in general quite tricky, since we support this kind of delayed initialization for ScalarPair -- so we'd have to track a timestamp for each pair component. Also this breaks our usual memory abstractions pretty badly.

There's a fairly easy solution, which is to put the write done at the time of actual (late) initialization at timestamp 0. That will avoid false UB but will introduce bugs where we miss UB, such as in this example.

I think currently my preferred solution is

• Either disable "delayed init" for all mutable local variables (let mut and interior mutability). However so far we've avoided making let vs let mut actually meaningful, and with Tree Borrows it is legal to write to immutable let variables...
• Or do a static analysis when pushing the stack frame to determine upfront which locals have their address taken, so that we can put those in memory from the start.