Is miri's mutable aliasing guard too conservative?

help
1

Hello. This question is the return of this other one, but unfortunately the brilliant work-around suggested by Quinedot can't be applied to this new case.

I have some code that exhibits the following pattern, and fails under miri.

use core::cell::UnsafeCell;

struct Database {
    state: UnsafeCell<Box<usize>>
}

struct Permission<'a> (&'a mut usize);

impl Permission<'_> {
    fn increment(&mut self) {
        *self.0 += 1;
    }
}

impl Database {
    fn new() -> Self {
        Self{ state: UnsafeCell::new(Box::new(0))}
    }
    fn get_permission(&self) -> Option<Permission<'_>> {
        //I know there needs to be other checks here so that multiple permissions aren't granted
        // to the same state.  That is elided because it's not relevant to this demonstration
        Some(Permission(unsafe{ &mut *self.state.get() }))
    }
    fn cleanup_permission(&self, perm: Permission<'_>) {
        drop(perm);

        let state = unsafe{ &mut *self.state.get() };
        **state += 1;
    }
}

fn main() {
    let db = Database::new();
    let mut perm = db.get_permission().unwrap();
    perm.increment();
    db.cleanup_permission(perm);
}

If I separate the cleanup_permission method into two, there is no problem. However, the point of the cleanup code is that it must run immediately after the permission object is destroyed*. So separating the API, ironically, makes it unsound.

My questions are:

  1. is my code actually UB? i.e. could the compiler reorder the drop somehow? Or is miri just being too conservative?
  2. Is there a work-around, given the new constraints?

Thanks for any thoughts or ideas.

*Dropping and even forgetting a permission without calling cleanup is not UB, so the outward API should be sound even without cleanup. The cleanup method is needed for full functionality, however.

2

Miri gets happier when I change Permission's variance from &mut to a constant variance. E.g.

struct Permission<'a> (*mut usize, PhantomData<&'a usize>)

But I'm not sure this is actually safe to do. I.e. the permission is, for all intents and purposes, a mutable reference to part of the database, while it's alive.

3

It's something like, the &mut _ is valid for the entirety of the method, and the compiler is allowed to exploit this, by e.g. assuming the memory under the &mut isn't aliased for the duration of the call. I don't think Rust is going to budge on that[1] unless it gains some special annotation or such to opt into it. AFAIU MaybeDangling will be such mechanism (but it's not implemented much less stable).

Thought experiment: let's say it was allowed without unsafe. Then you could safely write

fn mental_excercise(&self, perm: Permission<#[becomes_local] '_>) {
   drop(perm);
   let other_perm_obtained_before_cleanup = self.get_permission();
   cleanup_code_that_runs_too_late(self);
}

(I'm uncertain how relevant the mental exercise is given the code minimization. Maybe you're doing privacy restricted or unsafe stuff in there. I wrote that up as I was struggling to imagine the full picture.)

Have you accounted for the fact that it's safe to never call cleanup_permission? It seems you have, okay.

Is your real requirement that Database remains borrowed until the end of the cleanup code runs, once the beginning runs? If that's sufficient, you could do this.

Is it not possible to perform operations involving the UnsafeCell via the Permission<'_> (or a deconstruction of the Permission<'_>) in cleanup_permission?

Miri doesn't complain if you use *mut instead. Okay, you figured that out too.[2] *mut has less invariants than &mut.

  1. internal reasons aside, it needs LLVM to support something less stringent but not optimization-killing too ↩︎

  2. There is no change in variance here though... in the minimization anyway ↩︎

1 Like
4

Is your real requirement that Database remains borrowed until the end of the cleanup code runs, once the beginning runs? If that's sufficient, you could do this.

It's not exactly about the borrow of Database, it's about the fact that the Permission object represents the rights to run the cleanup code safely. It's proven that the cleanup code can run inside that function precisely because that's the only place the permission object is accounted for. Any other place, before or after that function, means there might be another permission to interfere.

When I saw your solution using the CleanupHelper's Drop impl, I was momentarily very happy. (It is ingenious, BTW) Unfortunately I discovered that this

let _ = CleanupHelper(self, permission_info);

doesn't work. Returning the CleanupHelper out of the function does work, but it means the caller might stash the CleanupHelper away somewhere, create another Permission, and cause UB when they get around to dropping the CleanupHelper. :frowning:

Is it not possible to perform operations involving the UnsafeCell via the Permission<'_> (or a deconstruction of the Permission<'_>) in cleanup_permission?

Sadly no. Otherwise I'd just do it in Permission's Drop handler. The cleanup operation needs access to stuff that's in the Database state but not accessible through Permission.

Miri doesn't complain if you use *mut instead.

Oh! I was under the impression miri was tracking the variance of the lifetimes associated with the references. I attributed this working to the fact that my version changed the &mut to a regular &, but your PhantomData uses &mut too. Therefore it seems like miri must be tracking the references themselves (but not pointers) huh... :thinking:

Thanks as always for your time and thoughts.

5

Right, so, that answers a couple of my questions... you apparently really do need the rest of the function to run definitely immediately. If you could require &mut self that would fix it, but I bet that doesn't work for you either.

&'a mut T is covariant in 'a (but invariant in T).

The problem isn't a lack of variance, it's that the reference must be valid for the entire method body (regardless of variance),[1] combined with &mut _ being exclusive. So any access to the *perm.0 memory has to go through the perm.0 in that method.

Another fix potential fix is

struct Permission<'a>(&'a UnsafeCell<Box<usize>>);

impl Permission<'_> {
    fn increment(&self) {
        unsafe { **self.0.get() += 1; }
    }
}

In this case the exclusive &muts only need exist in the increment body. But it will make Permission not Send. (OTOH you can only call cleanup_permission on the Database thread anyway (or you're unsound due to a bad Sync implementation)).

Another possible approach is RefCell instead of UnsafeCell, perhaps utilizing map_split.

  1. discussed in Example 2 of the MaybeDangling RFC ↩︎

2 Likes