[edit for readability] initial version of a Stacked Borrows spec

[RalfJung]

I asked @nikomatsakis where I could put such a document, and he said this repo wouldn't be a bad place. So here you go, a description of Stacked Borrows that I intend to keep in sync with the implementation in Miri.

I don't have much experience writing specs in English as opposed to maths with lots of Greek letters, so I'd welcome feedback that helps clarify ambiguities.
However, this of course touches on all sorts of other aspects of MIR that still lack any form of specification. If I had a clone I'd make him write that spec, but the way things are I am not sure when I will have the time to write down how I think one could go about specifying a Rust abstract machine by specifying idealized MIR. (That will certainly involve defining the state of the abstract machine using Rust types so that at least that part is reasonably precise.) So I'm afraid there'll probably be some ambiguities that I cannot really resolve inside this document alone.

Also, please let's not discuss the actual content of the spec at this point. This is not intended to reflect any form of consensus amongst the UCG, it is just describing a possible aliasing model that we might eventually use as the basis of a discussion at the end of which we might have some form of consensus. This PR serves just to obtain some document matching the current implementation.

[nikomatsakis]

I wanted to leave a general concern somewhere. I feel like we have to be careful with this effort and we may wind up needing two specifications. Specifically, I am imagining that we will want the freedom to refine the definition of UB to make some things UB that did not used to be. For example, you could imagine us saying "it used to be UB to have pattern X, but we adopted an extended version of two-phase borrows and that requires us to adjust the logic to accommodate that". And yet at the same time there is clearly some kind of "core logic" that unsafe authors need to depend on.

Intuitively, I map this somewhat to the idea of constructive proofs vs negative proofs relying on contradiction, but that is probably not the best way to think about. As a simple example, I would think that if an unsafe author uses reasoning like:

• I have an &'a mut T
• I know that 'a is live during some function
• Therefore, during this function I have unique access to the T and I could (e.g.) process it in another thread

I don't have a great example of "invalid" logic yet, but I feel like there may be ways to assume that something can't happen in safe code that could later become possible.

[RalfJung]

@nikomatsakis I agree with the general concern and have some thoughts, but can we please discuss this in a separate issue or so? I explicitly did not want this PR to be about what the actual aliasing model will be, and only about whether this document is actually comprehensible for anyone but me -- and now you're starting an even more meta discussion. :/

[nikomatsakis]

OK fair enough =)

[strega-nil]

@RalfJung It's somewhat hard to read the english - would it be possible to include code for each of the algorithms given, as well as code that shows an example of where each of the steps would happen? Otherwise, seems good.

[RalfJung]

For the algorithms, well, there's code in Miri. ;) But I guess you were asking for something more like pseudocode? Fair, but that'll be quite some work, not sure when I'll get around to do that.

For examples there are my blog posts. Keeping examples up-to-date is a lot of work, so I didn't plan to have examples here.