Externally initialized memory and the abstract machine

[anp]

What are the interactions between the rust AM and memory initialized by e.g. an operating system? For example, how in the following code does Rust know that the bytes are considered initialized (zeroed) when they are faulted in by the kernel?

    let mapping_len = 4096;
    let mapped = unsafe {
        let mmem = libc::mmap(
            std::ptr::null_mut(),
            mapping_len,
            libc::PROT_WRITE | libc::PROT_READ,
            libc::MAP_ANON | libc::MAP_PRIVATE,
            -1,
            0,
        );
        assert_ne!(mmem, libc::MAP_FAILED);
        std::slice::from_raw_parts(mmem.cast::<u8>(), mapping_len)
    };
    for &n in mapped {
        assert_eq!(n, 0);
    }

As a human I "know" the bytes are initialized to 0 because that's the behavior of MAP_ANONYMOUS on Linux.

The above code passes miri on the playground, and I think these bytes need to be considered initialized for optimizations like the implementation of vec![0; ...] to be sound. But I'm having a hard time figuring out how the AM "knows" these are initialized.

I did a bit of searching on issues/PRs here, the published UCG, and the reference, apologies if I missed an existing discussion on this topic.

[CAD97]

Roughly speaking, the AM semantics “know” because “you told it” what the semantics of your FFI call does. The implementation with raw asm! remains consistent by being maximally conservative within what you've said the block is allowed to do, but for an abstract proof you should define the effect of any FFI call outside the AM in terms of what AM operations (e.g. allocation and initialization of memory) are performed.

For Miri specifically, Miri implements OS/syscall functionality as needed. Somewhere there's a bit of code that implements useful subsets of mmap in terms of the Miri machine.

[RalfJung]

I would say that answers the question. :) Rust doesn't know, but it is possible for mmap to zero-initialize things without doing anything that would break Rust's idea of memory, so if that is what the implementation does, everything is coherent and worked fine. If mmap gained a flag to fill everything with 0x2A, that would also be fine. You just can't declare/"imagine" mmap to do anything that Rust code couldn't already do in some other way.

@anp please reopen/comment if there are further questions related to this.