Tree Borrows: improved diagnostics #2828

Vanille-N · 2023-03-29T22:34:42Z

Better diagnostics for Tree Borrows violations.

Shows where the conflicting tags (the one that was accessed and the one that had a permission or protector that caused UB) were reborrowed, which is more readable than only <TAG>
Shows a small history of what happened for the faulty tag to get there (which lines caused it to lose read/write permissions)
Explains permissions and transitions in natural language (e.g. "does not have read permissions" instead of "is Disabled")

Not perfect, but at least testing TB will be less confusing.

Lack of range information from RangeMap makes selection of relevant events nontrivial: we reconstruct history from knowledge of (initial, final) and (offset, pi, p'i) so that initial -> final = p1 -> p1' = p2 -> p2' = p3 -> ... = final

saethlin · 2023-03-29T23:01:26Z

src/diagnostics.rs

-            TreeBorrowsUb { .. } => {
-                let helps = vec![
+            TreeBorrowsUb { trigger_history, faulty_history, .. } => {
+                let url = "https://perso.crans.org/vanille/treebor";


I agree that we should link people to something helpful, and also that your write-up is helpful, but I'm not excited about linking someone to a site that's not managed by the Rust project.

Very understandable. I'll remove that.

FWIW the readme still links there.

We could do what we did with SB, and have a page in https://github.com/rust-lang/unsafe-code-guidelines/tree/master/wip and link there. For now that page would basically just link to Neven's blog, but in the future it could contain its own concise description of the rules (like we do for SB).

saethlin · 2023-03-29T23:27:48Z

tests/fail/tree-borrows/error-range.stderr

@@ -0,0 +1,39 @@
+error: Undefined Behavior: read access through <TAG> is forbidden because it is a child of <TAG> which is Disabled.


"which is disabled" clashes with the rest of the terminology in this diagnostic now. Where was it disabled? Nothing in this diagnostic mentions a disable. (this is rhetorical)

Not to open up the terminology question again, but I feel like in light of the other details given below it makes more sense to say "because it is a child of {tag} which lost all permissions". It seems like we have two sets of terminology here, and the one used in the helps requires a few more words but is more obvious to a reader.

I'll update the diagnostic for protector violations too, it currently says "change from Active to Frozen"

I agree we should use the same set of terminology everywhere, but I think it should be the state names. Reserved, Active, Frozen, Disabled seems much clearer to me than having to talk about "future write permissions".

RalfJung · 2023-04-01T06:06:02Z

This required getting some more information from RangeMap: from just the offset to the actual range.

Please undo that, the range is meaningless. Instead do what we did for SB: the offset is the first byte where a conflict happens; no statement is made about later bytes. Conceptually this code iterates over bytes and checks each byte separately; the fact that RangeMap optimizes this is an implementation detail that should not be observable.

Vanille-N · 2023-04-01T10:30:27Z

Yeah I had specifically tried to avoid SB's way of doing this, which is to reconstruct the previous range from the current offset, which led me to think I needed the range from RangeMap.
It is in fact not necessary, but I'll let you decide if you find the added complexity of extract_relevant worth it.

src/borrow_tracker/tree_borrows/diagnostics.rs

RalfJung · 2023-04-13T08:28:36Z

tests/fail/tree-borrows/error-range.stderr

@@ -0,0 +1,39 @@
+error: Undefined Behavior: read access through <TAG> is forbidden because it is a child of <TAG> which is Disabled.


I agree we should use the same set of terminology everywhere, but I think it should be the state names. Reserved, Active, Frozen, Disabled seems much clearer to me than having to talk about "future write permissions".

RalfJung · 2023-04-13T08:36:07Z

tests/fail/tree-borrows/write-during-2phase.stderr

+LL | |         n
+LL | |     });
+   | |______^
+help: <TAG> lost read and write permissions due to a write access at offsets [0x0..0x8]


This should tell a story, e.g.

TAG was created here in Reserved state by a reborrow (name parent tag, maybe?)

TAG later changed to Disabled state due to a Foreign write access at offsets...

I guess @saethlin will want us to avoid using special Tree Borrows terminology here, but I really don't see a good way to avoid that. Replacing state names by long permission descriptions doesn't really explain that much IMO, and this here currently describes Reserved as "with read and write permissions" which is confusing since that sounds like Active.

Maybe we have the help line be a short one using special terms, and then have a more detailed note/help below (or somewhere) that explains a bit more, and that people familiar with TB can skip?

Replacing state names by long permission descriptions doesn't really explain that much IMO

🤷 I think it helps. It also gets us out of discussing disabled children.

Really we have a Stroustrup's Rule problem here: Everyone finds the new terminology confusing at first, but then later they want a terse notation for it. I've noticed that the pickup rate for changes in Miri can be amazingly slow, some rather experienced unsafe code users didn't notice the new span-based diagnostics until 6 months after they released.

So however you want to navigate all that is good with me. If we're going to put up all the Tree Borrows terminology, there needs to be an accessible way for people to learn what those terms mean. https://perso.crans.org/vanille/treebor/ is a great breakdown of the whole model, but it is quite intimidating for a newcomer who is just trying to figure out why Miri doesn't like their new data structure idea.

I've long wanted a sort of glossary built from common patterns that explains why they are invalid and how to fix them. https://miri.saethlin.dev/tree-borrows/ub exists now and will be complete once the upload finishes. I will work on such a glossary eventually if someone else doesn't beat me to it.

Stroustrup's Rule

Definitely. But we also have the problem that there's a lot going on and trying to cram that all into a single sentence will not result in anything readable.

If you have good suggestions for how to avoid the state names, I am all ears. But the PR as-is describes Reserved as "having read and write permissions" and that's just misleading -- and the more correct "having read and future-write permissions" is no better than just saying "Reserved". (In fact it is worse; having a concise name for a concept is very useful for documentation and teaching.)

It also gets us out of discussing disabled children.

It'll look more like "child of , which is Disabled", I think. We could also consider renaming Disabled to Inactive, Invalid, Deactivated, something like that.

If you have good suggestions for how to avoid the state names, I am all ears.

I don't. I wish I did.

I was a bit surprised by the direction @Vanille-N took my comment, but as I dislike terse notation (because with my route through grad school I was constantly reading papers outside my subfield) I am not inclined to get in anyone's way when they are removing it. My initial comment was focused on the consistency or logical flow of terminology/phrasing because that's a clearer topic. If it turns out that addressing my comment that requires opening up a lot more lines of discussion let's do the incremental thing and add all the extra notes now and decide on the English that surrounds them later.

We could also consider renaming Disabled to Inactive, Invalid, Deactivated, something like that.

Please not another use of Invalid :p

I don't particularly care what color the shed is, but I want us to be happy with the term before Tree Borrows becomes a default.

Vanille-N · 2023-04-14T07:22:30Z

Speaking of "cram that all into a single sentence", I hope this is more readable ?
I used help: by default because it's not obvious how to have that part of the code use another marker.

bors · 2023-04-14T19:16:38Z

☔ The latest upstream changes (presumably #2843) made this pull request unmergeable. Please resolve the merge conflicts.

tests/fail/tree-borrows/error-range.stderr

RalfJung

Very nice, just some nits for the messages!

And one more concern: could you benchmark this against tree-borrows without the history tracking? In SB we had to work a bit to avoid regressing perf too much.

src/borrow_tracker/tree_borrows/diagnostics.rs

tests/fail/tree-borrows/read-to-local.stderr

RalfJung · 2023-04-20T07:28:01Z

tests/fail/tree-borrows/outside-range.stderr

   |
+   = help: the accessed tag <TAG> is a foreign tag for the conflicting tag <TAG>.
+   = help: the conflicting tag <TAG> is protected, and the access would cause it to transition from Reserved to Disabled, which is a loss of read and write permissions.


This is hard to follow. If the conflicting tag is protected, does its relation with the accessed tag even matter? Or could we say something more like "this access conflicts with protected tag "..."the access would cause the protected tag to transition..."..."the protected tag was created here"...? Somewhere it should also say something like "protected tags must not lose permissions" or so; it already says that for deallocation but not for these errors here.

src/borrow_tracker/tree_borrows/perms.rs

src/borrow_tracker/tree_borrows/diagnostics.rs

src/diagnostics.rs

Vanille-N · 2023-04-20T12:52:19Z

And one more concern: could you benchmark this against tree-borrows without the history tracking? In SB we had to work a bit to avoid regressing perf too much.

Tested just now. The easy comparison is between recording or ignoring the events: the only diagnostics-related operation that is done more than once per allocation is pushing an Event to the history. (The other operations are allocating a history (once per allocation), and filtering the history (once per execution))

With this measure, the two versions of the code with and without diagnostics have their mean ± σ that intersect on every single ./miri benchmark, so the cost of recording every event on every range is no more than 2%. I'll try a more in-depth comparison by also removing the computation of Span and stuff.

RalfJung · 2023-04-20T13:32:50Z

Are there any situations where we can avoid storing an event, or discard events that we won't need any more?

Vanille-N · 2023-04-20T13:43:09Z

Discard, yes. Events are garbage collected with the tag they are relevant to.

Avoid storing, no. An event is not an access, Event = (access, range, transition) where !transition.is_noop(), so there are by design at most 4 events (1 creation + ≤3 transitions) per tag per location.

All events can possibly be relevant to reconstruct the history of a tag, unless we're fine with having holes in the history, such as if we don't care where a tag went from Active to Frozen if the error is triggered because it is now Disabled.
I like having the current complete history of the permission, but it is true that we don't need all of it.

RalfJung · 2023-04-20T14:03:24Z

Well I guess let's just go with this for now and maybe if @saethlin optimizes TB and this becomes an actual bottleneck we decide to only keep some of that history around. ;)

RalfJung · 2023-04-20T14:28:36Z

tests/fail/tree-borrows/reserved/cell-protected-write.stderr

@@ -15,7 +15,7 @@ LL |             *y = 1;
   |             ^^^^^^ write access through <TAG> (y, callee:y, caller:y) is forbidden.
   |
   = help: the accessed tag <TAG> (y, callee:y, caller:y) is a foreign tag for the protected tag <TAG> (callee:x).


Why is the "foreign" part relevant here?

The "foreign" part is guaranteed, since protector violations outside of deallocations only ever occur on foreign accesses. If you think it distracts from the rest of the diagnostic it's easy to remove.

Yeah I think it is a distraction, to understand the error it is not relevant that the pointer is foreign.

Hm okay that also reads awkwardly... I have tweaked the wording a bit more, time to land this. :)

saethlin · 2023-04-20T15:39:12Z

FWIW in Stacked Borrows I was rather shocked by how cheap the history is compared to the actual stacks. I think the reason this is the case is that these events are not split up per byte like aliasing properties are. In real programs I think a lot of the reborrows are many bytes in size and the history events are not split no matter what aliasing activity is below them.

RalfJung · 2023-04-28T11:23:30Z

@bors r+

bors · 2023-04-28T11:23:32Z

📌 Commit 47059d4 has been approved by RalfJung

It is now in the queue for this repository.

bors · 2023-04-28T11:23:38Z

⌛ Testing commit 47059d4 with merge 81eda2a...

bors · 2023-04-28T11:57:21Z

☀️ Test successful - checks-actions
Approved by: RalfJung
Pushing 81eda2a to master...

saethlin reviewed Mar 29, 2023

View reviewed changes

Vanille-N force-pushed the tb-diags branch from 44ca1e8 to 12ff8a5 Compare March 29, 2023 23:10

saethlin reviewed Mar 29, 2023

View reviewed changes

Vanille-N force-pushed the tb-diags branch from c442dad to 80444f0 Compare April 1, 2023 10:07

RalfJung reviewed Apr 13, 2023

View reviewed changes

Vanille-N force-pushed the tb-diags branch from ae5f48d to caccab0 Compare April 14, 2023 19:28

RalfJung reviewed Apr 20, 2023

View reviewed changes

tests/fail/tree-borrows/error-range.stderr Show resolved Hide resolved

RalfJung reviewed Apr 20, 2023

View reviewed changes

src/diagnostics.rs Outdated Show resolved Hide resolved

RalfJung reviewed Apr 20, 2023

View reviewed changes

Vanille-N and others added 2 commits April 28, 2023 13:02

Tree Borrows: improved diagnostics

e415edb

tweak wording

47059d4

RalfJung force-pushed the tb-diags branch from 70e8802 to 47059d4 Compare April 28, 2023 11:22

bors merged commit 81eda2a into rust-lang:master Apr 28, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Tree Borrows: improved diagnostics #2828

Tree Borrows: improved diagnostics #2828

Vanille-N commented Mar 29, 2023 •

edited

Loading

saethlin Mar 29, 2023

Vanille-N Mar 29, 2023

RalfJung Apr 1, 2023

saethlin Mar 29, 2023 •

edited

Loading

Vanille-N Mar 29, 2023

RalfJung Apr 13, 2023

RalfJung commented Apr 1, 2023

Vanille-N commented Apr 1, 2023

RalfJung Apr 13, 2023

RalfJung Apr 13, 2023

saethlin Apr 13, 2023

RalfJung Apr 13, 2023 •

edited

Loading

RalfJung Apr 13, 2023

saethlin Apr 13, 2023

Vanille-N commented Apr 14, 2023

bors commented Apr 14, 2023

RalfJung left a comment

RalfJung Apr 20, 2023

Vanille-N commented Apr 20, 2023 •

edited

Loading

RalfJung commented Apr 20, 2023

Vanille-N commented Apr 20, 2023

RalfJung commented Apr 20, 2023

RalfJung Apr 20, 2023

Vanille-N Apr 26, 2023

RalfJung Apr 26, 2023

RalfJung Apr 28, 2023

saethlin commented Apr 20, 2023 •

edited

Loading

RalfJung commented Apr 28, 2023

bors commented Apr 28, 2023

bors commented Apr 28, 2023

bors commented Apr 28, 2023

		@@ -0,0 +1,39 @@
		error: Undefined Behavior: read access through <TAG> is forbidden because it is a child of <TAG> which is Disabled.

Tree Borrows: improved diagnostics #2828

Tree Borrows: improved diagnostics #2828

Conversation

Vanille-N commented Mar 29, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

saethlin Mar 29, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RalfJung commented Apr 1, 2023

Vanille-N commented Apr 1, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RalfJung Apr 13, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Vanille-N commented Apr 14, 2023

bors commented Apr 14, 2023

RalfJung left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Vanille-N commented Apr 20, 2023 • edited Loading

RalfJung commented Apr 20, 2023

Vanille-N commented Apr 20, 2023

RalfJung commented Apr 20, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

saethlin commented Apr 20, 2023 • edited Loading

RalfJung commented Apr 28, 2023

bors commented Apr 28, 2023

bors commented Apr 28, 2023

bors commented Apr 28, 2023

Vanille-N commented Mar 29, 2023 •

edited

Loading

saethlin Mar 29, 2023 •

edited

Loading

RalfJung Apr 13, 2023 •

edited

Loading

Vanille-N commented Apr 20, 2023 •

edited

Loading

saethlin commented Apr 20, 2023 •

edited

Loading