What is the exact meaing of the restriction brought by a lifetime annotation

Where is the foo? Is it the ii? I see it below. You must give me the wrong link...

You're not confused here.

But I suggest you thoroughly read the sentences from @quinedot , especially

There are different examples, foo with a lifetime 'b is in Limits of Lifetimes - The Rustonomicon. Resembly, why the reference/borrow in my example does not have a short lifetime as rf in its scope?

It is true that the lifetime of a type cannot be shorter than the liveness scope of the value within it. If that was the case, you would have a value that was still live (used) after the lifetime expired. So since the loan is used at the top and bottom of the (non-branching) block which was illustratively labeled 'c, the lifetime of the type of loan must be (at least) the entirety of 'c.

But the lifetime of a type can be longer than the liveness scope of the value within it. So just because you have a &'static i32 in a variable, that doesn't mean the variable cannot be dropped before the end of the program.

(There were a lot of quick replies so hopefully I've correctly understood what this particular comment was about.)


The links I mentioned, which have perhaps been shared before:

  • Liveness, of both values and of lifetimes, and how they relate
    • After that are a number of sections about generating NLL constraints, and then
  • Solving constraints, which implies the shortest-valid-possible property of inferred lifetimes

    Once the constraints are created, the inference algorithm solves the constraints. This is done via fixed-point iteration: each lifetime variable begins as an empty set and we iterate over the constraints, repeatedly growing the lifetimes until they are big enough to satisfy all constraints.

  • The introduction to Polonius and the next post regarding region errors provide an alternative interpretation of borrow checking (Polonius is the next-generation borrow checker)
    • But again the approach consists of analyzing where borrows are used and detecting conflicting uses; the lack of a conflict implies a valid program

The algorithms described in these links are not simple by any means, and aren't necessarily something you need to keep in your head as a mental model of how lifetimes work on a day-to-day basis. The reason I've shared them / referred to them earlier is that I feel they illustrate that inferred lifetimes aren't the output of some block-based or unidirectional analysis. Instead, there is an analysis of obligations over an entire function body, and if no conflicts are detected, the inferred lifetime has been proved valid.

That's what lifetimes in Rust are ultimately about: proving that they are in some sense valid, proving that your program is memory safe. If the compiler can prove it, you're good. If it can't, it throws an error. The nominally concrete lifetimes inferred are useful to aid human understanding of why a program is valid, but are technically unnecessary so long as the proof holds.

2 Likes

The key thing to notice is that a lifetime annotation 'a means two different things in two contexts:

  • As a bound on a type: T: 'a means that values of type T are valid at least as long as 'a (potentially longer), so you can (but don't have to) create a reference of type &'a T to such a value.
  • In a reference: &'a T means that the referent will live at least as long as 'a.
3 Likes

For this comment, you mean here? I'll assume so:

fn shrink_the_lifetime<'a>(original_static:&'a i32, used_for_shrink:&'a i32){}
fn main(){
   static I:i32 = 0; // 'static -------------------------------------+
   let rf; // Liveness scope 'rf ---------------------------------+  |
   { //                                                           |  |
      rf = &I;     // &'static_or_shorter i32 --------------------+  |
      let ii = 0;  // Liveness scope 'ii --------------------+    |  |
      let rf_block = &ii; // &'ii_or_shorter i32 --------+   |    |  |
      shrink_the_lifetime(     //                        |   |    |  |
          rf,  // -- a reborrow &'short i32 --------+    |   |    |  |
          rf_block // also a reborrow &'short i32 --+    |   |    |  |
      ) // The reborrows only have to last for      |    |   |    |  |
      ; // the call to the function ----------------+    |   |    |  |
       // -------- No more uses of rf_block -------------+   |    |  |
   }   // -------- End of 'ii -------------------------------+    |  |
   rf; // -------- End of 'rf ------------------------------------+  |
} //                                                                 :

I'm guessing the confusion is, how can rf still be valid after the inner block if it was forced to have a lifetime limited by the inner block? And the answer is that it wasn't actually limited to the inner block by the call to shrink_lifetime, because when you pass a function argument, it can be coerced to a subtype (in this case a shorter lifetime), which means that there is an implicit reborrow that goes on here, as if you had typed

shrink_the_lifetime(&*rf, &*rf_block);

So this function call doesn't actually have to restrict the lifetime inferred for the type of rf; the type of the values passed to the function can be different than rf and rf_block (they can have shorter lifetimes).

Reborrows are another one of those woefully underdocumented features of the language.


OK, so. I'm going to forge ahead here in anticipation of follow-up questions, which would be completely reasonable. Understanding reborrows is pretty important to understanding why various programs compile, whereas the rest of this post goes into examples which, in my experience, you probably won't need to worry about from a practical perspective.

So perhaps stop here until you have a firm grasp on reborrows. Or even stop here forever! I ramble on quite a bit.


Anyway, forging ahead. How can we actually limit the lifetime of rf in some way the compiler doesn't like? Here's one way:

   static I:i32 = 0;
   let mut rf;
   {
      rf = &I;
      let ii = 0;
      let rf_block = &ii;
      rf = rf_block;
   }
   rf;

It's probably pretty easy to see why this is problematic:

  • You put a borrow of ii into rf
  • You drop ii
  • You use rf, but it still points to ii, which has been dropped

So we could say that rf had a lifetime that was inferred to end when the inner block did, so the use after the block was invalid.

But you've tenacious about fleshing out the rules, so perhaps you'll push on forward to try this:

   static I:i32 = 0;
   let mut rf;
   {
      rf = &I;                  // (a)
      let ii = 0;               // (b)
      let rf_block = &ii;       // (c)
      rf = rf_block;            // (d)
      rf = &I; // new           // (e)
   }
   rf;                          // (f)

Now it compiles again, and most mental models of the analysis which also account for strict, static typing (including lifetimes) will fail to explain why this is allowed:

  • rf_block has a static type with a lifetime limited to the inner block ('rfb)
  • rf has a static type with a lifetime that must be valid outside the inner block ('rf)
  • But somehow we could assign rf_block to rf, implying 'rfb: 'rf

This is where things like liveness analysis come in:

  • The borrow of I at (a) is doesn't need to exist beyond (a)
    • It isn't used after it's created
  • The borrow of ii at (c) needs to exist at (c) and (d), where it is created then used
    • It gets killed at (e) by rf being overwritten, after which rf_block no longer used
  • The borrow of I at (e) needs to be valid of (e) and (f)

So what's the lifetime of the static types of rf and rf_block? There is no simple answer because NLL lifetimes are codepoint and control-flow sensitive. The lifetimes are perhaps something like

'rf:
  at (a), {(a)}
  at (b), {}
  at (c), {}
  at (d), {(d)} // lifetimes are "forward looking", no need to include (b) (c)
  at (e), {(e), (f)}
  at (f), {(f)} // similarly no need to include (e) here
'rfb:
  at (c), {(c), (d)}
  at (d), {(d)}

And 'rfb: 'rf at (d).

I must also admit, I'm still being cagey by saying "perhaps" here, because I didn't actually take the time to walk through the entire NLL algorithm as presented in the RFC.

So I'm afraid to say, there is no simple explanation of lifetimes for every scenario. Inferred lifetimes are the output of a static, but liveness and control-flow sensitive, analysis of your code.


The practical approach to getting a deeper grasp on Rust lifetimes, in my opinion, is to build a mental model that explains common patterns and lifetime errors. This mental model will probably be more simplistic than the actual compiler analysis. That is, there may be programs which compile which shouldn't under your mental model, like the example just given. But so long as your mental model is strictly too conservative, this is -- from a practical perspective -- usually still okay. If your program compiles, you generally just assume the compiler proved it was sound, and you don't have to think about it.

Instead, this mental model can provide an answer as to why the compiler gave you an error, after which you'll either think

Occasionally you'll also be surprised when things do compile, and you may have to expand your mental model (e.g. to accommodate reborrows). This is mostly true (in my experience) as you are still learning and building up your mental model, i.e., you'll be adjusting for failure modes long after you'll be adjusting for success modes.

I agree this isn't the most satisfying when you're trying to develop a complete understanding of the rules, or even appropriate when you're trying to suss out compiler bugs where it has potentially allowed an unsound program to compile. But I also feel such a complete understanding isn't actually possible (as there is no specification and even compiler experts are occasionally surprised / create bugs).

I have long wished for a "Rust lifetime book" to present an adequately complete, but not overwhelmingly complex, mental model. Alas, as far as I know, it does not exist.


Another approach is to build a mental model which is also sound, but potentially more general than the compiler / Rust itself. This is the goal of stacked borrows. It isn't concerned with static types per se, it tracks borrows themselves as a runtime analysis.

Let me take another shot at the last example under my looser mental take on stacked borrows, ala those diagrams I've presented before:

   static I:i32 = 0; // ----- lifetime of I ------+------------------+
   let mut rf; //                                 |                  |
   {           //                                 |                  |
      rf = &I;                  // (a) -- I used -+ ~ rf 1st used ~* |
      // But the borrow isn't used after (a)...                    : |
      let ii = 0;               // (b) ----+-- lifetime of ii ---+ : |
      //          ii is about to get used  |                     | : |
      let rf_block = &ii;       // (c) ----+  This borrow gets   | : |
                                //         |  used but not       | : |
      rf = rf_block;            // (d) ----+  after (d)          | : |
      // ii is not longer used after here -----------------------+ : |
      rf = &I; // new           // (e) -------+                    : |
   } //                                       |                    : |
   rf;                          // (f) -------+                    : |
   // ~~~~~ rf no longer used ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~* |
   //                                                                :

If we accept the fudging about rf not being used until sometime after it's declared, it works (there are no crossed edges). But I admit, this take is still a mental model weaker than stacked borrows itself, and is still pretty much a static analysis. (Granted, the example is linear.)

A more formal look at this example with stacked borrows would instead actually write out the stacks of every memory location with the tags of the borrows, etc. My apologies, but I'm not going to do that here. But if you run Miri (under tools in the playground), that uses stacked borrows, and it accepts the program.

Both what I've presented here, and doing the formal analysis, are exercises in showing a lack of runtime memory unsafety, in contrast with an exercise in determining what static lifetime (variable type) the compiler inferred. I.e.,

  • Useful for convincing ourselves it's ok Rust accepted some program
  • Useful for demonstrating why it's right Rust rejected some program
  • Useful for arguing that Rust rejected a program it could have accepted
  • Not necessarily useful for figuring out what the compiler actually does or what a lifetime was inferred to be

As is probably clear if you have read this far, even though I have what I feel is a decent grasp on Rust lifetimes, I am still primarily exercising mental models that are more simplistic than the actual analysis the compiler (or Miri) perform. If you read the NLL RFC, I think you'll agree that it is quite low-level and challenging to perform in your head. And as I also said, I feel it is impractical to not have a mental model simpler than the compiler itself.

Therefore, I encourage to develop your own mental models that sufficiently explain Rust lifetimes most of the time, even if they are not technically speaking complete. And that includes continuing to ask questions like you have been in this thread!

2 Likes

This point will make the wording in the book false. The book says

The lifetime system is forced to extend the &mut foo to have lifetime 'c, due to the lifetime of loan and mutate_and_share's signature.

The book says the reference/borrow will live for 'c. However, you say the referent should live longer than 'c.

So, this is a confusion that, for &'a T, does 'a denotes the lifetime of the reference or the lifetime of the referent?

There's no contradiction: the reference may live for 'c (it may be dropped earlier, but that's irrelevant); therefore, the referent must live for 'c (so that the reference won't dangle).

1 Like

You are confusing the lifetime annotation of the type with that of the reference; this is exactly what I was trying to clear up in my previous answer. T: 'a and &'a T are not the same. T: 'a means you are allowed to create a &'a T, because the value of type T is valid for the lifetime 'a at least. Whereas if you already created a reference, it necessarily means that the referent lives at least as long as the reference (otherwise there would be a dangling reference).

1 Like

It's the lifetime of the borrow; it's the lifetime/validity-region of the type of the reference.

It can't be longer than the liveness scope of the referent (that would be a dangling reference), but it could be shorter.

It can't be shorter than the liveness scope of the reference (that would be an invalid reference / allow data races), but it could be longer.

  • Let type T: 't (T is only valid at 't)
  • Let value/variable t: T last until 'u (its liveness scope is 'u)
    • t can't outlast 't so 't: 'u
  • let r: &'a T = &t
    • 'a can't outlast t can't outlast 'u, so 'u: 'a
  • Let value/variable r last until 'b (its liveness scope is 'b)
    • r can't outlast 'a so 'a: 'b
't : 'u : 'a : 'b
 ^    ^    ^    ^___ liveness scope of the reference
 |    |    |________ lifetime of the borrow of the referent
 |    |                  (and validity region of the type `&'a T`)
 |    |_____________ liveness scope of the referent
 |__________________ validity region of the type `T`

The wording of the page you keep quoting is just one interpretation (mental model) of the borrow check finding a conflict. It says

  • &mut foo is forced to have lifetime 'c
  • Then we call share and we get an error because it aliases &'c mut foo

But another interpretation is

  • loan is a &'foo mut foo for some 'foo
  • The call to share invalidates the exclusive borrow, so 'foo ends before 'd
    • Could be phrased "&mut foo is forced to have a lifetime less than 'd"
  • Then at the println! you try to use the invalidated &'foo mut foo

This interpretation is just as valid of a mental model IMO, but the type of loan was never "forced to have lifetime 'c". Instead it was prevented from having lifetime 'c, which then became a problem when you tried to use it at the end of 'c!

Between these two interpretations, which lifetime does the type of loan actually have? I feel it's a vacuous question in some sense because the entire function is undefined (has no sound solution in current Rust). Under the 'c interpretation, the share call conflicts. Under the other interpretation, loan is invalid at the println!. In the end, loan has no valid lifetime. Both interpretations fail to find a sound solution.

4 Likes

Thanks. So, the interpretation of the example in nomicon is not a canonical/standard interpretation. It is just a reasonable interpretation, Right? For my second example

fn main(){
    static I:i32 = 0;
    let rf;
   {
      let rf_block = &I; // the type of rf_block is &'static i32
      rf = rf_block;
   }
  rf;
}

The type of rf_block can be &'static i32. By this logic, it seems we can also intepret the first example by this way.

fn main() {
    'b: {
        let mut foo: Foo = Foo;
        'c: {
            let loan: &'b Foo = Foo::mutate_and_share::<'b>(&'b mut foo);
            'd: {
                Foo::share::<'d>(&'d foo);
            }
            println!("{:?}", loan);
        }
    }
}

