[Brainstorming] Is there a body of research on ownership equivalent to Stacked Borrows

Ownership in Rust is entirely a type system fiction. If you only look at the language and its operational semantics ("what happens when you run Rust code"), then there is no ownership. The only thing that exists on that level is the "aliasing model" (of which Stacked Borrows is the most worked-out proposal). Another way to say this it to note that Miri knows nothing about ownership.

The "memory model" of Rust (at least in the way I know that term) likewise has nothing to do with ownership. A "memory model" answers the question: when you read from address a, what are the possible values that you can see? With concurrency, that is a non-trivial question. Rust uses the C++ memory model for that. The sequential part of Rust's memory model is unfortunately not specified very much; the only thing I am aware of is my write-up of Rust's "memory interface". This is not a memory model, this just defines more precisely the interface that a memory model "implements". In Rust, I envision this interface to be fairly simple, directly exposing a bunch of bytes for each allocated block. (This is very unlike C/C++ where memory is typed and addressed through logical "paths" besides addresses.) The main complication here is that in Rust/C/C++, bytes are weird. But this also means that the memory model is very simple aside from concurrency: it just stores those bytes, and retrieves them on a read.

So, coming back to your question... I'm afraid I don't understand what you are asking. Ownership in Rust is basically whatever you make it. When you define your own type, you get to define its datastructure invariants, and the ownership represented by that type is part of said invariant. (This is probably the hardest thing to grok here. It is based on "separation logic", an ingenious approach that lets you talk about ownership in the same way that we usually talk about normal mathematical properties.) You need to ensure that the invariant and its ownership are properly maintained by all public functions, of course, but that's about it. Types like Rc/Arc (mentioned above) demonstrate that this mechanism indeed lets you stretch the notion of "ownership" quite far. Unless you are using primitive types such as Box, &mut, &, you can do whatever you want inside your data structure, as long as a safe client cannot cause UB. If you are using primitive types, you have to follow their rules (such as aliasing rules).

Maybe it would help if you had a concrete, small example?

17 Likes