diff --git a/use-based-refs/use-based-refs.pdf b/use-based-refs/use-based-refs.pdf index db25cf6d2c32e69f93f07de95bf24e08b8ecc71c..fa12378f51bbb3c5b25965b51f505bc790e66aa3 100644 --- a/use-based-refs/use-based-refs.pdf +++ b/use-based-refs/use-based-refs.pdf @@ -1,3 +1,3 @@ version https://git-lfs.github.com/spec/v1 -oid sha256:b46647f538ab1fd4a27ed5bf54da16d1c191a901cf8395a838a0f88a4b2ccf8e -size 199524 +oid sha256:d820c6621f77b3474c0ec8e3b52c386d001e735e302f6248cc282a156acd414d +size 194723 diff --git a/use-based-refs/use-based-refs.tex b/use-based-refs/use-based-refs.tex index 81e2cff845ab23f7aaa86402c80eaed47832a482..ed14726ed05fa7954b32b2e83328ff8a0e9ab057 100644 --- a/use-based-refs/use-based-refs.tex +++ b/use-based-refs/use-based-refs.tex @@ -78,63 +78,6 @@ We propose an alternative approach to borrow checking by introducing \item a formalization of these concepts in an extension to a simple $\lambda$-calculus (\autoref{sec:formalization}). \end{itemize} -\section{Location and Provenance}\label{sec:use-based-refs} - -To enforce AXM, there are three pieces of information that must be known at each point during execution: - -\begin{itemize} - \item All references which may be accessed at that point, - \item The kind of access, that is read or write, and - \item which of these references may alias. -\end{itemize} - -It can then be guaranteed that no set of references violates AXM. To ensure this, a reference comes with the following data: - -\begin{itemize} - \item A unique identifier which is generated at the point of creation of the reference.\todo[inline]{Do we allow creation of references outside of variable definitions? Otherwise, we could have reference id = variable name, assuming single static assignment.} - \item A \emph{provenance}, that is a set of locations that the reference may point to. Two references may alias if they have overlapping provenance. -\end{itemize} - -\subsection{Concrete Locations} - -Locations can be \emph{concrete} or \emph{abstract}. A \emph{concrete location} is created by an allocation and refers to the portion of memory which is reserved by the allocation. For example, in the code - -\begin{algorithmic} - \State{$r_1$ \gets \Call{alloc}{$T$}} - \State{$r_2$ \gets $\&v$} -\end{algorithmic} - -$r_1$ is the result of an allocation, meaning there is a concrete location $l$ and the provenance of $r_1$ is just the set $\{l\}$. Further, $r_2$ is derived from $r_1$ and inherits its provenance. - -\subsection{Abstract Locations} - -An \emph{abstract location} is used as a standin whenever the concrete location is not known because it is e.g. passed as a function argument. For example, in - -\begin{algorithmic} - \Function{TakeTwo}{$r_1 \colon \&T$, $r_2 \colon \&T$} - \State{$e$} - \EndFunction -\end{algorithmic} - -the concrete locations are not known, necessitating us to create a fresh abstract location $p_i$ for each $r_i$. Since $r_1$ and $r_2$ are of the same type, they may alias, for example through a call like the following: - -\begin{algorithmic} - \State{$r$ \gets \Call{alloc}{$T$}} - \State{\Call{TakeTwo}{$r$, $r$}} -\end{algorithmic} - -Thus both references have the same provenance $\{p_1, p_2\}$. - -% Additionally, we need a \emph{state graph}. It augments the control-flow graph of the program by keeping track for each node of all references that are in scope at that point. References may be in several \emph{states}: - -% \begin{itemize} -% \item An \emph{inactive} reference is guaranteed to not be used at this point, -% \item a reference in the \emph{read} state may be read but not be written to, -% \item the \emph{write} allows writing as well as reading, and -% \item a \emph{dead} reference may not be accessed until it falls of scope. -% \item {\color{red} \emph{drop/own} can be dropped, for owning pointers?} -% \end{itemize} - \section{Regions and Aliasing}\label{sec:provenance} We propose that the construction of provenance sets shall only rely on the local context of a function $f$. There are three ways of bringing a reference into context, each of which comes with a different way to determine its region.