RustLog

A first preview of the Rust borrow checker

by H. Haldi and M. Algelly

Report of the 7th of March 2023

What did we do?

Understand

  • Rust Syntax
  • Ownership in Rust
  • The borrow checker
  • Limitations of the borrow checker
  • How to improve it with Polonius

Problems encountered

  • Reference vs copy vs move
  • shared vs mutable
  • Liveness of variables
  • Lifetime of variables (e.g. ‘a)

Reference vs copy vs move

Reference vs copy vs move (cont.)

let x = 5;
let mut y = x;

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

Reference vs copy vs move (cont.)

let s = String::from("hello");
let t = s;

println!("s: {}, t: {}", s, t);
// does not compile
// println!("s: {}, t: {}", s, t);
//                          ^ value borrowed here after move

Reference vs copy vs move (cont.)

fn takes_ownership(s: String) {
    println!("s: {}", s);
}

fn main() {
    let s = String::from("hello");
    takes_ownership(s);
    println!("s: {}", s);
    // does not compile
    // println!("s: {}", s);
    //                   ^ value borrowed here after move
}

Reference vs copy vs move (cont.)

let s = String::from("hello");
let t = &s;

println!("s: {:p}, t: {:p}", &s, t);
// s: 0x7fff7e26fc50, t: 0x7fff7e26fc50

Shared vs mutable

Shared vs mutable (cont.)

let x = 5;
let y = &x;
let z = &x;

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

Shared vs mutable (cont.)

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

println!("x: {}, y: {}", x, y);

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;
// 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);

/*0*/ let mut x: u32 = 22;
/*1*/ let y: &{L1} u32 = &{L1} x /* Loan L1 */;
/*2*/ x += 1;
/*3*/ print(y);

Conclusion

  • Good understanding of Rust and its borrow checker
  • What are the limitations of the current borrow checker
  • How to improve it with Polonius

What’s next?

gantt