Skip to content
Snippets Groups Projects
Commit 99a4aec0 authored by Jasper Clemens Gräflich's avatar Jasper Clemens Gräflich
Browse files

Restructure 1.1.6 outline

parent 193e0e17
No related branches found
No related tags found
No related merge requests found
Pipeline #86569 passed
......@@ -532,7 +532,7 @@ fn first_or_insert(v: &mut Vec<i32>) -> &i32 {
% \path [->, ultra thick] (B) edge node[left] {} (C);
% \path [->] (C) edge node[left] {} (D);
\end{tikzpicture}
\caption{Control-flow diagram for \autoref{lst:nll-reject-correct}}
\caption{Control-flow diagram for \autoref{lst:nll-reject-correct}, nodes in which the reference returned by \inline{v.first()} is live are marked with a thick border.}
\label{fig:cfg-nll-reject-correct}
\end{figure}
......@@ -540,89 +540,56 @@ fn first_or_insert(v: &mut Vec<i32>) -> &i32 {
When creating a reference, it gets an associated \emph{region} (\emph{origin} in Polonius), which is part of its type. (What is a region?) A loan is live if some live variable has it in its type.
What cool things are possible now?
\subsubsection{Polonius the Crab}
A Rust library emulating Polonius by using a safe abstraction around raw pointers.(?)
\subsubsection{Cyclone}
Cyclone is a C dialect with region based memory. It uses concrete memory regions whereas Polonius uses abstract ones.
\todo[inline]{flesh out subsection with help of the below}
\subsubsection{Structure of the Talk by \href{https://www.youtube.com/watch?v=_agDeiWek8w}{Niko Matsakis}}
\begin{enumerate}
\item Throughout, Niko uses this example:
\begin{lstlisting}[language=Rust]
/* 0 */ let mut x : u32 = 22;
/* 1 */ let y : &'0 u32 = &'1 x;
/* 2 */ x += 1;
/* 3 */ print(y);
\end{lstlisting}
\item What exactly is a borrow error? The following conditions must be met:
\begin{enumerate}
\item statement $N$ accesses path $P$
\item accessing $P$ would violate the terms of some loan $L$. For shared loans: modifying $P$, for mutable loans: accessing $P$.
\item Note that e. g. mutating a field of a loaned struct is still forbidden; this is an \emph{indirect} mutation.
\item The loan must be live at $N$ (it, or some derived reference, might be used later)
\end{enumerate}
\item Borrow checking before Polonius:
\item Borrow checking in Polonius:
\begin{enumerate}
\item compute lifetimes of references: the part (set of nodes in the control-flow graph; we use lines as a simplification) of the program where the references might be used
\item Every reference has a fresh inference variable (variable in the algebraic sense), and the compiler has to figure out which set they correspond to.
\item For example \inline{y} has the lifetime \inline{'0} associated with it. Since \inline{y} is live on lines 2 and 3, $'0$ must include them. Therefore $'0 = \{2, 3\}$. $'1$ must outlive $'0$, therefore $'1 = \{2, 3\}$. We receive:
\item Instead of tracking where a reference $R$ might be used, we track where it comes from, its \emph{origin}. The origin of $R$ is a set of loans $R$ might have come from (so we go backwards).
\item $'1$ has the origin $\{L1\}$, it is a singleton since it is a freshly created reference. $'0$ also has origin $\{L1\}$, since there is only one assignment to \inline{y}. We have:
\begin{lstlisting}[language=Rust]
/* 0 */ let mut x : u32 = 22;
/* 1 */ let y : &{2, 3} u32 = &{2, 3} x;
/* 1 */ let y : &{L1} u32 = &{L1} x;
/* 2 */ x += 1;
/* 3 */ print(y);
\end{lstlisting}
\item A loan is then simply live during the lifetime of that reference.
\item So, in our example: The statement on line 2 accesses path \inline{x}, which violates the loan $L$ \inline{(x, shared, {2, 3})} from line 1, and $L$ is live at this point. Therefore, we have an error.
\end{enumerate}
\item Borrow checking in Polonius:
\begin{enumerate}
\item Instead of tracking where a reference $R$ might be used, we track where it comes from, its \emph{origin}. The origin of $R$ is a set of loans $R$ might have come from (so we go backwards).
\item $'1$ has the origin $\{L1\}$, it is a singleton since it is a freshly created reference. $'0$ also has origin $\{L1\}$, since there is only one assignment to \inline{y}. We have:
\begin{lstlisting}[language=Rust]
/* 0 */ let mut x : u32 = 22;
/* 1 */ let y : &{L1} u32 = &{L1} x;
/* 2 */ x += 1;
/* 3 */ print(y);
\end{lstlisting}
\item Liveness is not relevant here, only flow of values. Only the liveness of variables are important.
\item Now, a loan $L$ is live if some live variable has $L$ in its type.
\item So, in our example: Line 2 modifies \inline{x}, violating the loan \inline{(x, shared)}. \inline{y} is live at this point and contains the loan \inline{(x, shared)}. Therefore, we have an error.
\end{enumerate}
\item Why does it matter?
\begin{lstlisting}[language=Rust]
fn get_or_insert(
map: &mut HashMap<u32, String>
) -> &String {
match map.get(&22) {
Some(v) => v,
None => {
map.insert(22, String::from("hi"));
&map[%22]
fn get_or_insert(
map: &mut HashMap<u32, String>
) -> &String {
match map.get(&22) {
Some(v) => v,
None => {
map.insert(22, String::from("hi"));
&map[%22]
}
}
}
}
\end{lstlisting}
\end{lstlisting}
Here (with classical NLL), \inline{v} lives longer than the function, meaning that the loan is live for the whole function call. In particular, it is live when we try to insert, which is a violation (since we need an exclusive reference here)
With Polonius, \inline{v} is not live in the \inline{None} branch and therefore no violation happens because there are no live variables with that loan in their type.
\item Polonius can also help with self-referential structs:
\begin{lstlisting}[language=Rust]
struct Message {
buffer : Vec<String>,
slice: &'buffer [u8], // borrow from field `buffer`
}
\end{lstlisting}
struct Message {
buffer : Vec<String>,
slice: &'buffer [u8], // borrow from field `buffer`
}
\end{lstlisting}
When creating a \inline{Message}, Polonius can check that the origin of \inline{'buffer} is within the struct.
\end{enumerate}
\subsubsection{Polonius the Crab}
\todo[inline]{A Rust library emulating Polonius by using a safe abstraction around raw pointers.(?)}
\subsubsection{Cyclone}
\todo[inline]{Cyclone is a C dialect with region based memory. It uses concrete memory regions whereas Polonius uses abstract ones.}
\section{Contracts and Refinement Types}
\subsection{Contracts}
\begin{enumerate}
......
No preview for this file type
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment