Why multiple mutbale reference to a same local varible can exist in move IR?

Move
#1

My code is as following:

module SandCoin {
    public func1() {
        let a: u64;
        let b: &mut u64;
        let c: &mut u64;

        a = 1;

        b = &mut a;
        c = &mut a;

        return;
    }
}

when I execute cargo run -p compiler -- --no-stdlib ./test.mvir, the compiler tells me there is no error in bytecodes, but I DON’T think the variable b and c is reasonable here.

#2

Thanks for the question!

At first glance, this code might seem dangerous, but it is actually safe. In the Move bytecode, you can have multiple mutable references to a given location, but only one of those references can be used at any point in time.

In your example, c cannot be modified nor read from – only b can be used. Once b is released c can be used.

For example

// VALID
a = 1;
b = &mut a;
c = &mut a;
*move(b) = 2;
*move(c) = 2;

// INVALID
a = 1;
b = &mut a;
c = &mut a;
*move(c) = 2; // error `a` is being borrowed by `b`
*move(b) = 2;

In some sense, the Move bytecode verifier separates the creation of references from the usage of references. This allows for very nuanced programs, even though it might seem dangerous in some examples (but luckily it is not).

More in depth:

Internally to the bytecode verifier, borrow relationships are modeled as a graph.

In the example

a = 1;
b = &mut a;
c = &mut a;

We would say that the local a is borrowed by the reference stored in c which is borrowed by the reference stored in b. Thus b can be mutated as it is not being borrowed. But c cannot be mutated as it is being borrowed by b

It might seem a bit quirky that c is being borrowed by b, when c was assigned after b. When a location is borrowed again, any existing borrows are transferred to the new reference.

So

a = 1;
b = &mut a;

The local a is borrowed by the reference stored in b

c = &mut a;

After this line, the local a is borrowed by the reference stored in c. The existing borrows on a are transferred to the reference stored in c. So the reference stored in c is being borrowed by the reference stored in b.

1 Like
#3

Thanks for replying!

After reading the source code of language/bytecode-verifier/src/borrow_graph.rs and language/bytecode-verifier/src/type_memory_safety.rs, I found that your describing is correct.

But… as you’ve said, it’s really a bit quirky and indirect that c is being borrowed by b, although it’s really true that there is a strong empty edge from nonce of c and nonce of b in borrow graph after the calling to BorrowGraph::add_strong_edge. If I don’t read the source code, I may never know why multiple mutable references to a common local variable is feasible in Move but only one of those can be used. Contrarily, the error info is clear in Rust:

cannot borrow `a` as mutable more than once at a time

Now I wonder about another two questions:

  1. With this “a little naughty” feature, how to prove that your borrow checker still working correctly? :smile:
  2. The code of function AbstractState::borrow_local_value is:
    /// update self to reflect a borrow of a value local@idx by new_nonce
pub fn borrow_local_value(&mut self, mut_: bool, idx: LocalIndex) -> Option<Nonce> {
    checked_precondition!(self.locals[&idx].value.is_value());
    if !mut_ {
        // nothing to check in case borrow is mutable since the frame cannot have a NIL outgoing edge
        let borrowed_nonces = self
            .borrow_graph
            .consistent_borrows(self.frame_root, LabelElem::Local(idx));
        if !self.all_nonces_immutable(borrowed_nonces) {
            return None;
        }
    }
    let new_nonce = self.add_nonce();
    self.borrow_graph
        .add_strong_edge(self.frame_root, vec![LabelElem::Local(idx)], new_nonce);
    Some(new_nonce)
}
    It seems that you skip the check of mutable reference deliberately, but why don’t you add a test here to check that a variable has been mutable referenced before?
1 Like
#4

With this “a little naughty” feature, how to prove that your borrow checker still working correctly?

We have type soundness properties over the borrow checker. The internal state only needs to know that there is a unique modifier for a mutable reference, it does not matter if there exists more than one mutable borrow.

We maintain very detailed information in our borrow graph, which lets us know which mutable reference is currently “owning” the location.

The code of function AbstractState::borrow_local_value … It seems that you skip the check of mutable reference deliberately, but why don’t you add a test here to check that a variable has been mutable referenced before?

There is nothing to check for mutable borrow, because you can have more than once mutable borrow! The borrow graph code in add_strong_edge will correctly transfer the existing borrows to this new reference

We need to perform a check on the immutable case to prevent both immutable and mutable borrows on the same source location (if an immutable borrow exists, all transitive borrows must also be immutable)

1 Like