The type of loan can also be &'b Foo, have the similar manner to the the first example in this comment. In 'd, there is another reference that is excluded by a mutable reference in 'b, where 'd overlaps with 'b, hence the example is also invalid in this interpretation, Right?

Merely, if we had a mutable reference with lifetime 'b, then the mutable reference would also prevent we from using variable foo in 'b, which seems to result in the overly borrowed.

From this perspective, that is to say, how the lifetime a reference will exactly have is opaque. It is the internal strategy of the compiler. In other words, the compiler can try best to limit a reference with a minimal lifetime as long as the program can be compiled with that inferred lifetime.


Still with the example in the second question

'static:{
   let I = 0;
   fn main(){
     'a:{
      let rf:&'? i32 = &I;  
      test_lifetime(rf); // the trait bound requires `&'a i32` to satisfy 'static
     }
  }
}

the borrow produced by &I should have had the lifetime 'a, however, with that lifetime, the call to test_lifetime would be an error. So, the minimal lifetime that can be inferred for rf should be 'static, and the borrowed content I has lifetime 'static, so the inferred lifetime 'static is ok. Hence, the eventually usable minimal guaranteed lifetime for rf is 'static, Right?

I agree with everything here.

I thought of another way to phrase my last reply that doesn't rely on defining what exactly a lifetime is. Instead, we can use an analogy to another type of problem entirely: Satisfiability.

