Types as Contracts

[RalfJung]

@hanna-kruppe

if I have a raw pointer and somehow know nobody else is accessing it currently, then I should be able to just access it, no questions asked.

Now that's funny, because I fully agree with this. It is exactly this kind of thinking which lead me to a model that uses no provenance tracking, a model where a pointer really is just a location in memory and does not also carry some "magic" meta-data about how it was computed. For example, I think unsafe code authors will expect the following two snippets should be contextually equivalent, meaning that snippet A can be replaced by snippet B no matter the surrounding code:

// ptr1, ptr2: *mut i32
// A
if (ptr1 as usize == ptr2 as usize) {
  *ptr1 = 42;
}
// B
if (ptr1 as usize == ptr2 as usize) {
  *ptr2 = 42;
}

So, what is your (and any other unsafe code author reading this) thinking here? Is it expected/acceptable/a catastrophe for a model to ever make a distinction between the two programs above?

@hanna-kruppe

I shouldn’t have to worry about what types I have in the function signature, or the precise placement of the unsafe keyword, except insofar is necessary to ensure that my assumption (about no one else accessing the memory location) is correct. Of course, this desire is incompatible with other nice properties I want, my point is that access-based models are quite appealing to the unsafe code author in me.

My problem with this is that I do not think alias-based models provide that. They typically involve some form of provenance tracking, which means whether it is okay for you to use a pointer or not depends on how the pointer was computed. The two snippets I gave above are generally not equivalent in models that track how pointers are computed. (E.g., to use @ubsan notation, it may be that for some third pointer ptr3, we have ptr3 $ ptr1 but not ptr3 $ ptr2, so one snippet may be allowed while the other is not.)