Freezing &mut only works for locals.

[michaelwoerister]

The following is an example program that shows what I mean:

struct Stuff {
    x: int,
    y: int
}

// This works fine:
fn borrow_local_mut_to_immutable(stuff: &mut Stuff)
{
    let a : &mut int = &mut stuff.x;
    let c = copy_out_of_immutable(&stuff.y);
}

// But this does not:
fn borrow_mut_to_immutable(stuff: &mut Stuff)
{
    let a = borrow_part(stuff);
    let c = copy_out_of_immutable(&stuff.y);
}

fn borrow_part<'a>(stuff: &'a mut Stuff) -> &'a mut int {
    return &mut stuff.x;
}

fn copy_out_of_immutable(int_ref: &int) -> int {
    return *int_ref;
}

fn main() {

    let mut stuff = Stuff { x: 10, y: 20 };

    borrow_local_mut_to_immutable(&mut stuff);
    borrow_mut_to_immutable(&mut stuff);
}

The compiler error is:

/home/mw/playground-rust/borrow-mut-to-imm.rs:17:34: 17:42 error: cannot borrow `(*stuff).y` as immutable because it is also borrowed as mutable
/home/mw/playground-rust/borrow-mut-to-imm.rs:17     let c = copy_out_of_immutable(&stuff.y);
                                                                                   ^~~~~~~~
/home/mw/playground-rust/borrow-mut-to-imm.rs:16:24: 16:29 note: second borrow of `(*stuff).y` occurs here
/home/mw/playground-rust/borrow-mut-to-imm.rs:16     let a = borrow_part(stuff);
                                                                         ^~~~~

I think the borrow checker should allow both cases. During the execution of copy_out_of_immutable() no mutable alias to neither stuff nor stuff.y is accessible, so it is guaranteed that the data behind the immutable reference won't change.

This might be the same as #6268 (although I think it is a bit different).

[alexcrichton]

I think that this is a legit error, although perhaps the error message could be improved. The problem is that the compiler doesn't know what borrow_part is borrowing. If it returned &mut stuff.y, then if the compiler allowed the call to copy_out_of_immutable you could possibly create an alias to the y field.

The error message makes you think that (*stuff).y was borrowed by the call to borrow_part, which is technically true but the whole truth is that all of (*stuff) was borrowed with the call to borrow_part because the compiler can't actually determine what was borrowed from that function.

That's also why the first case works, it's because the compiler knows exactly what's been borrowed stuff.x so it knows it can also give out a loan on stuff.y.

[michaelwoerister]

That's also why the first case works, it's because the compiler knows exactly what's been borrowed stuff.x so it knows it can also give out a loan on stuff.y.

That's true.

However, I still think it would be completely safe to allow for passing the immutable reference to copy_out_of_immutable because there is no way that an alias to stuff.y could leak out of the call.
I don't see a problem with temporarily treating an &mut reference as an immutable & reference, given of course, that the immutable reference goes out of scope before the mutable one is used again. In a case like this one (where the reference is passed to a function as immutable and the function returns a type that does not contain any references) this should also be provable locally at the call-site.
(Thinking about it, this case reminds me of the Uniqueness and Reference Immutability for Safe Parallelism paper)

[bblum]

10 brownie points to @alexcrichton for saying exactly what I wanted to say

@michaelwoerister -- Before 'pure' was removed, the old borrow-checker used to be able to reason about what copy_out_of_immutable could do with its alias to y. The problem is that if (for example) you added extra arguments to copy_out_of_immutable, you could explode if you passed the result of borrow_part as a second argument. (I think you maybe could achieve the same effect with a Cell inside a &-pointer.) The pure keyword guaranteed that a function wouldn't mutate such arguments if they existed, which allowed extra permissiveness for "borrowing-if-pure".

@nikomatsakis, is this a motivating use case for keeping &const in the language?

[michaelwoerister]

@bblum I think the compiler can still do some reasoning about that now (although it may not be exactly the same as was possible with 'pure').
I'll list the assumptions I am working under, perhaps I have something wrong here.

An & reference
(1) guarantees that there exists no mutable alias to the referenced object,
(2) it allows that there are other & references to the referenced object

From (1) and (2) follows that:
(3) no mutable reference to an & referenced object exists as long as there is any & reference to it,
(4) one cannot upgrade an & reference to an &mut reference because it cannot be guaranteed that there is no other & reference to the same object somewhere else.

An &mut reference
(5) guarantees that it is the only reference to the object, be it mutable or immutable,
(6) it brings with it the right to mutate the object,
(7) but it does not say anything about reading from the object.

So if I have a function taking only & references it is guaranteed to
(8) never introduce any mutable references to its arguments (or their interiors) because of (4)

A function not returning any references (& or &mut)
(9) cannot not create any references that outlive the functions stack frame.

From (8) and (9) follows that a function not returning a reference and taking only immutable reference cannot violate any of '&mut' guarantees (5, 6, 7).

I am not sure how all this relates to @ and @mut pointers, but for the case above, I think the reasoning should be sound.

The reason for my longwinded argumentation is that this is a pretty common case and I think it might be off-putting to people if they can't do something that they know to be safe and that is no problem in other languages.

Concerning &const, I think refining the rules for & and &mut a little more might make removing it easier.

[bblum]

Hmm, I think your reasoning is right (and the motivation to make the borrow-checker more permissible is definitely right).

