But I still do not understand why we need to invalidate UNQ, when reading from an orthogonal/parent pointer. So why is this code illegal under SB?
let mut place = 0;
let ptr = &raw mut place;
let r1 = &mut *ptr;
println!("{}", *ptr);
println!("{}", *r1);
when this is legal:
let mut place = 0;
let ptr = &raw mut place;
let r1 = &*ptr;
println!("{}", *ptr);
println!("{}", *r1);
Because Uniq is supposed to be unique. You need to do something to prevent
*p;
*r = 1;
*p;
because if you don't, that prevents write reordering and coalescing.
If you really want to make &mut _-but-not-written-through behave like & _, you need to have a two-state Uniq tag, (exactly like the two-phase borrow‽ this might actually be a meaningful insight), where once it has been written to, reading from a tag not derived from it invalidates it. You could potentially even go three-state, from pre-write to writing to post-write.
I think maybe exploring making Uniq always two-state in order to support two-phase borrows uniformly actually makes sense, but it should be explained from such an angle of "activating" the uniqueness by a write, and reads from the direct parent pointer should also be valid.
[Zulip spinoff thread for this observation.]
What is different between that tree and the stack of
U(root), U(a), U(b), SRW(c, d, e, f), U(g), U(h)
where all of the SRW shares the same tag? SB's coalescing of all pointers to share a single tag can be seen as an optimization over giving each pointer a unique tag at the same {position in the stack | depth in the tree}. Unless having the tags be disjoint has an impact on operations on the tree (and now that sibling branches aren't downgraded from SRW to SRO I don't recall any), treating the shared raw pointers as one unit seems a more useful way of modeling them. Plus, you still have to deal with pointers with the same exact tag from when they're byte-copied rather than typed-copied.
Sorry, I'm still translating between the stack and the tree constantly in my head. If I myself say above/below, I'm referring to treating the tree as if it were a stack, where the top of the stack is where you push/pop from.
Ok lets move this part to zulip.
Yes this definitely reduces the "treeiness" of the tree, but what about this:
order of creation: a, b, c, d, e
U(a)
|-- SRW(b)
| \-- SRW(d)
\-- SRW(c)
\-- SRW(e)
IIUC, the stack would look this: [U(a), SRW(b, c, d, e)]. So here the tree would also provide more information, the question still is, is this information even useful? Theoretically the tree would enable us to selectively disable c and e, if a Unq is derived from d (not current behavior). I do not know where this might be useful.
If the implementation of a tree would be simpler to understand than a stack (because it behaves more like a tree normally is used, compared to the currently non-stack-like behavior of SB), then I see this as a benefit for unsafe code writers coming in contact with this.
Another (to me weird) code snippet:
let mut place = 42;
let x = &mut place;
let p1 = x as *mut i32;
let y = &mut *p1;
let p2 = y as *mut i32;
*p2 = *p1 + 3;
println!("{}", &*y );
*p2 = *p1 + 7;
println!("{}", *y + *x);
This runs without problems under miri, but is rather unexpected. While UB should not be possible (passing p1 and x/y to a function will issue a retag and insert an appropriate protector), but I still find this weird (two consecutive reads from &mut without deriving a new pointer/writing using the original pointer yielding two different values).
Yeah, that's where I'm getting hung up, I think. I don't see the benefit to distinguishing between sibling-ish SRW tags, and see treating them uniformly as an active benefit of the existing model.
However, I do think that relaxing the current model's almost-stack to a tree with primarily stack-like operations could be beneficial (e.g. my draft of how to handle "UnsafeMutCell" and of course the DelayUniq two-phase borrow idea) but even then I think collapsing all connected SRW to a single tag is not just a useful implementation optimization but useful semantically to treat them identically.
#[allow(clippy::no_effect, unused_must_use)]
fn main() {
unsafe {
let mut place = 42;
let x = &mut place;
let p1 = x as *mut i32;
let y = &mut *p1;
let p2 = y as *mut i32;
*p2 = *p1 + 3;
&*y;
*p2 = *p1 + 7;
*y;
*x;
}
}
That fails under -Zmiri-tag-raw-pointers with
error: Undefined Behavior: trying to reborrow <1776> for SharedReadOnly permission at alloc924[0x0], but that tag does not exist in the borrow stack for this location
--> src\main.rs:10:9
|
10 | &*y;
| ^^^
| |
| trying to reborrow <1776> for SharedReadOnly permission at alloc924[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of a reborrow at alloc924[0x0..0x4]
|
What's happening is that because Miri doesn't tag raw pointers by default (they're just Untagged), the access through p1 is picking up the Untagged for p2 and using that.
For the most part, default Miri is wildly over-conservative with raw pointers, even compared to the paper's SB AIUI, which always tags raw pointers IIUC. You typically want to use -Zmiri-tag-raw-pointers or -Zmiri-strict-aliasing if the snippets aren't doing usize/pointer casts to get a fuller picture of what's going on.
rustc 1.62.0-nightly (082e4ca49 2022-04-26)
binary: rustc
commit-hash: 082e4ca49770ebc9cb0ee616f3726a67471be8cb
commit-date: 2022-04-26
host: x86_64-pc-windows-msvc
release: 1.62.0-nightly
LLVM version: 14.0.1
miri 0.1.0 (a71a008 2022-04-25)
With -Zmiri-tag-raw-pointers (-Zmiri-tag-raw-pointers -Zmiri-track-pointer-tag=1776)
7 | let y = &mut *p1;
| ^^^^^^^^ created tag 1776
9 | *p2 = *p1 + 3;
| ^^^ popped tracked tag for item [Unique for <1776>] due to Read access for <1775>
10 | &*y;
| ^^^
| |
| trying to reborrow <1776> for SharedReadOnly permission at alloc924[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of a reborrow at alloc924[0x0..0x4]
Unfortunately there's no good way to have miri dump all of the borrow stack operations on an allocation, and <untagged> can't really be tracked, so I can't exactly show what's happening without -Zmiri-tag-raw-pointers exactly. What I was able to get is (-Zmiri-track-pointer-tag=1724,1723,1725 -Zmiri-track-alloc-id=924)
5 | let x = &mut place;
| ^^^^^^^^^^ created allocation with id 924
| ^^^^^^^^^^ created tag 1723
7 | let y = &mut *p1;
| ^^^^^^^^ created tag 1724
10 | &*y;
| ^^^ created tag 1725
11 | *p2 = *p1 + 7;
| ^^^^^^^^^^^^^ popped tracked tag for item [SharedReadOnly for <1725>] due to Write access for <untagged>
13 | *x;
| ^^ popped tracked tag for item [Unique for <1724>] due to Read access for <1723>
14 | }
| ^ freed allocation with id 924
| ^ popped tracked tag for item [Disabled for <1724>] due to deallocation
| ^ popped tracked tag for item [Unique for <1723>] due to deallocation
Aw dang, should have checked with that...
Yeah, i was mostly aware of the Untagged business, good explanation!
I guess I should just set MIRIFLAGS to that permanently (I dont think I use pointer<->int crimes code when running miri, but i will see...).
Yes that optimization seems to be useful, but I also think that tracking the relation between blobs of SRW (derived from different Unq) could also have some benefit (SB already separates these groups of SRW, but does not accurately track their relation).
Why does miri not complain about this (playground):
use core::ptr;
static mut EVIL: *mut i32 = ptr::null_mut();
unsafe fn store(ptr: *mut i32) {
EVIL = ptr;
}
unsafe fn foo() {
*EVIL += 20;
}
fn main() {
unsafe {
let mut x = 0;
let x = &mut x;
let ptr = &mut *x as *mut i32;
store(ptr);
foo();
println!("{:?}", *x);
foo();
println!("{:?}", *x);
}
}
Adding let x = &*x; or let x = x; before the first foo() will produce UB.
Tracing info (rustc 1.62.0-nightly (082e4ca49 2022-04-26), MIRIFLAGS="-Zmiri-strict-provenance -Zmiri-track-pointer-tag=1773,1774,1775,1776,1777,1778 -Zmiri-track-alloc-id=924", MIRI_LOG="miri::stacked_borrows" plus a lot of manual cleanup):
#[allow(warnings)]
fn main() {
unsafe {
let mut x = 0;
let x = &mut x;
let ptr = &mut *x as *mut i32;
*ptr += 20;
&*x;
*ptr += 20;
&*x;
}
}
5 | let x = &mut x;
| ^^^^^^ created allocation with id 924
| ^^^^^^ created tag 1773
| ^^^^^^ created tag 1774
6 | let ptr = &mut *x as *mut i32;
| ^^^^^^^ created tag 1775
| ^^^^^^^ created tag 1776
8 | &*x;
| ^^^ created tag 1777
| ^^^ popped tracked tag for item [Unique for <1775>] due to Read access for <1774>
9 | *ptr += 20;
| ^^^^^^^^^^ popped tracked tag for item [SharedReadOnly for <1777>] due to Write access for <1776>
10 | &*x;
| ^^^ created tag 1778
11 | }
| ^ freed allocation with id 924
| ^ popped tracked tag for item [SharedReadOnly for <1778>] due to deallocation
| ^ popped tracked tag for item [SharedReadWrite for <1776>] due to deallocation
| ^ popped tracked tag for item [Disabled for <1775>] due to deallocation
| ^ popped tracked tag for item [Unique for <1774>] due to deallocation
| ^ popped tracked tag for item [Unique for <1773>] due to deallocation
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] New allocation alloc924 has base tag <1773>
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] write access with tag <1773>: alloc924, size 4
note: tracking was triggered
--> src\main.rs:5:17
|
5 | let x = &mut x;
| ^^^^^^ created allocation with id 924
| ^^^^^^ created tag 1773
|
= note: inside `main` at src\main.rs:5:17
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] reborrow: unique reference <1774> derived from <1773> (pointee i32): alloc924, size 4
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] reborrow: adding item [Unique for <1774>]
note: tracking was triggered
--> src\main.rs:5:17
|
5 | let x = &mut x;
| ^^^^^^ created tag 1774
|
= note: inside `main` at src\main.rs:5:17
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] reborrow: unique reference <1775> derived from <1774> (pointee i32): alloc924, size 4
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] reborrow: adding item [Unique for <1775>]
note: tracking was triggered
--> src\main.rs:6:19
|
6 | let ptr = &mut *x as *mut i32;
| ^^^^^^^ created tag 1775
|
= note: inside `main` at src\main.rs:6:19
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] reborrow: raw (mutable) reference <1776> derived from <1775> (pointee i32): alloc924, size 4
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] reborrow: adding item [SharedReadWrite for <1776>]
note: tracking was triggered
--> src\main.rs:6:19
|
6 | let ptr = &mut *x as *mut i32;
| ^^^^^^^ created tag 1776
|
= note: inside `main` at src\main.rs:6:19
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] read access with tag <1776>: alloc924, size 4
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] write access with tag <1776>: alloc924, size 4
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] read access with tag <1776>: alloc924, size 4
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] reborrow: shared reference <1777> derived from <1774> (pointee i32): alloc924, size 4
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] access: disabling item [Unique for <1775>]
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] reborrow: adding item [SharedReadOnly for <1777>]
note: tracking was triggered
--> src\main.rs:8:9
|
8 | &*x;
| ^^^ created tag 1777
| ^^^ popped tracked tag for item [Unique for <1775>] due to Read access for <1774>
|
= note: inside `main` at src\main.rs:8:9
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] read access with tag <1776>: alloc924, size 4
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] write access with tag <1776>: alloc924, size 4
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] access: popping item [SharedReadOnly for <1777>]
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] read access with tag <1776>: alloc924, size 4
note: tracking was triggered
--> src\main.rs:9:9
|
9 | *ptr += 20;
| ^^^^^^^^^^ popped tracked tag for item [SharedReadOnly for <1777>] due to Write access for <1776>
|
= note: inside `main` at src\main.rs:9:9
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] reborrow: shared reference <1778> derived from <1774> (pointee i32): alloc924, size 4
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] reborrow: adding item [SharedReadOnly for <1778>]
note: tracking was triggered
--> src\main.rs:10:9
|
10 | &*x;
| ^^^ created tag 1778
|
= note: inside `main` at src\main.rs:10:9
[2022-05-07T13:41:33Z TRACE miri::stacked_borrows] deallocation with tag <1773>: alloc924, size 4
note: tracking was triggered
--> src\main.rs:11:5
|
11 | }
| ^ freed allocation with id 924
| ^ popped tracked tag for item [SharedReadOnly for <1778>] due to deallocation
| ^ popped tracked tag for item [SharedReadWrite for <1776>] due to deallocation
| ^ popped tracked tag for item [Disabled for <1775>] due to deallocation
| ^ popped tracked tag for item [Unique for <1774>] due to deallocation
| ^ popped tracked tag for item [Unique for <1773>] due to deallocation
|
= note: inside `main` at src\main.rs:11:5
I can't parse exactly what the execution is here.
If I had to guess, something w.r.t. two-phase borrows being weird.
#[allow(warnings)]
fn main() {
unsafe {
let mut x = 0;
let x = &mut x;
let ptr = x as *mut i32;
*ptr += 20;
&*x;
*ptr += 20;
&*x;
}
}
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] New allocation alloc924 has base tag <1773>
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] write access with tag <1773>: alloc924, size 4
note: tracking was triggered
--> src\main.rs:5:17
|
5 | let x = &mut x;
| ^^^^^^ created allocation with id 924
| ^^^^^^ created tag 1773
|
= note: inside `main` at src\main.rs:5:17
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] reborrow: unique reference <1774> derived from <1773> (pointee i32): alloc924, size 4
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] reborrow: adding item [Unique for <1774>]
note: tracking was triggered
--> src\main.rs:5:17
|
5 | let x = &mut x;
| ^^^^^^ created tag 1774
|
= note: inside `main` at src\main.rs:5:17
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] reborrow: raw (mutable) reference <1775> derived from <1774> (pointee i32): alloc924, size 4
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] reborrow: adding item [SharedReadWrite for <1775>]
note: tracking was triggered
--> src\main.rs:6:19
|
6 | let ptr = x as *mut i32;
| ^ created tag 1775
|
= note: inside `main` at src\main.rs:6:19
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] read access with tag <1775>: alloc924, size 4
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] write access with tag <1775>: alloc924, size 4
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] read access with tag <1775>: alloc924, size 4
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] reborrow: shared reference <1776> derived from <1774> (pointee i32): alloc924, size 4
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] reborrow: adding item [SharedReadOnly for <1776>]
note: tracking was triggered
--> src\main.rs:8:9
|
8 | &*x;
| ^^^ created tag 1776
|
= note: inside `main` at src\main.rs:8:9
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] read access with tag <1775>: alloc924, size 4
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] write access with tag <1775>: alloc924, size 4
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] access: popping item [SharedReadOnly for <1776>]
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] read access with tag <1775>: alloc924, size 4
note: tracking was triggered
--> src\main.rs:9:9
|
9 | *ptr += 20;
| ^^^^^^^^^^ popped tracked tag for item [SharedReadOnly for <1776>] due to Write access for <1775>
|
= note: inside `main` at src\main.rs:9:9
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] reborrow: shared reference <1777> derived from <1774> (pointee i32): alloc924, size 4
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] reborrow: adding item [SharedReadOnly for <1777>]
note: tracking was triggered
--> src\main.rs:10:9
|
10 | &*x;
| ^^^ created tag 1777
|
= note: inside `main` at src\main.rs:10:9
[2022-05-07T14:06:56Z TRACE miri::stacked_borrows] deallocation with tag <1773>: alloc924, size 4
note: tracking was triggered
--> src\main.rs:11:5
|
11 | }
| ^ freed allocation with id 924
| ^ popped tracked tag for item [SharedReadOnly for <1777>] due to deallocation
| ^ popped tracked tag for item [SharedReadWrite for <1775>] due to deallocation
| ^ popped tracked tag for item [Unique for <1774>] due to deallocation
| ^ popped tracked tag for item [Unique for <1773>] due to deallocation
|
= note: inside `main` at src\main.rs:11:5
So I did some more digging and added some custom diagnostics to miri and found this:
5 | let x = &mut x;
| ^^^^^^ stack accessed using <2945>: [UNQ<2945>]
| ^^^^^^ stack updated [added <2946>] to [UNQ<2945>, UNQ<2946>]
6 | let ptr = &mut *x as *mut i32;
| ^^^^^^^ stack accessed using <2946>: [UNQ<2945>, UNQ<2946>]
| ^^^^^^^ stack updated [added <2947>] to [UNQ<2945>, UNQ<2946>, UNQ<2947>]
| ^^^^^^^ stack updated [added <2948>] to [UNQ<2945>, UNQ<2946>, UNQ<2947>, SRW<2948>]
7 | *ptr += 20;
| ^^^^^^^^^^ stack accessed using <2948>: [UNQ<2945>, UNQ<2946>, UNQ<2947>, SRW<2948>]
8 | &*x;
| ^^^ stack updated [changed <2947>] to [UNQ<2945>, UNQ<2946>, DBL<2947>, SRW<2948>]
| ^^^ stack accessed using <2946>: [UNQ<2945>, UNQ<2946>, DBL<2947>, SRW<2948>]
| ^^^ stack updated [added <2949>] to [UNQ<2945>, UNQ<2946>, DBL<2947>, SRW<2948>, SRO<2949>]
9 | *ptr += 20;
| ^^^^^^^^^^ stack accessed using <2948>: [UNQ<2945>, UNQ<2946>, DBL<2947>, SRW<2948>, SRO<2949>]
| ^^^^^^^^^^ stack updated [removed <2949>] to [UNQ<2945>, UNQ<2946>, DBL<2947>, SRW<2948>]
| ^^^^^^^^^^ stack accessed using <2948>: [UNQ<2945>, UNQ<2946>, DBL<2947>, SRW<2948>]
10 | &*x;
| ^^^ stack accessed using <2946>: [UNQ<2945>, UNQ<2946>, DBL<2947>, SRW<2948>]
| ^^^ stack updated [added <2950>] to [UNQ<2945>, UNQ<2946>, DBL<2947>, SRW<2948>, SRO<2950>]
note: tracking was triggered
--> src/main.rs:5:17
|
5 | let x = &mut x;
| ^^^^^^ created allocation with id 1533
|
= note: inside `main` at src/main.rs:5:17
note: tracking was triggered
--> src/main.rs:5:17
|
5 | let x = &mut x;
| ^^^^^^ stack accessed using <2945>: [UNQ<2945>]
|
= note: inside `main` at src/main.rs:5:17
note: tracking was triggered
--> src/main.rs:5:17
|
5 | let x = &mut x;
| ^^^^^^ stack updated [added <2946>] to [UNQ<2945>, UNQ<2946>]
|
= note: inside `main` at src/main.rs:5:17
note: tracking was triggered
--> src/main.rs:6:19
|
6 | let ptr = &mut *x as *mut i32;
| ^^^^^^^ stack accessed using <2946>: [UNQ<2945>, UNQ<2946>]
|
= note: inside `main` at src/main.rs:6:19
note: tracking was triggered
--> src/main.rs:6:19
|
6 | let ptr = &mut *x as *mut i32;
| ^^^^^^^ stack updated [added <2947>] to [UNQ<2945>, UNQ<2946>, UNQ<2947>]
|
= note: inside `main` at src/main.rs:6:19
note: tracking was triggered
--> src/main.rs:6:19
|
6 | let ptr = &mut *x as *mut i32;
| ^^^^^^^ stack updated [added <2948>] to [UNQ<2945>, UNQ<2946>, UNQ<2947>, SRW<2948>]
|
= note: inside `main` at src/main.rs:6:19
note: tracking was triggered
--> src/main.rs:7:9
|
7 | *ptr += 20;
| ^^^^^^^^^^ stack accessed using <2948>: [UNQ<2945>, UNQ<2946>, UNQ<2947>, SRW<2948>]
|
= note: inside `main` at src/main.rs:7:9
note: tracking was triggered
--> src/main.rs:8:9
|
8 | &*x;
| ^^^ stack updated [changed <2947>] to [UNQ<2945>, UNQ<2946>, DBL<2947>, SRW<2948>]
|
= note: inside `main` at src/main.rs:8:9
note: tracking was triggered
--> src/main.rs:8:9
|
8 | &*x;
| ^^^ stack accessed using <2946>: [UNQ<2945>, UNQ<2946>, DBL<2947>, SRW<2948>]
|
= note: inside `main` at src/main.rs:8:9
note: tracking was triggered
--> src/main.rs:8:9
|
8 | &*x;
| ^^^ stack updated [added <2949>] to [UNQ<2945>, UNQ<2946>, DBL<2947>, SRW<2948>, SRO<2949>]
|
= note: inside `main` at src/main.rs:8:9
note: tracking was triggered
--> src/main.rs:9:9
|
9 | *ptr += 20;
| ^^^^^^^^^^ stack accessed using <2948>: [UNQ<2945>, UNQ<2946>, DBL<2947>, SRW<2948>, SRO<2949>]
|
= note: inside `main` at src/main.rs:9:9
note: tracking was triggered
--> src/main.rs:9:9
|
9 | *ptr += 20;
| ^^^^^^^^^^ stack updated [removed <2949>] to [UNQ<2945>, UNQ<2946>, DBL<2947>, SRW<2948>]
|
= note: inside `main` at src/main.rs:9:9
note: tracking was triggered
--> src/main.rs:9:9
|
9 | *ptr += 20;
| ^^^^^^^^^^ stack accessed using <2948>: [UNQ<2945>, UNQ<2946>, DBL<2947>, SRW<2948>]
|
= note: inside `main` at src/main.rs:9:9
note: tracking was triggered
--> src/main.rs:10:9
|
10 | &*x;
| ^^^ stack accessed using <2946>: [UNQ<2945>, UNQ<2946>, DBL<2947>, SRW<2948>]
|
= note: inside `main` at src/main.rs:10:9
note: tracking was triggered
--> src/main.rs:10:9
|
10 | &*x;
| ^^^ stack updated [added <2950>] to [UNQ<2945>, UNQ<2946>, DBL<2947>, SRW<2948>, SRO<2950>]
|
= note: inside `main` at src/main.rs:10:9
I also differentiated between two-phase borrows by adding a new permission tag that would print TPU, but I do not see it in the output (so either I did not add it correctly, or there are no two-phase borrows here).
So what it looks like IIUC is that access at UNQ<2946> is disabling Uniq tags above it on the stack but not impacting SRW tags. This definitely feels like a bug in Miri; cc @RalfJung if/when you have time to look at this.
I did another test to see if two-phase borrows would be correctly identified by my custom diagnostic and it seems to work:
let mut vec = vec![];
vec.push(vec.len());
just a small sample from the log:
3 | let mut vec = vec![];
| ^^^^^^ stack accessed using <2946>: [UNQ<2946>]
| ^^^^^^ stack updated [added <2947>] to [UNQ<2946>, UNQ<2947>[proc(929)]]
4 | vec.push(vec.len());
| ^^^^^^^^^^^^^^^^^^^ stack accessed using <2946>: [UNQ<2946>]
| ^^^^^^^^^^^^^^^^^^^ stack updated [added <2950>] to [UNQ<2946>, TPU<2950>]
| ^^^^^^^^^ stack accessed using <2946>: [UNQ<2946>, TPU<2950>]
| ^^^^^^^^^ stack updated [added <2951>] to [UNQ<2946>, TPU<2950>, SRO<2951>]
There exists a section in the paper about a bad pointer pattern (page 21). IIRC it only applies to reads of the location though:
fn bad_pattern (x: & mut i32 ) {
retag [ fn ] x; // Assume x = Pointer(ℓ, t x ).
let raw_ptr = make_raw (x ); // Desugars to ` make_raw (& mut *x ) `.
// h(ℓ) = [. . . , Unique(t x ), Unique(t tmp ), Unique(ty ), SharedRW(⊥)]
let val1 = *x;
// h(ℓ) = [. . . , Unique(t x )]
let val2 = unsafe { * raw_ptr }; // Fails because SharedRW(⊥) is no longer in the stack!
}
Writes using raw_ptr with interleaved reads of x still feel very wrong (and should probably not be permitted, but I do not know if there is some other reason this is allowed).
Created a miri version that replaces all SRW with SRO upon reading from a pointer below in the stack: GitHub - y86-dev/miri at deny_writes_after_unique_read (it also contains the custom diagnostic, you can ignore that/rebase from miri/master if you do not want to have it)
This is not very sophisticated yet, I have only quickly looked at the failed tests (15) and it seems it breaks slice::iter -.-. It also should break interleaved R/W using SRWs, but I have not investigated that yet (but only 15 failed tests might hint that it does not break that).
In the iter case, it seems like a very small fix, could make it work, but again I have only glanced at the problem for a few minutes.
Thanks for sharing this writeup! Sorry I could not reply earlier; I have been super busy unfortunately and reading these proposals always takes a good chunk of time. It is great to see more people explore the space of memory models. 
I also hope to do some work on "Tree Borrows" soon, but my ideas are quite different at least in some aspects -- in particular, I am going to explore a single global tree, rather than a per-location tree. So there could be some interesting possible comparisons later. 
To me, the key motivations for a tree are
Those are not on your list, so I take it you are tackling different problems? I am curious how in particular the UnsafeCell trouble is even related to trees; I see the problems around UnsafeCell as being largely orthogonal to using a tree vs using a stack.
SharedImmutRead
If I understand your table correctly, this tag does not allow aliasing, i.e., it is unique? Then why is it called "shared"?
So, your SHIR is exactly like SharedReadOnly in Stacked Borrows, and your SharedReadOnly is different from the thing with the same name in Stacked Borrows? That sounds quite confusing 
3.1.1 Allow reading from *mut T after writes using the parent &mut T
To me, this is a key property of Stacked Borrows: after writing to a &mut (that we privately created the tag for), we should be sure that no pointers "derived from" our pointer exists that has read or write access to this memory. That is what uniqueness means, I think. If we allow then, then what are we even achieving with all our rules? So if you want to allow this, then my question for you would be to more clearly state the goals of the model -- are there certain optimizations you want to have, or certain reasoning principles you want to establish?
The best outline is this blog post. But the summary is: for the purpose of this discussion, we can pretend that int2ptr casts never happen. The proposed approach makes them entirely orthogonal to whatever the aliasing model does.
Thanks for your reply! In the meantime I have realized some of the problems that have come up with the document I wrote. I have not written something new about it (but I have some unfinished changes...), as I have been busy in other areas, but would love to help find some better solution in this area!
At the time of writing I did not know of those problems. My main motivation was the better interior mutability tracking to allow more optimizations of !Unpin types related to the Unsafe{Alias, Mut}Cell discussion. The discussion is a bit long, but the gist is that we could use a type that lifts the restriction that &mut UnsafeAliasCell<T> needs to be unique.
I thought that these are related to the model, because the model models &mut and &, &UnsafeCell<T> and &mut UAC lift some of the restrictions and as such cannot be represented by the model in the same way as &mut/&. Now I am not so sure anymore, because &UnsafeCell<T> and &mut UAC are essentially *mut T, but there might be some benefit in tagging them differently...
No this is not unique.
No it is not exactly, as SHIR also has the invariant, that the pointee is never written to, SRO allows (in both models) the modification of the pointee by other pointers.
This is going to be removed in the next iteration.
Thanks, I have read that blog post since.
What I plan to do in the next weeks, is to write the next iteration and find some more implementation details. In particular, I think that the always-two-phase-borrow approach looks promising and I will try to incorporate that.
I see. However, what I don't get is what that has to do with trees. This is entirely analogous to UnsafeCell on shared references: if we have UnsafeAlias, then when we reborrow for &mut we want to use Unique permission on the bytes outside UnsafeAlias, and SharedReadWrite permission on the bytes inside UnsafeAlias.
Stacked Borrows UnsafeCell handling has its problems, but I don't know how any of them can be solved by using trees.
SharedReadOnly allows modification? I am confused.^^ In Stacked Borrows, it does not allow modification.
Yes that is what I found out as well, so on the initial glances a tree does not seem to improve thiis area.
I do not know either, so I will see if I find anything.
In my model it allows it via other pointers. So you can have
let mut a = 0;
let shared_read_only = &raw const a;
let shared_read_write = &raw mut a;
println!("{}", *shared_read_only);
*a = 3;
println!("{}", *shared_read_only);
Miri does not allow for this, so I was under the wrong impression that SB allowed this. Sorry for the confusion!
Disallowing that code is pretty much the defining property of SharedReadOnly. It is absolutely crucial that when reading twice from a shared reference (without UnsafeCell), there was no mutation in between.
I guess you are then using SharedImmutRead for shared references, which still works like SharedReadOnly in SB? Let me then call your new permission SharedConst, because it works like C const pointers. I do not understand the motivation for distinguishing SharedConst from SharedReadWrite. IMO &raw const a should either be a read-only pointer like in Stacked Borrows, or it should be full SRW -- I don't see a good motivation for making it "constant but other pointers can mutate this memory". That is an extra complexity that I deliberately avoided.