Consider the following boolean formula:

( a | !b |  c) &
(!a | !b |  c) &
(!a |  b | !c) &
( a |  b | !c) &
( a |  b |  c) &
(!a |  b |  c) &
( a | !b | !c) &
(!a | !b | !c)

We want to satisfy it in some way. If the entire formula is true, what are the values of the variables?

As it turns out, there is no way to assign values so that the formula is true, so that's a bummer. But what is the value of a? It doesn't matter -- if a is true we can't solve it, and if a is false, we still can't solve it. We could pick one and then show the reduced formula is still unsolvable, but it wouldn't matter which we pick.

I could say, "Because of XYZ, a must be true. But then there's a conflict because...". Or I could say, "Becaues of UVW, a must be false. But then there's a conflict because...". Both could be legitimate ways to explain why the formula as a whole cannot be satisfied.

How about this one?

(!a |  b | !c) &
( a |  b | !c) &
( a |  b |  c) &
(!a |  b |  c)

This one is satisfiable. So what is the value of a? We still don't necessarily know! If a is false, the reduced formula is still satisfiable, but that is also the case if a is true. There are multiple values for the variables that work. We do happen to know that b must be true though -- if b were false, the reduced formula is not satisfiable.

We can explain why it's satisfiable by picking some specific values for all the variables and walking through it, but again there might be multiple viable ways to do so.


