Note for Rust lifetime

lifetime.md

Lifetimes for The Rust References

Terms

• x outlives y
  • When y is alive, x is alive. But x and y can be destroyed at the same time. That is, x must live at least as long as y.
• x strictly outlives y
  • When y is alive, x is alive, and x must be alive when y is destroyed. That is, x lives longer than y.
• If starttime(z) and endtime(z) are the timestamps when z is created and destroyed, then
  • x outlives y: (starttime(x) <= starttime(y)) ∧ (endtime(x) >= endtime(y)).
  • x strictly outlives y: (starttime(x) <= starttime(y)) ∧ (endtime(x) > endtime(y)).
• x (strictly) outlives y: [starttime(x), endtime(x)] contains [starttime(y), endtime(y)].

Rules

1. References are never null
2. To make sure the references with the lifetime 'a in a struct T, defined by struct T<'a>, are never null(rule 1), the lifetime 'a must cover the lifetime of the struct T variable. That is, the references with lifetime 'a in T outlive the variable with struct T in an inclusive manner, and therefore we can make sure the references with lifetime 'a in T must be alive when T variable is alive.
3. it's natural that a variable outlives the references to it(The referents outlive references). For example, the variable with type T referred by r outlives the reference r with lifetime 'a (without impl Drop for T), where 'r is defined by r: &'a T. For example, the x must live at least as long as 'a in the code Struct T {..} Struct S<'a> { r: &'a T } let x: T = ...; let s = S { r: &x };.
4. By Drop Check, the presence of Drop for T will force that struct T variable strictly outlives any reference to the struct T variable. That is, r: &'a mut T with impl Drop for T requires the variable referred by r strictly outlives the reference r. For example, the x must live longer than 'a in the code Struct T {..} impl Drop for T {..} Struct S<'a> { r: &'a T } let x: T = ...; let s = S { r: &x };.

Syntax

• Lifetime Subtyping: 'a: 'b means the references with 'a outlives the references with 'b. That is, lifetime 'a that lives at least as long as 'b, or 'a

Discussion

1. Will the lifetime 'a be different for a reference with &'a T and a reference with &'a mut T ?
   • No ?
2. What is the relationship of 'a, 'b, and lifetime(x) within code Struct S<'a, 'b> { r: &'a T<'b> }; let x: T = ...; let s = S { r: &x } ?
   • By rule 2: T<'b> implies 'b outlives the variable x
   • Without implementing Drop for T, by rule 3: &'a T implies x outlives a
     • 'b outlives x and x outlives a
   • With implementing Drop for T, by rule 4: &'a T implies x strictly outlives a
     • 'b outlives x and x strictly outlives a
   • Thus, in any case, 'b must outlive 'a. We should add 'b: 'a in Struct S: Struct S<'a, 'b: 'a> { r: &'a T<'b> };.

none_1.rs

fn main() {
    let foo = Foo::new(); // What is the lifetime 'a here ?
}

struct Foo<'a> {
    ref_opt: Option<&'a i32>,
}

impl<'a> Foo<'a> {
    fn new() -> Self {
        Foo { ref_opt: None }
    }
}

// Is it right ? 'a exists even ref_opt is None.
// fn main() {
//     'a: {
//         let foo = Foo::new();
//     }
// }

none_2.rs

fn main() {
    let foo = Foo::new();       // What is the lifetime 'a here ?
    let bar = Bar::new(&foo);   // What are the lifetimes 'x, 'y here ?
}

struct Foo<'a> {
    ref_opt: Option<&'a i32>,
}

impl<'a> Foo<'a> {
    fn new() -> Self {
        Foo { ref_opt: None }
    }
}

struct Bar<'x, 'y: 'x> {
    ref_foo: &'x Foo<'y>,
}

impl<'x, 'y> Bar<'x, 'y> {
    fn new(foo: &'x Foo<'y>) -> Self {
        Bar { ref_foo: foo }
    }
}

// Is it right ?
// fn main() {
//     'a: {
//         let foo = Foo::new();
//         'b: { // 'x is 'b = 'x, 'y is 'a
//             let bar = Bar::new(&foo);
//         }
//     }
// }

notation.md

Notation

⊇ and ⊃

When x and y are referred as the two different ranges, x ⊇ y and x ⊃ y are defined as

