@@ -309,7 +309,7 @@ Sometimes, we have a reference to one type but need a reference to another, simi
Generally, there are many types that can act as a substitute for another. The common interface for this behavior is the \inline{AsRef} trait. There can be many implementations of this trait for a given type. for example, \inline{String} can stand in for \inline{str}, \inline{[u8]}, \inline{OsStr} and \inline{Path}. Every time a reference to one of these types are needed, we can use a \inline{String} instead, if we first call \inline{as_ref} on it:
\begin{lstlisting}[language=Rust, caption={Use \inline{String} in place of \inline{[u8]}}, label={lst:as_ref_bytes}]
\begin{lstlisting}[language=Rust, caption={Use \inline{String}and \inline{as_ref}in place of \inline{[u8]}}, label={lst:as_ref_bytes}]
fn needs_bytes(x: &[u8]) { /*...*/ }
// ...
...
...
@@ -343,7 +343,7 @@ All three of the aforementioned traits work for shared references only, but thei
In \autoref{lst:lexical-lifetimes} we saw how lexical lifetimes stood in our way and we had to manually wrap a reference in an additional block just to make our correct program pass the borrow checker. This was because the lifetime of any value is bound to its scope, at the end of which it is dropped. \acl{NLL}is a different approach to lifetime analysis. A reference is live for as long as it may be used later. The borrow checker determines the points of the program in which the reference is live by building a \acfi{CFG}. All nodes of the \ac{CFG} that can be reached from the point of creation until the last use of the reference are where it is live. Consider the program in \autoref{lst:non-lexical-lifetimes}.
In \autoref{lst:lexical-lifetimes} we saw how lexical lifetimes stood in our way and we had to manually wrap a reference in an additional block just to make our correct program pass the borrow checker. This was because the lifetime of any value is bound to its scope, at the end of which it is dropped. \acl{NLL}are a different approach to lifetime analysis. A reference is live for as long as it may be used later. The borrow checker determines the points of the program in which the reference is live by building a \acfi{CFG}. All nodes of the \ac{CFG} that can be reached from the point of creation until the last use of the reference are where it is live. Consider the program in \autoref{lst:non-lexical-lifetimes}.
@@ -472,13 +472,104 @@ Right now, two-phase borrowing works only for method calls where the first argum
\todo[inline]{Excurse on multi-phase borrowing}
\subsection{Loans and Regions}
Previously, we looked at the advantages of \acl{NLL} over lexical lifetimes. But lifetimes have a general defect and are supposed to be replaced by an approach using \emph{regions} using the \emph{Polonius borrow checker}, which is currently in an experimental stage. Here, we will explore how \ac{NLL} and regions work under the hood, and what the advantage of using regions is.
\subsubsection{Borrow Errors}
A borrow error needs three things: A statement accessing a path, accessing the path violating some loan, and the loan being live at this point.
What is a loan, what is a path, what is liveness of a loan?
\subsubsection{Classic \ac{NLL}}
When creating a reference, it is live at some points. A loan is live if its reference is. Some references outlive others, this leads to a subtyping relationship.
\subsubsection{Polonious}
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.
\subsubsection{Structure of the Talk by \href{https://www.youtube.com/watch?v=_agDeiWek8w}{Niko Matsakis}}
\begin{enumerate}
\item What are loans and regions?
\item regions as an alternative to lifetimes
\item regions are more powerful
\item Piggyback on the talk by \href{https://www.youtube.com/watch?v=_agDeiWek8w}{Niko Matsakis}
\item Note: Polonius will be a new borrow checker using regions but it is unstable
\item Note: concrete memory regions à la Cyclone vs abstract regions à la Polonius
\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 A \emph{path} is a local variable on the stack, \inline{x}, a field of a path \inline{x.f}, a dereference \inline{*x}, or an index \inline{x[_]} (the index itself is not interesting to us; indexing accesses the whole of \inline{x}).
\item A \emph{loan} is the result of a borrow expression \inline{&x}: a path (here \inline{x}) and a \emph{mode} (shared or unique).
\item Borrow checking before 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:
\begin{lstlisting}[language=Rust]
/* 0 */ let mut x : u32 = 22;
/* 1 */ let y : &{2, 3} u32 = &{2, 3} 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]
}
}
}
\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 a unique 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}
When creating a \inline{Message}, Polonius can check that the origin of \inline{'buffer} is within the struct.
\end{enumerate}
\section{Contracts and Refinement Types}
...
...
@@ -548,4 +639,4 @@ Right now, two-phase borrowing works only for method calls where the first argum
