RustLog

Deep dive into the Polonius model checker

by H. Haldi and M. Algelly

Report of the 4th of April 2021

What did we do?

Understand

  • Loan, path, lifetime, statement
  • The borrow checker error rule

Problems encountered

  • Liveness of variables
  • Lifetime of variables (e.g. ‘a)
  • How NLL and Polonius are different

Liveness of variables

let mut x = 5;
let y = &mut x;
// here y is no longer alive

println!("x: {}", x);
// x: 5

let mut x = 5;
let y = &mut x;

println!("x: {}", x);
*y = 4; // <-- here y is used, so it is still alive
// does not compile
// x is already borrowed as mutable

Lifetime of variables

let r;
{
    let x = 5;
    r = &x;
}

println!("r: {}" , r);

// error[E0597]: `x` does not live long enough
// r = &x;
//     ^^ borrowed value does not live long enough

The borrow checker

What is a Path ?

A path P is an expression that leads to a memory location.

e.g. x, x.f, *x.f, (*x.f)[_]

What is a Loan

A loan is a name for a borrow expression, e.g. &x.

Associated with a path and a mode (shared or mutable).

Borrow check error

Error occurs at statement N if:

  • N accesses path P
  • Accessing P violates a loan L
  • L is live at N

Example

let mut x: u32 = 22; // path P
let y: &u32 = &x; // loan L shares `x`
x += 1; // statement N accesses path `x`, violating L
print(y) // L is live

How does current Rust works

/*0*/ let mut x: u32 = 22;
/*1*/ let y: &{2, 3} u32 = &{2, 3} x;
/*2*/ x += 1;
/*3*/ print(y);
  • The statement at line 2 modifies the path x, so violates the terms of &x loan from line 1
  • Loan from line 1 is live on lines 2 because it is used on line 3

=> ERROR

/*0*/ let mut x: u32 = 22;
/*1*/ let y: &{L1} u32 = &{L1} x /* Loan L1 */;
/*2*/ x += 1;
/*3*/ print(y);
  • x has origin L1
  • y has the same origin L1
  • line 2 modifies the path x, so violates the terms of the loan L1
  • y is live on line 2 and its type includes L1
    • type of y is &{L1} u32

=> ERROR

Conclusion

  • Learned some vocabulary
  • Difference between NLL and Polonius
  • Formally defined the borrow checker error rule

What’s next?

  • Show precise example where Polonius is better than NLL