Start 1.1.6 polonius

thesis/1-introduction.tex

@@ -507,29 +507,36 @@ Different approaches to borrow checking only differ in determining when $L$ is l
 
 \subsubsection{Classic \ac{NLL}}
 
-Under \ac{NLL} the liveness of a loan is derived from the lifetime of a reference. As discussed in \autoref{subsec:non-lexical-lifetimes}, a reference is live in a node of the \ac{CFG} if it may be used later. The corresponding loan is live exactly when the reference is live. \todo{lifetime subtyping and inferred lifetimes/constraints} Crucially, if a function returns a reference, it is live for the whole body of the function. \autoref{lst:nll-reject-correct} shows an example. In the \inline{Some} branch, the reference returned by \inline{v.first()} is in turn returned from the function, meaning it must be live at least until the end of the function body. But in the \inline{None} branch, an exclusive reference is needed to push a value to the vector. This should not be a problem since the shared reference from \inline{v.first()} is not used in this branch, and a different reference is returned from the function instead. However, \ac{NLL} can’t accomodate this situation because it \emph{may} be used later, see \autoref{fig:cfg-nll-reject-correct}.\todo{Is this correct? I think maybe the problem lies with \inline{x}. But the borrow checker is not angry about it.}
+Under \ac{NLL} the liveness of a loan is derived from the lifetime of a reference. As discussed in \autoref{subsec:non-lexical-lifetimes}, a reference is live in a node of the \ac{CFG} if it may be used later. The corresponding loan is then simply live exactly when the reference is live. \todo{lifetime subtyping and inferred lifetimes/constraints, “outlive” relationship, \inline{'a : 'b}} Crucially, if a function returns a reference, it is live for the whole body of the function.
 
 \begin{lstlisting}[language=Rust, caption={\ac{NLL} reject correct program}, label={lst:nll-reject-correct}]
 fn first_or_insert(v: &mut Vec<i32>) -> &i32 {
-    match v.first() {
+    let fst = v.first();
+    match fst {
         Some(x) => x,
         None => {v.push(1); &v[0]},
     }
 }
 \end{lstlisting}
 
+\autoref{lst:nll-reject-correct} shows an example. In the \inline{Some} branch, \inline{x} is returned from the function, which in turn depends on the reference produced by \inline{fst}. Because \inline{x} is returned from the function, it needs to be live at least until the end of the body of \inline{first_or_insert}. But since \inline{x} is derived from \inline{fst}, that reference must outlive \inline{x}, hence being live for the whole function body as well. In the \inline{None} branch, an exclusive reference to \inline{v} is created for the call to \inline{push}. This produces an error because that node lies on a path between the creation of \inline{fst} and the return point.
+
+This should not happen. We can see that \inline{fst} is not actually used when we go through the \inline{None} arm because a different reference is returned in that case. However, \ac{NLL} can’t accomodate this situation because \inline{fst} \emph{may} be used later, see \autoref{fig:cfg-nll-reject-correct}.
+
 \begin{figure}[!ht]
     \centering
     \begin{tikzpicture}
         \begin{scope}[every node/.style={draw, rectangle}]
-            \node[ultra thick] (A) at (0,5) {\inline{match v.first()}};
+            \node[ultra thick] (Z) at (0,7.5) {\inline{let fst = v.first();}};
+            \node[ultra thick] (A) at (0,5) {\inline{match fst}};
             \node[ultra thick] (B) at (-1,2.75) {\inline{x}};
             \node[ultra thick, draw=red] (C) at (1,3.5) {\inline{v.push(1);}};
             \node[ultra thick] (D) at (1,2) {\inline{&v[0]}};
             \node[ultra thick] (E) at (0,0.5) {\inline{return}};
         \end{scope}
-        \path [->, ultra thick] (A) edge node[left] {} (B);
-        \path [->, ultra thick] (A) edge node[left] {} (C);
+        \path [->, ultra thick] (Z) edge node[left] {} (A);
+        \path [->, ultra thick] (A) edge node[left] {\inline{Some}} (B);
+        \path [->, ultra thick] (A) edge node[right] {\inline{None}} (C);
         \path [->, ultra thick] (C) edge node[left] {} (D);
         \path [->, ultra thick] (B) edge node[left] {} (E);
         \path [->, ultra thick] (D) edge node[left] {} (E);
@@ -540,6 +547,8 @@ fn first_or_insert(v: &mut Vec<i32>) -> &i32 {
 
 \subsubsection{Polonious}
 
+With lifetimes, we looked \emph{forwards} from the borrow expression to see how long a reference (and therefore the loan) are live. Polonius goes \emph{backwards} from a point of use to see if there is still a live reference. Polonius doesn’t use lifetimes but \emph{regions} to determine the liveness of a loan. A region\footnote{Polonius calls regions \emph{origins}, which is a more telling name, but regions is the more standard term.} is a set of loans.
+
 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.
 
 \todo[inline]{Write up nicely the stuff below}