Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

TB: Missed UB in the "optimization" that allows skipping subtrees #3846

Closed
JoJoDeveloping opened this issue Aug 26, 2024 · 3 comments · Fixed by #3847
Closed

TB: Missed UB in the "optimization" that allows skipping subtrees #3846

JoJoDeveloping opened this issue Aug 26, 2024 · 3 comments · Fixed by #3847
Labels
A-aliasing Area: This affects the aliasing model (Stacked/Tree Borrows) C-bug Category: This is a bug. I-misses-UB Impact: makes Miri miss UB, i.e., a false negative (with default settings)

Comments

@JoJoDeveloping
Copy link
Contributor

JoJoDeveloping commented Aug 26, 2024

Tree Borrows has an optimization where we skip subtree updates if we know that the subtree has not changed -- at least that was the idea. More specifically, every node records if its last access was a child access, a foreign read, or a foreign read/write (mixed, since a write followed by a read is idempotent). Then, if e.g. the last access was a foreign read, and the next access is also a foreign read, we should be able to skip the entire subtree, since it should already be idempotent.

But turns out, we can not always skip the tree. The reason is that lazy nodes exist, which are "silently" created across the entire allocation whenever you do a reborrow, while the reborrow only emits an event for the actually accessed range. Combined with protected Reserved being supposed to become conflicted on a foreign read (even when lazy), this leads to missed UB. The optimization for foreign writes can also be broken by a ReservedIM node, which would shield its children from foreign write accesses, which is even worse.

Here is an example:

use std::ptr::addr_of_mut;

fn do_something(_: u8) {}

unsafe fn access_after_sub_1(x: &mut u8, orig_ptr: *mut u8) {
    // causes a second access, which should make the lazy part of `x` be `Reserved {conflicted: true}`
    do_something(*orig_ptr);
    // read from the conflicted pointer
    *(x as *mut u8).byte_sub(1) = 42;
}

pub fn main() {
    unsafe {
        let mut alloc = [0u8, 0u8];
        let orig_ptr = addr_of_mut!(alloc) as *mut u8;
        let foo = &mut *orig_ptr;
        // cause a foreign read access to foo
        do_something(alloc[0]);
        access_after_sub_1(&mut *(foo as *mut u8).byte_add(1), orig_ptr);
    }
}

Because the foo reference is internally marked as "already experienced a foreign read," the second foreign read in do_something skips the entire subtree, and thus does not mark that the lazy part of x as conflicted. Thus, the later read is possible, whereas it should not be.

CC @Vanille-N

I was not able to turn this into a LLVM misoptimization, but the generated LLVM code has UB, I believe (accesses a noalias ptr and another pointer pointing to the same memory location). In general, turning this into a miscompilation is hard since LLVM does not seem to be willing to reorder reads and writes that are the first access.

@JoJoDeveloping
Copy link
Contributor Author

JoJoDeveloping commented Aug 26, 2024

The question of how to resolve this is interesting. One option is to remove this optimization, but it surely exists for a reason. Another option is to weaken it, by making retags reset this "already experienced a foreign read" marker on all their parents across the entire range. But this introduces extra overhead, and it should be tested what the performance impact is here.

Luckily, not all is lost. Instead on optimizing traversals based on "what was the last access", one can instead optimize based on permissions -- it is sound to skip foreign reads when a node is Frozen, as this can never miss any UB; similarly, for Disabled, write accesses can be skipped. See here for an experimental implementation. While this was pretty useless in the past, if we weaken the "last access" optimization, then it can become very relevant. This does not fully subsume the "last access" optimization, which was also able to handle subtrees consisting only of Reserved, which such an approach is not.

Someone can have lots of fun profiling this. 🙃

@RalfJung
Copy link
Member

Wow, good catch!

Did we not have exhaustive tests checking this optimization, or were they not exhaustive enough?

The immediate next step should be to disable that optimization, and then we can take time to figure out another, actually sound optimization.

@JoJoDeveloping
Copy link
Contributor Author

JoJoDeveloping commented Aug 26, 2024

Did we not have exhaustive tests checking this optimization, or were they not exhaustive enough?

There was an exhaustive test checking that foreign reads after foreign writes are no-ops, and another one that two foreign accesses repeated are no-ops. These were not the issue here.

The problem was that this option was simply missed. The comment on that function prominently states:

    // Helper to optimize the tree traversal.
    // The optimization here consists of observing thanks to the tests
    // `foreign_read_is_noop_after_foreign_write` and `all_transitions_idempotent`,
    // that there are actually just three possible sequences of events that can occur
    // in between two child accesses that produce different results.
    //
    // Indeed,
    // - applying any number of foreign read accesses is the same as applying
    //   exactly one foreign read,
    // - applying any number of foreign read or write accesses is the same
    //   as applying exactly one foreign write.
    // therefore the three sequences of events that can produce different
    // outcomes are
    // - an empty sequence (`self.latest_foreign_access = None`)
    // - a nonempty read-only sequence (`self.latest_foreign_access = Some(Read)`)
    // - a nonempty sequence with at least one write (`self.latest_foreign_access = Some(Write)`)

But there's the secret fourth option: silently add a new node with lazy permission, but without ever causing an access at the position where the node is lazy (outside of the initial range). But that's of course not an action that changes any node, so it was overlooked in the exhaustive tests (or rather: what would the exhaustive test do there?). The problem with them was that they only checked things for one node, but of course the problem here is we add a second node.

The implicitly assumed tree invariant was that "if the foreign last access to a node was X, then the last access to its children was also at least as strong as X; and every child is invariant under that access", but lazy nodes break that. This is an "entire tree" invariant and not easily exhaustively testable.

Looking back, these lazy permissions that are added silently are a pretty large footgun. #3732 was similarly due to them being overlooked.

JoJoDeveloping added a commit to JoJoDeveloping/miri that referenced this issue Aug 26, 2024
JoJoDeveloping added a commit to JoJoDeveloping/miri that referenced this issue Aug 26, 2024
@RalfJung RalfJung added C-bug Category: This is a bug. A-aliasing Area: This affects the aliasing model (Stacked/Tree Borrows) I-misses-UB Impact: makes Miri miss UB, i.e., a false negative (with default settings) labels Aug 27, 2024
JoJoDeveloping added a commit to JoJoDeveloping/miri that referenced this issue Aug 27, 2024
@bors bors closed this as completed in 6d114cb Aug 27, 2024
JoJoDeveloping added a commit to JoJoDeveloping/miri that referenced this issue Nov 1, 2024
This commit supplies a real fix, which makes retags more complicated, at the benefit of
making accesses more performant.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-aliasing Area: This affects the aliasing model (Stacked/Tree Borrows) C-bug Category: This is a bug. I-misses-UB Impact: makes Miri miss UB, i.e., a false negative (with default settings)
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants
@RalfJung @JoJoDeveloping and others