Make stacked borrow failures easier to debug

[oli-obk]

After a single run of miri fails with a stacked borrow failure, it is pretty hard to debug what's going on. All you get is an id of a borrow and a backtrace pretty late in the process. Since we can be deterministic, maybe we could add a -Ztrace-borrows flag that you can give a list of ids and it will print backtraces or other things whenever an id from the list is affected.

[RalfJung]

Yeah, debugging is quite awful for this. Ideally we'd capture (partial) stacktraces to tell you where the ID became invalid, or so.

[RalfJung]

For those reading along: the Stacked Borrows debugging situation got a lot better with #1080. There's still a lot to be desired, though.

[jrvanwhy]

Note: I'm still trying to comprehend stacked borrows, so my suggestion may not make sense.

One tool that I would find useful is a way to print out the borrow stack for a place. Something like:

#[cfg(miri)]
extern "Rust" {
    fn miri_print_borrow_stack(place: *const u8);
}

miri_print_borrow_stack would print out the information in the Stack type described here.

[RalfJung]

@jrvanwhy I like the basic idea.

However, what do you think the output will look like? It mostly consists of many numbers that are entirely meaningless on their own: stack elements look like [SharedReadOnly for <17539>]. These numbers only make sense when you know which pointers (in which Rust variables) have which tag, and I am not sure how Miri would convey that information.

[bjorn3]

I think it would be useful if priroda could visualize the stacked borrows state. That would make it possible to take a deeper look at the state than a static error message.

[jrvanwhy]

@jrvanwhy I like the basic idea.

However, what do you think the output will look like? It mostly consists of many numbers that are entirely meaningless on their own: stack elements look like [SharedReadOnly for <17539>]. These numbers only make sense when you know which pointers (in which Rust variables) have which tag, and I am not sure how Miri would convey that information.

That looks right to me. Seeing the permissions printed alone will help me identify when I missed a stack entry (e.g. when a I fail to identify that a retag has happened). If execution is deterministic, I could use -Zmiri-track-pointer-tag and -Zmiri-track-call-id to identify the unexpected entries.

It's possible that my suggestion is a better learning tool for those of us trying to understand stacked borrows than it is a debugging tool for those who already understand stacked borrows.

I think it would be useful if priroda could visualize the stacked borrows state. That would make it possible to take a deeper look at the state than a static error message.

Thanks for mentioning priroda, I have not heard of it before!

[RalfJung]

I think it would be useful if priroda could visualize the stacked borrows state. That would make it possible to take a deeper look at the state than a static error message.

Yes, that would be really nice.

That looks right to me. Seeing the permissions printed alone will help me identify when I missed a stack entry (e.g. when a I fail to identify that a retag has happened). I

I must be missing something, since the entries look completely meaningless to me. Could you give a concrete example?

[jrvanwhy]

That looks right to me. Seeing the permissions printed alone will help me identify when I missed a stack entry (e.g. when a I fail to identify that a retag has happened). I

I must be missing something, since the entries look completely meaningless to me. Could you give a concrete example?

I took your example from https://www.ralfj.de/blog/2019/05/21/stacked-borrows-2.1.html and tweaked it:

fn main() { unsafe {
    extern "Rust" {
        fn miri_print_borrow_stack(*const u8);
    }

    let c = &UnsafeCell::new(UnsafeCell::new(0));
    let inner_uniq = &mut *c.get();
    // Prints [{tag: 2723, perm: SharedReadWrite},
    //         {tag: 2731, perm: Unique}]:
    miri_print_borrow_stack(inner_uniq as *const _ as *const u8);

    let inner_shr = &*inner_uniq; // adds a SharedReadWrite
    // Prints [{tag: 2823, perm: SharedReadWrite},
    //         {tag: 2731, perm: Unique},
    //         {tag: 2732, perm: SharedReadWrite}]:
    miri_print_borrow_stack(inner_shr as *const _ as *const u8);

    *c.get() = UnsafeCell::new(1); // invalidates inner_shr
    // Prints [{tag: 2823, perm: SharedReadWrite}]:
    miri_print_borrow_stack(inner_shr as *const _ as *const u8);

    let _ = inner_shr;
} }

If this doesn't make sense, then I probably need to learn more before I can make useful suggestions.

[RalfJung]

No that makes sense, but how useful is this given that these tag numbers don't mean anything, i.e., are not related to any particular local variables? (The stacks will often have dozens of entries in real programs.)

[jrvanwhy]

No that makes sense, but how useful is this given that these tag numbers don't mean anything, i.e., are not related to any particular local variables? (The stacks will often have dozens of entries in real programs.)

Maybe it's much less useful than I think (my understanding of Miri + Stacked Borrows is still very basic).

[saethlin]

I think this is closed by #2030.

Also, locally I slapped in a little hack where you can enable and disable a flag that makes Miri print the stacks that are modified after every retag that touches them. Even as a somewhat expert user I found the output almost completely useless, on account of the signal-to-noise ratio. Here's just two lines of a tiny program, I tried calling Vec::push but it basically filled my screen.

note: currently here
  --> src/main.rs:12:9
   |
12 |         x.len();
   |         ^^^^^^^

[i32; 3]: 
    0..12: [[Unique for <2392>], [Unique for <2393>], [SharedReadOnly for <2394>]]
[i32]: 
    0..12: [[Unique for <2392>], [Unique for <2393>], [SharedReadOnly for <2394>], [SharedReadOnly for <2395>]]
usize: 
    0..8: [[Unique for <2396>], [Unique for <2397> (call 770)]]
[i32]: 
    0..12: [[Unique for <2392>], [Unique for <2393>], [SharedReadOnly for <2394>], [SharedReadOnly for <2395>], [SharedReadOnly for <2398> (call 770)]]
[i32]: 
    0..12: [[Unique for <2392>], [Unique for <2393>], [SharedReadOnly for <2394>], [SharedReadOnly for <2395>], [SharedReadOnly for <2398> (call 770)], [SharedReadOnly for <untagged>]]
note: currently here
  --> src/main.rs:13:9
   |
13 |         &mut x[0];
   |         ^^^^^^^^^

i32: 
    0..4: [[Unique for <2392>], [Unique for <2393>], [Unique for <2400>]]
    4..12: [[Unique for <2392>], [Unique for <2393>], [SharedReadOnly for <2394>], [SharedReadOnly for <2395>], [SharedReadOnly for <2398> (call 770)], [SharedReadOnly for <untagged>]]

[RalfJung]

All right, let's close this and open more specific issue in case there are concrete things we think we can still improve.

Thanks a lot @saethlin for working on this!