Similarly, a lifetime solver borrow checker doesn't have to assign a concrete lifetime to every type per se; it just needs to prove that the constraints are solvable or not. Sometimes that will boil down to some single possibilities ("rf must be 'static for this to work") and sometimes it won't.

Getting into what those constraints have to be in order guarantee soundness [1], or how to make an algorithm to solve the problem, or sometimes trying to understand what the heck the compiler error was trying to tell you... that is when you start reading things like Stacked Borrows and the NLL RFC.


  1. and to remain somewhat comprehensible to us humans ↩ī¸Ž

4 Likes

In short, could I just understand the borrow checker as that?

For a given context, the borrow checker tries its best to find out a set of lifetime values in order to make the rules true. If there does not exists such a set, or the found set will contradict other rules, the borrow checker will emit an error.

@quinedot Anyway, another thing should be confirmed here due to the opinion of @H2CO3 in his comment.

Given a type &'a T, we seem to agree that the lifetime value is used to describe how long the borrow/reference(i.e. the value adorned by the type &'a T) will live rather than how long the referent/borrowed context will live. The borrowed content/referent must live at least longer as 'a, which guarantees that we do not have a dangling reference. However, IIUC, @H2CO3 seems to consider that the lifetime value 'a describes how long the referent/borrowed context will live. I think they are totally different interpretations. This issue just backs to the subject of this question, what stuff does the lifetime annotation in &'a T directly restrict?

