This looks like a really nice model. I definitely like the general approach, especially the way that this takes the intptrcast model's broadcast operation and makes it significantly more local and bounded through the creation of references. And making the broadcast be on casting from reference to raw pointers neatly sidesteps all the annoying questions about comparing pointers, since that requires casts to raw pointers.
For this purpose, we tag shared references with some kind of “timestamp” indicating when it was created.
This is definitely out of scope for now, but it seems like when generalized to multiple threads, this will want to be a vector or tree clock that interacts with the happens-before relationships generated by acquire-release pairs. Which seems like it would actually fit super well and possibly make a number of data races detectable, which is super nice.
So, when a &mut is cast to *mut like above, we instead push Raw onto the stack, indicating that any raw pointer may be used to access this location.
Is this also true when a &mut gets transmuted to *mut? I can see arguments for both sides. It would be nice to have a way to cast a &mut into *mut explicitly requesting that you not open the memory location up to modification through other raw pointers, for use in ways that will never be dereferences, such as in comparisons, hash consing, and memoization.
Shared references with interior mutability do not really have any restrictions in terms of what can happen to memory, so we treat them basically like raw pointers.
I'm a little bit confused as to what you mean by "treat them basically like raw pointers". You've addressed in other comments that only the specific bytes that are within UnsafeCell are affected by this, but does that mean that Raw gets pushed when you create a reference to that location? Or just that the frozen flag is ignored?
I also think it might be worth having another marker specifically for this circumstance, i.e. when you create a shared reference to a location with interior mutability, you push a special Shared item onto the stack for the location. This would prevent other random raw pointers from the modifying or viewing area, but doesn't impose any constraints on which reference is used to access the memory. This would allow transforming
fn foo(x: *mut i32, y: &Cell<i32>) {
*x = 15;
y.set(3);
*x
}
into
fn foo(x: *mut i32, y: &Cell<i32>) {
y.set(3);
*x = 15;
15
}
This might be totally useless in practice, though, since UnsafeCell is primarily used via the get method, which creates a raw pointer. I think to actually get a benefit we'd need to add an intrinsic for "reclaiming" a piece of memory, popping off the Raw and pushing a Shared.
“Time” here is a rather abstract notion, we really just need some counter that we bump up every time a new reference is created. This gives us a unique ID for each mutable reference – and, as we have seen, for shared references we actually exploit the fact that IDs are handed out in increasing order (so that we can test if a reference was created before or after a location was frozen).
I'm a bit concerned that making tags just timestamps makes it hard to reason about moving around the creation of references. There may be no way to actually compare the timestamps of references, but that doesn't seem at all clear to me. Because of that, I don't see that it would be valid to rewrite
fn bar<'a>(baz1: &'a mut u32, baz2: &'a mut u32) -> (&'a mut u32, &'a mut u32) {
let p1 = &mut *baz1;
let p2 = &mut *baz2;
(p1, p2)
}
into
fn bar<'a>(baz1: &'a mut u32, baz2: &'a mut u32) -> (&'a mut u32, &'a mut u32) {
let p2 = &mut *baz2;
let p1 = &mut *baz1;
(p1, p2)
}
which in my mind should absolutely be valid - I don't feel like the relative time of creation of two pointers should matter.
Instead, would it work to tag pointers with a pair of a timestamp and just a fresh unique id? The timestamps remain usable for dealing with shared references, but when considering unique elements on the stack you just look at the id. These ids can be compared for equality, but aren't ordered. Then, the only moments when the time gets stepped forward when memory gets frozen, not when any reference gets created. In the example above, p1 and p2 would have the same timestamp, and reordering them would be perfectly valid.
In fact, I think in that case it might be possible to record time on a per-memory-location basis, which would mean that most timestamps would be highly unordered, making various properties about aliasing stronger. Possibly.
To be clear, these are just random ideas I'm having that might fix what I'm seeing as somewhat complicated reasoning. I'm not sure my idea would actually simplify things; it just seems like it might.
We change the tags of the mutable references to the current clock value, bumping up the clock after every tag we assign, and then we push those new tags on top of the borrow stack.
So essentially there is an implicit reborrow of every pointer passed into a function? That actually feels very natural, and might actually remove special cases since Rust already allows you to reborrow the input to a function without any extra syntax.
(this can be a function argument, but also loading it from memory or getting it as the return value of some other function)
What happens when a pointer is loaded in many individual bytes and only reconstituted later? Does the retagging happen at reconstitution time?
The idea is to put a “barrier” into the stack of all function arguments when demo5 gets called, and to make it UB to pop that barrier from the stack before demo5 returns.
Does this, in analogy to retagging, also happen when a pointer is first moved into a function through other means (reading memory, etc.)?
A nice side-effect of barriers in combination with renumbering is that even if demo4 from the previous subsection would not use its arguments at all, it would still be UB to call it with two aliasing references:
Initially, I was definitely against this being a "nice" side-effect. However, if we want it to be possible to introduce unnecessary writes to some &mut pointers (which I do for the sake of lifting writes out of loops that might have 0 iterations) and reorder accesses to &mut pointers (which I really do), it has to be UB to just pass two &mut references to an empty function:
fn baz(ref1: &mut u32, ref2: &mut u32) { }
turns into
fn baz(ref1: &mut u32, ref2: &mut u32) {
let val1 = *ref1;
*ref1 = 15;
*ref1 = val1;
let val2 = *ref2;
*ref2 = val2;
}
turns into
fn baz(ref1: &mut u32, ref2: &mut u32) {
let val1 = *ref1;
*ref1 = 15;
let val2 = *ref2;
*ref1 = val1;
*ref2 = val2;
}
which breaks on aliasing inputs. So I'm tentatively convinced although I was very skeptical of the validity-based model before. And of course being able to safely mark things as noalias is very important.
TL;DR I like this model a lot, at least on first and second read-through. It may want tweaking, but it has a lot of properties that I like.
On an irrelevant editorial note,
...while “Stacked Borrows” is (to some extend) “access”-based.
That should be "to some extent", I believe.
Did you expect a difference in behavior between 
One thing I am wondering is if there is an equivalent model that is expressed in the more axiomatic style you have been using (i.e., stating properties that shall always holds true instead of defining an "instrumented machine"). It seems to me there should be, though the barriers could make this interesting. However, I have a hard time working with axiomatic models or thinking in those terms.
