Aliasing Models for Rust

The Rust programming language is getting increasingly popular in systems programming, becoming the second ever high-level language accepted into Linux beside C.
This is in no small part due to Rust's memory safe references preventing many bugs already at compile time.
However, low-level programming also requires using unsafe features like raw pointers, whose memory safety cannot be checked by the compiler.
The interaction between safe and unsafe Rust has many subtle difficulties and is an area of ongoing research.

This talk provides an introduction to memory safety in Rust, explaining the fundamentals of the Borrow Checker and the challenges of interacting with unsafe code.
It then gives an overview of Stacked Borrows (Jung et al., 2020), a proposed formal model defining clear semantics for both raw pointers and references.
Practical guidelines are derived for systems programmers working with unsafe Rust.

No previous knowledge of Rust is required.

(Advanced Seminar)