Can we use some notion of safe reachability for legal unsafe code?

[asajeffrey]

I wrote some notes on using a notion of safe reachability for defining legal unsafe code. They are a bit of a brain-dump, and contain lots of gaps, but they might be a start. Notes on safe reachability for Rust.

[asajeffrey]

This followed on from some discussion on #21 with @RalfJung.

[RalfJung]

Considering that Rust's type system is putting a strong emphasis on ownership, which in turn is very much about spatial reasoning ("this is my memory, this is your memory"), when we talk about "trusting types", we IMHO are already talking spatially.

So maybe another way to phrase the relation to Tootsie Pop would be that unsafe code is not just restricted wrt. when it has to establish invariants again, it is also restricted wrt. which invariants it is allowed to break. Clearly, for example, if there is safe code concurrently running in another thread, the unsafe code must not do anything "bad" to the memory visible to that other thread. Reasoning about interference by other threads is complicated, but lucky enough, Rust is already very well equipped to do so :)

[asajeffrey]

@RalfJung indeed, the idea was to define something that was as close to what Rust is currently doing as possible. Is there a current definition of something like safe reachability for Rust?

In comparison to Tootsie Pop, the main difference is saying that the invariants always have to hold (because there may be concurrent threads relying on them) rather than just at call boundaries.

[RalfJung]

In comparison to Tootsie Pop, the main difference is saying that the invariants always have to hold (because there may be concurrent threads relying on them) rather than just at call boundaries.

Well, but if the unsafe code can prove that no other code can possibly observe the invariants being violated, then doing so should be fine -- if the compiler doesn't rely on them. That's what Tooties Pop is about, so I see that as complementary to your suggestion -- one covers when invariants can be violated, and the other one covers which invariants can be violated.

For example, if the unsafe code is within a function of type fn foo(x: &mut Vec<T>), it can totally rely on no other thread having any kind of access to anything (transitively) contained in that vector. So the vector's invariants don't always have to hold; they only have to be re-established before the environment (i.e., code outside the current abstraction boundary, whatever that is) can see that they have been broken.

[asajeffrey]

In your example, fn foo(x: &mut Vec<T>), the vector x isn't safely reachable for the duration of the function, so this case should already be covered. (OK, I should go over the defn of safely rechable to make sure this is true!)

[asajeffrey]

I updated the gist with a (probably wrong, but "morally right") notion of how the roots are changed by incoming/outgoing function calls/returns.