[blog post] Nested method calls via two-phase borrowing

We could consider reserved borrows to be something akin to the old const borrows we used to support: these would permit reads and writes of the original path, but not moves. There are some tricky cases to be careful of (for example, if you reserve *b where b: Box, you cannot permit people to mutate b, because that would cause the existing value to be dropped and hence invalidate your existing reference to *b), but it seems like there is nothing fundamentally stopping us. I did not propose this because (a) I would prefer not to introduce a third class of borrow restrictions and (b) most examples which would benefit from this change seem quite artificial and not entirely desirable (though there are exceptions). Basically, it seems ok for vec.get({vec.push(2); 0}) to be an error. =)

I had a thought that if a third class of borrow restriction were not only added (scary) but exposed in the type system (much scarier), it could make some helper methods more ergonomic - ones that look like:

fn get_baz(&mut self) -> &mut Baz { &mut self.foo.bar.baz }

Right now, calling that locks you out of the whole rest of self, because the contract is "return value is alive and won't be touched as long as self is alive and won't be touched". In theory, if you could change the signature to have the contract just be "return value is alive as long as self is alive", and then later "activate" it into a mutable borrow (which would still lock out all of self, but only temporarily), you could greatly reduce spurious lifetime conflicts.

But that doesn't help if baz is behind a pointer or option or something, because then that contract can't be guaranteed. So this is probably a dumb idea. If the problem needs solving at all, I guess it would be better to approach it with things like "which fields I borrow" specifications on methods (which are really ugly, but at least more flexible).

The v.push(v.len()) thing makes me wonder. Are such nested function calls codified? Someone on /r/rust mentions that they don't understand why it's not desugared to

let foo = v.len(); v.push(foo)

which is good enough in that simple case, but what about more complex things, like

foo.bar().baz(foo.qux())

where bar, baz and qux might do arbitrary things?

I think that if you start allowing “yet-to-be-borrowed” lifetimes to be present in types, you can’t rely on the borrow-checker to enforce them, because of things like:

let mut x = 1;
let mut y = 2;
let mut x_ = (&mut x,);
let mut y_ = (&mut y,);
mem::swap(&mut x_, &mut y_);

// must allow (one occurrence) of these lines in both orders, but
// not concurrently
read(*y);
*x_ = 2;

In the “normal” case, the “lifetime as set of points” proposal dually identifies a live lifetime with it’s set of exits. I suppose we can allow for “yet-to-be-live” lifetimes by identifying them with their set of starts and set of exits (and therefore, in the dual “set of points” representation, forcing all points between a start and an exit to be live). We can achieve this in inference by adding dataflow equalities that force regions to be contiguous.

Also, LSP computes the “precise” lifetimes of each borrow by itself - even if you have eqtys, 'a ~ 'b is defined as 'a <: 'b ∧ 'b <: 'a - LSP subverts eqty, so there is no need for borrowck to do its own dataflow.

What I am wondering is whether it can assume that the state will not be read. To step back, when you see a signature like this one:

fn foo<'a>(&'a mut Foo) -> &'a u32

The way I think of it is: you give me exclusive access to some memory containing Foo for the lifetime 'a. I give you back shared access to some memory containing a u32 for the remainder of the lifetime 'a.

There is no a priori reason to think that (a) the u32 is part of the Foo or, even if it is, that (b) I have relinquished my exclusive access to the other parts of Foo.

Now, it may be that one cannot make productive use of those other parts of Foo. For example, if I had (e.g.) started a thread that was accessing the other fields of Foo in parallel, I wouldn't have any way to make that thread stop executing before 'a concluded -- but this argument is subtle, and it relies on the fact that 'a is bound on the method (it's a kind of lifetime parametricity argument).

So I guess what I'm saying is that I can imagine yes that we could make some rules for when the caller must be "relinquishing" their borrow (or at least converting it to a shared borrow) but I'm wary and would like to think more deeply about it. At best that would be a sort of "pattern matching" on the signature, since we don't currently have a way to express that concept in the type system. (Which might be satisfactory.)

Regardless, this is a good example to keep in mind. I've been meaning to write up a post going through my list of "borrowck challenges" -- I think that NLL and the nested method thing addresses a good many of them, but certainly some remain. My personal list I just put into a gist with some very brief notes, but it's probably incomplete.

This is an interesting example. To be clear, the system I was thinking of would consider the mutable borrows of x and y to start immediately, since (in the MIR) the temporary would get used when it is packaged up into a tuple.

