From: Ralf Jung Date: Tue, 1 Sep 2020 09:31:31 +0000 (+0200) Subject: add my PhD thesis X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/3fb92c77d312e17e83a50598bbda29dd890ce3d8 add my PhD thesis --- diff --git a/research/_config.yml b/research/_config.yml index 67fc2a8..4c1f1f9 100644 --- a/research/_config.yml +++ b/research/_config.yml @@ -11,7 +11,7 @@ defaults: # Build settings markdown: kramdown -exclude: ['*.sh', 'thesis.html'] +exclude: ['*.sh'] # Custom settings mpi_sws_imprint: True diff --git a/research/phd/thesis-print.pdf b/research/phd/thesis-print.pdf new file mode 100644 index 0000000..7024a5e Binary files /dev/null and b/research/phd/thesis-print.pdf differ diff --git a/research/phd/thesis-screen.pdf b/research/phd/thesis-screen.pdf new file mode 100644 index 0000000..d573631 Binary files /dev/null and b/research/phd/thesis-screen.pdf differ diff --git a/research/thesis.html b/research/thesis.html index 2510b23..29ca075 100644 --- a/research/thesis.html +++ b/research/thesis.html @@ -3,4 +3,17 @@ title: Understanding and Evolving the Rust Programming Language slug: Thesis --- -This is where my PhD thesis will be made available. +

Rust is a young systems programming language that aims to fill the gap between high-level languages—which provide strong static guarantees like memory and thread safety—and low-level languages—which give the programmer fine-grained 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 important 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 designed to verify the safety of a number of intricate APIs from the Rust standard library, despite the fact that the implementations of these APIs use unsafe language features.

+ +

Stacked Borrows is a proposed extension of the Rust specification, which enables the compiler to use the strong aliasing information in Rust’s types to better analyze and optimize the code it is compiling. The adequacy of this specification is evaluated not only 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, implemented in the Coq proof assistant, for building higher-order concurrent separation logics. This dissertation begins by giving an introduction to Iris, and explaining how Iris enables the derivation of complex high-level reasoning principles from a few simple ingredients. In RustBelt, this technique is exploited crucially to introduce the lifetime logic, which provides a novel separation-logic account of borrowing, a key distinguishing feature of the Rust type system.

+ +

Download

+ +