The best counterexample I came up with would be something like:

fn use_immutably(x: &Option<T>, blk: &fn(&T)) { blk(x.get_ref()); } // this borrowchecks today

let x = Some(...);
let y = &mut x;
do use_immutably(&x) |inner_ptr| {
    *y = None; // inner_ptr invalidated
}

But the catch is that the closure captures a mutable borrow in its environment, so is secretly a mutable borrow itself. (And we are already planning to track whether stack closures are 'secretly mutable borrows', so we would be able to notice this case.)

[bblum]

The risk with adding this sort of permissiveness is that, while it allows more cases, it makes the set of cases that are allowed defined by more complicated rules and hence more difficult to fully understand. (I think the same has come up regarding making the borrow-checker more flow-sensitive.) As I see it the tradeoff is between confusing people earlier by forbidding seemingly-legal code and confusing people later with a more complex overall model.

(Personally I am fine with this suggested rule, but others may see it differently?)

[michaelwoerister]

@bblum Thanks for taking the time to think about this. I am aware of the trade off. However, I think this case could be okay because it is kind of intuitive ("I hold the exclusive right to modify something right now, I should be able to temporarily give somebody else the right to read from it") and all information needed is available statically (no need to know the current runtime state of something) and locally (no need to look anywhere else but the current function body to know what's going on---well, except one has to know that the return type of the function does not contain any references).

Regarding your example: This would be a different case from the one above because the mutable and the immutable reference are both accessible at the same time, while in my example the mutable reference would not be accessible during the execution of the function taking the immutable reference (which is the crucial condition for making this safe).

But I do hear you about making the overall ruleset more complicated.

[nikomatsakis]

There are certainly ways we could make the compiler smarter. In this particular case, one issue is that we have generally tried to draw the line at "alias analysis"---that is, we make no effort to determine what set of values is "reachable" from a called function, but instead assume that it can somehow connive its way into accessing everything. I am not opposed to extending the borrow checker to make it smarter, but I am wary of doing so now, since we are still finishing up the corner cases on the current set of rules.

[nikomatsakis]

I thought about this a bit more. The big challenge here is that (1) we do not currently treat borrows for calls differently than other borrows in the borrow checker and (2) we do not track nor know of the connection between a and self.x here:

fn borrow_mut_to_immutable(stuff: &mut Stuff)
{ // lifetime 'a
    let a: &'a mut Foo = borrow_part(&'a mut *stuff);
    let c = copy_out_of_immutable(&'b stuff.y); // call has lifetime 'b
}

Here I made the implicit stuff more explicit. What winds up happening from the borrow checker's point of view is that *stuff gets borrowed for the lifetime 'a, which makes stuff and *stuff inaccessible for that lifetime. Then, separately and independently, this new pointer a comes into existence that has the lifetime 'a. It does not know of any explicit connection between them. (Of course, the type system rules will guarantee that any pointer derived from the input to borrow_part() must have the same lifetime or smaller, but the connection between the return value and the input is not declared to the caller)

So now what would have to happen is that when &stuff.y is borrowed for 'b, we must ensure that any mutable pointers pointing into stuff are frozen for 'b, but we don't know what those pointers are. *stuff is already borrowed (hence the current error) so it wouldn't change anything to freeze that. Note that none of this reasoning was specific to calls. We haven't even gotten to the call yet, just the creation of the pointer that was going to be given as argument.

What we could do in such a situation is, in lieu of reporting an error, just go and effectively freeze everything, since we can't know for sure what we need to freeze. This is effectively what the old purity rules did. We'd want to think hard about the precise mechanism for doing this. We can of course get away with not freezing some stuff, and we'd have to decide where to draw the line. This is what I meant before by "alias analysis", since effectively we're trying to write some rules to decide what might and might not alias stuff.y.

[michaelwoerister]

So now what would have to happen is that when &stuff.y is borrowed for 'b, we must ensure that any mutable pointers pointing into stuff are frozen for 'b, but we don't know what those pointers are.

Yes, this probably is the hole in my argumentation. I thought we statically knew--- by construction ---that the initial &mut Stuff reference would not have any aliases in the program (which should be true for & [mut] aliases). That is, there is no other &mut or & pointer to the object behind stuff or any of its interior objects because otherwise borrow checking should have failed already earlier. What I did not properly take into account though are @mut boxes where this can't be verified at compile time. I need to think a little more about this, but I guess my initial mental model of the situation was a bit too simplistic.

If it were necessary to add another restriction, that no @mut boxes must be reachable from the & argument to copy_out_of_immutable(), then I guess it just gets to complicated for the user and the whole new set of rules jumps the shark.

[nikomatsakis]

@michaelwoerister Your model was a bit simplistic, but it is not the problem here. You were correct that &mut is effectively unaliased -- there may be @mut aliases out there, which can be used for reading, but if there is an attempt to write via such an alias a dynamic error is thrown.

The problem is more in the details of how much information the borrow checker has. At the point where, in your example, you do &stuff.x, all that it knows is that stuff was already borrowed, but it doesn't know which other &mut pointers correspond to data in stuff vs somewhere else. This is why I said we would have to conservatively block access to all accessible data.

[nikomatsakis]

Or at least block write access, I should say.

[catamorphism]

@nikomatsakis says this is a wontfix.