If we were just trying to track mutation regions, if seems like the mem::swap line would require that the type of x_ and y_ be equal (at that point), which would seem to imply that their write regions would overlap (at that point). This would then imply that the two borrows are overlapping and an error would be reported, right?

That is, I wouldn't expect this program to be legal, as long as any write occurs (since otherwise the write regions would be empty).

This is what I referred to as “changing the desugaring”. The previous internals thread did indeed discuss various options like that, along with their pros and cons.

I wanted to expand on my answer. I think I overstated the case in my conclusions and comparisons about the "equivalence" between this borrowck-based approach and a type-based approach (even one that guarantees continuous regions). In particular, I intentionally adopted a limited and simple version of "use" (i.e., one that cannot "see through" a move, or embedding the value into a structure). Most likely, if we took a type-based approach, you would get a similar feel, but with a richer notion of "use".

Example:

let a = &mut foo;
let b = a; // alternative: `let b = (a, );`
// is the borrow of `foo` active here?

With a type-based approach, presumably the type of b would be equal to the type of a (or, in the alternative case, it would be a tuple that includes a). I think that if we wanted a richer notion of "use" like this, I'd probably pursue some kind of type-based alternative -- you probably could model it with the borrowck, at least those examples, but there are a host of others where it might not work (e.g., let b = vec![a];).

That said, I don't really feel that's necessary. I think the main goal is to support the simple example of vec.push(vec.len()), not to make a super general concept of "delayed activation" that people will use all the time. I think the simple definition I gave is also readily explainable. When you do let x = &mut..., the next time you refer to x (basically), it is activated. When you do foo(&mut) or some such thing, it is as if you did let tmp = &mut; foo(tmp), and hence it is activated. But I have to ponder it -- perhaps it winds up being confusing in practice.

Yup. The advantage of true type-based approaches is that they work well with functions. And I want to pass multiphase borrows to functions because that solves at least the get/get_mut problem and allows writing the @comex foo function.

On the other thread, I think that discontiguous borrows are an inherent problem of may_dangle lifetimes:

struct Dangling<#[may_dangle] 'r> {
    data: *const u32,
    lifetime: PhantomDanglingLifetime<'r>,
}

fn main() {
    let mut x = None;
    loop {
        let a = 0;
        x = Some(Dangling::new(&a));
    }
}

The reason is that liveness does a very good job in preventing “lifetime use-after-free”, but if we allow dead lifetimes that guarantee is gone - so we need a special category for “non-freed but inactive” lifetimes, and we probably want to bound their lives with another lifetime.

1 Like

Can you elaborate more on how you envision this working?

I mean, at least I would want (note: this only requires delayed initialization + ref-as-a-type):

impl<K, V> HashMap<K, V> {
    fn get_v<'r, #[may_dangle] 'w>(Self: Ref<'r, 'w, Self>, key: &K) -> Ref<'r, 'w, V>;
}

And @comex could write his function in the same way.

Did you mean to write V in the output type instead of Self?

Yeah, my playground link was something like that.

Actually, here's a much simpler example.

struct Something { mutex: Mutex<String> }
impl Something {
    fn one(&mut self) -> &str {
        self.mutex.get_mut().unwrap()
    }
    fn two(&self) {
        *self.mutex.lock().unwrap() = "Surprise!".to_owned();
    }
}

No unsafe code, fixed or invariant lifetimes, or structure returns, just (&mut self) -> &T, but calling two with the borrow from one still active would be Bad.

1 Like

In any case, their model is a kind of generalization of Rust, in that it can accept a lot of programs that standard Rust cannot (it is intended to be used for assigning types to unsafe code as well as safe code).

