research/thesis.html

   1 ---
   2 title: Understanding and Evolving the Rust Programming Language
   3 slug: Thesis
   4 ---
   5
   6 <i>PhD Thesis, Defended in August 2020</i>
   7
   8
   9 <h3>Abstract</h3>
  10
  11 <p><em>Rust</em> is a young systems programming language that aims to fill the gap between <em>high-level languages</em>—which provide strong static guarantees like memory and thread safety—and <em>low-level languages</em>—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 <em>understand</em> and <em>evolve</em> this important language: <em>RustBelt</em> and <em>Stacked Borrows</em>.</p>
  12
  13 <p><em>RustBelt</em> 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 <em>unsafe</em> language features.</p>
  14
  15 <p><em>Stacked Borrows</em> 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 <em>Miri</em> interpreter that implements the Stacked Borrows semantics.</p>
  16
  17 <p>RustBelt is built on top of <em>Iris</em>, 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 <em>lifetime logic</em>, which provides a novel separation-logic account of <em>borrowing</em>, a key distinguishing feature of the Rust type system.</p>
  18
  19 <p style="font-weight:bold">
  20 This thesis has received an <a href="https://awards.acm.org/about/2020-doctoral-dissertation" style="font-weight:bold;">Honorable Mention for the ACM Doctoral Dissertation Award</a>,
  21 the <a href="https://sigplan.org/Awards/Dissertation/#2021_Ralf_Jung__Max_Planck_Institute_for_Software_Systems_and_Saarland_University" style="font-weight:bold;">ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award</a> (as one of two recipients),
  22 an <a href="https://www.mpg.de/prizes/otto-hahn-medal" style="font-weight:bold;">Otto Hahn Medal</a>,
  23 the <a href="https://etaps.org/2021/doctoral-dissertation-award" style="font-weight:bold;">ETAPS Doctoral Dissertation Award</a>,
  24 and the Saarland University <a href="https://www.uni-saarland.de/universitaet/aktuell/news/artikel/nr/24072.html" style="font-weight:bold;">Dr. Eduard Martin-Preis</a>.
  25 </p>
  26
  27 <h3>Download and references</h3>
  28
  29 <ul>
  30 <li><a href="phd/thesis-screen.pdf">Screen-optimized version (PDF)</a> (updated 2020-12-08)</li>
  31 <li><a href="phd/thesis-print.pdf">Print-optimized version (PDF)</a> (official final version)</li>
  32 <li>DOI: <a href="http://dx.doi.org/10.22028/D291-31946">10.22028/D291-31946</a></li>
  33 </ul>