FFI mutating raw pointer where immutable reference in scope, is this UB?

Disclaimer: there’s no formal memory model yet.

I’m going to use a simplified version of the Stacked Borrows model, which is roughly the direction that we seem to be going to what is intrinsically allowed in Rust’s memory model.

So let’s walk through what happens here:

let pointer: *mut extern = ffi_create();

We create a Raw pointer to some resource.

let ref_pointer: &(*mut extern) = &pointer

We create a Freeze reference to the pointer, pointer.

ffi_write_u8(pointer, 7);

We use the Raw pointer pointer to mutate the resource.

let integer = ffi_read_u8(*ref_pointer);

We load the Raw pointer from the Freeze reference and then load the resource behind the pointer.

assert_eq!(integer, 7);

We use our loaded value.

As the resource is behind a Raw pointer at all times, the Rust model assumes nothing about it, and it’s allowed to change at any point. The value which is unable to change because of the & borrow lock is pointer itself. (This only holds for this thread’s access; concurrent threaded access to the resource would be data race UB.)

Now, what if you had instead written

let pointer: *mut extern = ffi_create();
let mut_ref: &mut extern = &*pointer;
ffi_write_u8(pointer, 7);
let integer = ffi_read_u8(mut_ref);
assert_eq!(integer, 7);

Here, because the &mut exists, the value managed by ffi_create is assumed by Rust to be unique from the creation of mut_ref to the last use of it. This is obviously not the case, as the original pointer is used in-between the creation and use of the ref. This example is UB.

cc @RalfJung, did I get this right?