• x ⊇ y: The range of x is larger than or equal to y
• x ⊃ y: The range of x is larger than y

x ⊇ y

|
+---+- y ---+- x
|   |       |
|   |       |
+---+-------+
|
v
Value

|
+---+-- y --+- x
|   |       |
|   |       |
+---+       |
|           |
+-----------+
|
v
Value

|
+-----------+- x
|           |
+---+- y    |
|   |       |
|   |       |
+---+-------+
|
v
Value

|
+-----------+- x
|           |
+---+- y    |
|   |       |
|   |       |
+---+       |
|           |
+-----------+
|
v
Value

x ⊃ y

|
+---+- y ---+ x
|   |       |
|   |       |
+---+       |
|           |
+-----------+
|
v
Value

|
+-----------+- x
|           |
+---+- y    |
|   |       |
|   |       |
+---+-------+
|
v
Value

|
+-----------+- x
|           |
+---+- y    |
|   |       |
|   |       |
+---+       |
|           |
+-----------+
|
v
Value

Outlive and Strictly Outlive

• a outlives b: a is alive when b is alive but a and b can be destroyed at the same time. That is, a must live at least as long as b.
• a strictly outlives b: a is alive when b is alive and a must be alive when b is destroyed. That is, a lives longer than b.
• If starttime(c) and endtime(c) are the timestamps when c is created and destroyed, then
  • a outlives b: (starttime(a) <= starttime(b)) ∧ (endtime(a) >= endtime(b)).
  • a strictly outlives b: (starttime(a) <= starttime(b)) ∧ (endtime(a) > endtime(b)).

When 'a and 'b are referred as the lifetimes of two different variables a and b , where the lifetimes(c) is the range from starttime(c) to endtime(c) (both values are included) , denoted by: [starttime(c), endtime(c)] , the meanings of "a outlives b" and "a strictly outlives b" can be represented by the following figures with the definitions:

• 'a = lifetime(a) = [starttime(a), endtime(a)]
• 'b = lifetime(b) = [starttime(b), endtime(b)]

a outlives b

|
+---+- 'b --+- 'a
|   |       |
|   |       |
+---+-------+
|
v
Time

• starttime(a) = starttime(b)
• endtime(a) = endtime(b)

|
+---+- 'b --+- 'a
|   |       |
|   |       |
+---+       |
|           |
+-----------+
|
v
Time

• starttime(a) = starttime(b)
• endtime(a) > endtime(b)

|
+-----------+- 'a
|           |
+---+- 'b   |
|   |       |
|   |       |
+---+-------+
|
v
Time

• starttime(a) < starttime(b)
• endtime(a) = endtime(b)

|
+-----------+- 'a
|           |
+---+- 'b   |
|   |       |
|   |       |
+---+       |
|           |
+-----------+
|
v
Time

• starttime(a) < starttime(b)
• endtime(a) > endtime(b)

Thus, a outlives b can be represented as 'a ⊇ 'b. That is, lifetime(a) ⊇ lifetime(b).

a strictly outlives b

|
+---+- 'b --+- 'a
|   |       |
|   |       |
+---+       |
|           |
+-----------+
|
v
Time

• starttime(a) = starttime(b)
• endtime(a) > endtime(b)

|
+-----------+- 'a
|           |
+---+- 'b   |
|   |       |
|   |       |
+---+       |
|           |
+-----------+
|
v
Time

• starttime(a) < starttime(b)
• endtime(a) > endtime(b)

Thus, a strictly outlives b can be represented as ('a ⊃ 'b) ∧ (end of 'a > end of 'b). That is, (lifetime(a) ⊃ lifetime(b)) ∧ (endtime(a) > endtime(b)).

todo.md

• Read Ownership and Lifetimes
• Check if the meanings of outlive and strictly outlive are correct or not
• Use notations to denote the lifetime relationships
• Derive the following relationships:
  • a outlives b and b outlives c: a outlives c, if my assumption for outlives are right
  • a outlives b and b strictly outlives c: a strictly outlives c, if my assumption for outlives are right
  • a strictly outlives b and b outlives c: a strictly outlives c, if my assumption for outlives are right
  • a strictly outlives b and b strictly outlives c: a strictly outlives c, if my assumption for outlives are right