010_introduction.tex

\section{Introduction}\label{sec:introduction}

The Rust programming language is seeing widespread use in areas such
as system programming~\cite{ABGMMMS16,BBBPRR17,LCGPDL17}, blockchain
systems~\cite{HHHH18,NQ20}, smart contracts~\cite{Ash20,ZHCKHJJMS20}
and more~\cite{BHR18,AMPS19}.  A key feature of Rust is its ability to
automatically deallocate dynamically allocated data when it goes out
of scope. This differs from most other programming languages, that
either: require programmers free data structures explicitly
(e.g. C/C++); or, rely on garbage collection to free unreachable data
(e.g. Java, C\#, etc).  The former approach is error prone
(e.g. use-after-free or free-after-free errors), whilst the latter is
safe but costly (garbage collection consumes resources and data may
not be released in a timely fashion).

In Rust, each data structure is \emph{owned} by a
variable~\cite{RustBook}. Once that variable goes out of scope, the
data is freed as well.  Rust also allows data to be lent temporarily
(e.g. as a function parameter) using {\em borrows}, which can be seen
as pointers in traditional programming languages (but without
ownership).  Since borrows are access paths into data structures, the
type checker of Rust must enforce strict rules on their creation and
lifetime.  For example, a location cannot be mutated as long as a
borrow to it exists.  To support this, data is divided into two
categories: that which can be {\em copied} (e.g. primitives); and that
which must be {\em moved} (e.g. mutable borrows).  For the latter,
assignments result in a transfer of ownership from rightvalue to
leftvalue.  The Rust compiler performs \emph{borrow checking} to
statically check that borrows are used safely (i.e. that automatic
deallocation does not create dangling pointers, that multithreaded
code does not generate race conditions, etc).

Featherweight Rust (\FR/) formalises a subset of Rust and includes a
proof of correctness for borrow checking~\cite{Pea21}.  In particular,
borrow checking is formalised as a flow-sensitive type system, whose
types include primitives (such as \<int>), dynamically allocated data
structures (collectively represented by a boxing operator) and borrows
of leftvalues, both for {\em reading} (immutable borrows) and {\em
  writing} (mutable borrows). The type system rules are given by
structural induction on the syntax of the Rust source code, and are
hence well-founded. However, they use, internally, a procedure to type
leftvalues. Since borrows include other leftvalues, we have discovered
this procedure may enter an infinite loop and, in such case, the
borrow checker would not terminate either.

\paragraph{Contribution.}

This paper provides a sufficient condition which ensures the borrow
checker for Featherweight Rust terminates~\cite{Pea21}.  Our insight
is that, for well-typed programs, this condition already holds for
typing environments created during borrow checking.  Hence, this is
not a bug in Featherweight Rust {\em per se}, but rather an important
condition which was left implicit.  Our approach shows that data
structures are \emph{linearizable} at run time and, hence, that our
condition holds for the specific kind of type environments the borrow
checker builds during execution.  This result is important in order to
increase confidence in the borrow checker of Rust.  Moreover, it
provides a notion of well-foundness for the recursion used in the
borrow checker, that future work can exploit in order to prove other
properties by induction.  For example, this is a necessary step
towards a mechanical proof of Featherweight Rust.