I feel like there is a misunderstanding here on either your or my side that I should clarify (so sorry in advance for not contributing to the main story directly here, I'll keep it brief): My type system cannot assign types to unsafe code by type-checking. It is true that there are some programs I accept that the compiler doesn't (yet) accept (i.e. around non-lexical lifetimes), but the vast majority of unsafe code is not accepted by the type system, and that was never the goal. However, the type system is sufficiently small and formal that I can define the mathematical contract associated with each type. Then I can "assign a type to unsafe code" by manually proving that the code satisfies the contract. This is useful because it means that the type soundness theorem extends to code using the unsafe code at its given type. That's however not assigning a type to the code in the classical sense, i.e., these contracts are nothing a type checker could have any hope of checking against.

Coming back to the proposal at hand: First of all, at this point we plan to finish the type system we have and write a paper about it, just so that there is something there. Whatever is the solution to this problem, it'll probably not be in that first type system. But of course we may want to amend that later. :wink: Still, reading the blog post, one way of maybe dealing with this that would fit the existing framework fairly well came to my mind, and now I am wondering how close you think that is to your post, @nikomatsakis. I think this thought already lurked in my head when we previously talked about it, but it is much easier to express in your "two-phase borrowing" than it was in "borrowing for the future" or "two-phase lifetimes". Warning, very fresh thoughts ahead. So let's look at this code again:

/* 0 */ tmp0 = &mut vec;   // mutable borrow created here..
/* 1 */ tmp1 = &vec; // <-- shared borrow overlaps here         |
/* 2 */ tmp2 = Vec::len(tmp1); //                               |
/* 3 */ Vec::push(tmp0, tmp2); // ..but not used until here!

So here we have a shared borrow to vec while a mutable borrow is active. That is, on its own, not even a new phenomenon, it can already happen in today's code via re-borrowing. The following is legal, after all:

tmp0 = &mut vec; 
tmp2 = { tmp1 = &*tmp0; Vec::len(tmp1) };
Vec::push(tmp0, tmp2);

I feel like the restrictions for this pattern a pretty much the same as the restrictions you give for two-phase borrows (at least if we allow full NLL), if we just think of the "inactive" phase of the mutable borrow as being a sublifetime for which tmp0 is shared re-borrowed elsewhere. Clearly that shared re-borrow has to end before the next use of tmp0, and only read-only operations are allowed on it.

Of course, the key difference in the first block of code is that tmp1 is initialized from vec, not tmp0, which makes this a fairly strange form of re-borrowing (and we probably would not want to allow it for mutable re-borrows). And of course if tmp0 is based on a field of a struct, it may not be possible to re-write the code into above form. Still I am wondering whether there is some connection here between "not-yet-active" mutable borrows and "shared re-borrowed" mutable borrows.

1 Like

I prefer either desugaring (@RalfJung’s inferred reborrows seem promising), or whole new type (a la @arielb’s). The more magic in the borrow checking / lifetime inference that cannot be expressed directly, the more we risk only increasing expressiveness in a way that’s impossible to abstract over.

With re-borrowing, a new mutable borrow would be fine too:

tmp0 = &mut vec; 
tmp2 = { tmp1 = &mut *tmp0; Vec::push(tmp1, 0) };
Vec::push(tmp0, tmp2);

While this is blatantly unsound with BFTF

tmp0 = &mut vec[..];
tmp1 = &mut vec;
Vec::push(tmp1, 0);
<[_]>::sort(tmp0); // oops, `vec` might have resized

Indeed, I suppose I spoke imprecisely. I did not mean to imply that your type system can "type" unsafe code internals. But I realize that even though we talked about precisely this topic at POPL I am finding myself getting confused, so maybe we can clarify all the moving parts once more (and this time in some place I can search for later).

  • Your system can assign types to fn boundaries.
  • These types include richer invariants, so as to convert things like RefCell and Cell.
  • Custom proofs must be supplied to show that the body of some ref-cell method is "safe".
    • These proofs do, I believe, still refer to and manipulate lifetimes, right?
    • For example, in an unsafe method, we might reason about the fact that we borrowed something, which implies we created a lifetime and used it to bundle up some capabilities, while lending out others
  • Plus there is a "type system" that can be used to show that safe code is "safe"
    • i.e., to prove that any thing which passes the type system will not go wrong

Does this all seem at least not totally inaccurate? In that case, I think what I was trying to say is that the concept of a "lifetime with holes" is a significant change to the underlying logic that those custom proofs for unsafe code is operating in. But please do educate me as to how I am saying this all wrong.

Indeed. I think what you describe is roughly what I had in mind, yes, except that one has to cope with this distinction that you mention here. There is a related example that I discussed with @aturon, where you can see that sometimes reservations might permit mutation that makes the original path irrecoverable:

let mut foo: Box<Vec<u32>>;
let mut bar: Box<Vec<u32>>;
let mut x: &mut Box<Vec<u32>> = &mut foo;
let y = &mut *x;
x = &mut bar;
y.push(...); // pushes into `foo`

Currently, we do not accept this code, which leads to [some contortions around loops] (Permit mutation of `&mut` pointers whose pointees have been borrowed · Issue #10520 · rust-lang/rust · GitHub), but I would like to do so (I seem to recall us talking about this one time, right?). I've not thought very deeply about it just yet.

Yes, the inability to distinguish between borrowing a pointer vs pointee is very annoying. I’m a bit confused how it relates though?

I wanted to show that you can’t always “desugar” a reservation into a shared borrow and then re-evaluating the lvalue path (you might imagine that you can, because evaluating an lvalue path is side-effect free).

(Warning, half a blog-post ahead. I guess I should just make this a full blog post over the week-end, now that I already wrote all this text.^^)

In some sense, I am building two type systems, and I think the confusion here is coming from that. First of all, I am building a "syntactic type system" (usually I'd just call this the type system), which is an attempt to formally capture (an over-approximation of) the safe code that Rust accepts. This looks a lot like most type systems do: There's a grammar of legal types, there are some contexts tracking the types of variables and the lifetimes, there are inference rules telling you e.g. when you can load from a pointer, when you can call a function, and so on. This type system is an over-approximation because I provide more flexibility than rustc does when it comes to lifetimes. However, a design goal of this type system is for every rustc-accepted program not using unsafe blocks (that falls into the fragment I cover) to be (syntactically) well-typed. Notice that the program can call external, unknown functions; this corresponds to type-checking the program in a non-empty context. So, we can derive typing judgments like "If we assume that Cell::new, Cell::get, ... have the type given in libstd, then we can (syntactically) derive that this program is well-typed".

Next, there is a "semantic type system", which I usually call the "(semantic) model of the Rust type system". This model defines, for every type present in the syntactic system, a formal contract that values of the given type have to satisfy. In particular, for function types, the contract says that if all arguments satisfy their contract (as given by the argument types), then the function must execute safely and return something satisfying the contract of the return type. Notice how in defining the contract for function types, we only cared about the contract of the argument and return types -- the "actual types" (as in, their syntactic representation as an instance of the grammar) does not matter at all! This leads us to the idea that really, any contract is a valid "semantic type". This idea is incredibly powerful. We can now write down the contract saying "this is a legal 32-bit integer value representing a prime number". Let's call this type i32even. This type does not exist syntactically, but since we have defined its contract, we now also know the contract e.g. for types like fn(i32even) -> i32even or Option<i32even>. Things compose. So what I do to verify unsafe code is that I define semantic types like Cell<T> that do not exist syntactically. I can then compose these types with things like function types to obtain the contract of fn(T) -> Cell<T>, and then I can show that Cell::new actually satisfies this contract. This is the sense in which my "types include richer invariants", and the sens in which I can "type" unsafe code -- I can semantically type it, but not syntactically. However, since syntactic well-typedness implies semantic well-typedness, the two notions compose together.

This is absolutely correct. However, it may be that "two-phase borrows" also constitute a significant change. :wink: However, "lifetimes with holes" are certainly way further from what my mental model of a lifetime is.[quote="nikomatsakis, post:24, topic:4886"] let mut foo: Box<Vec<u32>>; let mut bar: Box<Vec<u32>>; let mut x: &mut Box<Vec<u32>> = &mut foo; let y = &mut *x; x = &mut bar; y.push(...); // pushes into foo

Currently, we do not accept this code, which leads to some contortions around loops, but I would like to do so (I seem to recall us talking about this one time, right?). I've not thought very deeply about it just yet. [/quote]

Ah, yes we talked about this. I do not understand however how this is related to nested method calls or two-phase borrowing. In my eyes, the only problem here is that rustc thinks x is being reborrowed, but actually it would be much smarter if it was moved instead. Actually, a tiny modification makes rustc accept this program (as has been pointed out to be by Jacques-Henri Jourdan):

let mut foo: Box<Vec<u32>>; let mut bar: Box<Vec<u32>>;
let mut x: &mut Box<Vec<u32>> = &mut foo;
let y = &mut *{x}; // the curly braces make rustc consider this a move out of x, i.e., x is uninitialized after this line
x = &mut bar;
y.push(...);
1 Like

If the borrow-checker was smarter, there would be no problem with a reborrow. If you MIR-assign (as opposed to HIR-assign aka DropAndReplace, which is a drop + an assignment) to a value, all borrows of parts of the value that are not behind a pointer get invalidated (because you overwrite them), but borrows of parts of the value that are behind a pointer get "forgotten" - the values can now only be accessed through the borrow result, so we can clear the borrow.