&'a T describes & constrains

  • how long the borrow/reference will live: &'a is apparent
  • and how long the referent/borrowed context will live: &'a T implies T: 'a, because if T lives shorter than 'a, &T can't live longer than 'a

It's causality. You must get T: 'a first, then you'll have &'a T, which is how Rust works.

1 Like

Yes.

If we're going to be this nuanced, you better be more specific than "borrow/reference". The borrow/lifetime-in-type-of-the-reference can be longer than the liveness-scope-of-the-reference/when-the-value-becomes-dead, which is why you can assign a &'static _ reference to a local variable. ('a vs 'b in this diagram.)

I think the interpretations are the same, modulo the amount of explicit nuance articulated. They said

the value of type T is valid for the lifetime 'a at least

Emphasis on "at least". They didn't say "is exactly 'a".

3 Likes

In &'a T, lifetime 'a serves as a bound for both reference and referent, but in a different ways:

  • For reference, it's the largest possible region of existence (it may exist in part of it, but not beyond).
  • For referent, it's the smallest possible region of validity (it may be valid beyond it, but not only for part).
3 Likes

@quinedot Through thinking about the relation between the referent and the reference, return to the example in the question. I have a question. The current is that the lifetime parameter in the method signature requires that the borrowing to foo should keep alive for 'c since the loan should be valid in 'c. This is the current interpretation and the reason why the example is an error. However, it appears to me that loan is the borrowing to the entity foo, in this example, we just need to guarantee foo itself outlives 'c, in this situation, we can guarantee the loan always not be a dangling reference, in other words, we do not need & mut foo to alive for 'c, it can be dead just after the call returns. Why doesn't the compiler adopt this strategy to avoid creating the mutable borrow & mut foo whose lifetime is not necessary to be so long?

This would be some sort of dual-lifetime borrow, wherein:

    let mut foo = Foo;
    let loan = foo
        .mutate_and_share() // 'foo_mut starts ...
                            // ...'foo_mut ends, but...
        ;                   // ...'foo_shared starts
    foo.share();  // 'foo_shared_2 starts and ends
    println!("{:?}", loan); // 'foo_shared used again

Why doesn't the compiler do this today? On one level, that's just not how lifetimes work -- the returned reference has to be a reborrow of the input reference, so the input reference has to last at least as long, and so on.

But there's another reason it can't be made to work that way now -- it would be a backwards-incompatible breaking change, as things like Mutex guards rely on the exclusivity pattern of the current system for soundness. We'd need some distinct function signature to enable this.

This comment is a retread of the first part of this earlier comment.

1 Like

In common sense, the mutable borrow &'c mut foo should overlap with the immutable borrow loan in the region 'c, which is just not permitted by the borrow checker, however, the example can be compiled, is this the magic of "reborrow" such that the example ok?