Campus Event Calendar
Event Entry
What and Who
Understanding and Evolving the Rust Programming Language
Ralf Jung
MMCI
SWS Student Defense Talks - Thesis Defense
SWS
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 21 August 2020
11:00
60 Minutes
E1 5
021
Saarbrücken
Abstract
Rust is a young systems programming language that aims to fill the gap between high-level languages with strong safety guarantees and low-level languages that give up on safety in exchange for more control.
Rust promises to achieve memory and thread safety while at the same time giving the programmer control over data layout and memory management. This dissertation presents two projects establishing the first formal foundations for Rust, enabling us to better understand and evolve this language:
RustBelt and Stacked~Borrows.
RustBelt is a formal model of Rust's type system, together with a soundness proof establishing memory and thread safety. The model is also able to verify some intricate APIs from the Rust standard library that internally encapsulate the use of unsafe language features.
Stacked Borrows is a proposed extension of the Rust specification which enables the compiler to use Rust types to better analyze and optimize the code it is compiling. The adequacy of this specification is not only evaluated formally, but also by running real Rust code in an instrumented version of Rust's Miri interpreter that implements the Stacked Borrows semantics. RustBelt is built on top of Iris, a language-agnostic framework for building higher-order concurrent separation logics.
This dissertation gives an introduction to Iris and explains how to build complex high-level reasoning principles from a few simple ingredients. In RustBelt, this technique is used to introduce the lifetime logic, a separation logic account of borrowing, which plays a key role in the Rust type system.
Rust promises to achieve memory and thread safety while at the same time giving the programmer control over data layout and memory management. This dissertation presents two projects establishing the first formal foundations for Rust, enabling us to better understand and evolve this language:
RustBelt and Stacked~Borrows.
RustBelt is a formal model of Rust's type system, together with a soundness proof establishing memory and thread safety. The model is also able to verify some intricate APIs from the Rust standard library that internally encapsulate the use of unsafe language features.
Stacked Borrows is a proposed extension of the Rust specification which enables the compiler to use Rust types to better analyze and optimize the code it is compiling. The adequacy of this specification is not only evaluated formally, but also by running real Rust code in an instrumented version of Rust's Miri interpreter that implements the Stacked Borrows semantics. RustBelt is built on top of Iris, a language-agnostic framework for building higher-order concurrent separation logics.
This dissertation gives an introduction to Iris and explains how to build complex high-level reasoning principles from a few simple ingredients. In RustBelt, this technique is used to introduce the lifetime logic, a separation logic account of borrowing, which plays a key role in the Rust type system.
Contact
--email hidden
Video Broadcast
Yes
SWS Space 2 (6312)
passcode not visible
logged in users only
Maria-Louise Albrecht, 08/15/2020 13:35
Maria-Louise Albrecht, 08/15/2020 13:34 -- Created document.
Maria-Louise Albrecht, 08/15/2020 13:34 -- Created document.